{"id":"W2046971437","doi":"10.1002/smr.527","title":"Model checking timed properties of healthcare processes","year":2011,"lang":"en","type":"article","venue":"Journal of Software Maintenance and Evolution Research and Practice","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":1,"is_retracted":false,"has_abstract":true,"ca_institutions":"St. Francis Xavier University","funders":"","keywords":"Computer science; Correctness; Model checking; Workflow; Temporal logic; Modalities; Process (computing); Software engineering; Distributed computing; Programming language; Database","routes":{"ca_aff":true,"ca_fund":false,"ca_venue":false,"about_ca":false,"invisible_to_affiliation_only":false},"retraction":null,"screen":null,"direct_labels":[],"prediction":{"model_version":"metacan-v3-hybrid-931329e0061c","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.01080618,0.0009730759,0.0009954444,0.001435972,0.0008376441,0.003298007,0.002203398,0.001724602,0.002231406],"category_scores_gemma":[0.04467896,0.001116553,0.002758413,0.0007349643,0.00439011,0.003541416,0.00264224,0.001900076,0.0002633179],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.002311826,"about_ca_system_score_gemma":0.003817527,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.00739068,"about_ca_topic_score_gemma":0.004768218,"domain_scores_codex":[0.9862714,0.005260564,0.001274908,0.002103071,0.004050796,0.001039159],"domain_scores_gemma":[0.9480851,0.03849673,0.005094823,0.004513058,0.00328807,0.000522124],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"simulation_or_modeling","study_design_gemma":"simulation_or_modeling","study_design_scores_codex":[0.0009726449,0.0003261599,0.009079698,0.00065312,0.0004787218,0.001713529,0.001296513,0.7171497,0.03223425,0.193282,0.001082098,0.04173167],"study_design_scores_gemma":[0.0001794108,0.0001469033,0.0003105106,0.00007846851,0.0001306442,0.0001446287,0.00007156272,0.9074079,0.02462255,0.06516546,0.001708344,0.00003346652],"study_design_candidate":"simulation_or_modeling","study_design_consensus":"simulation_or_modeling","genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.07729997,0.0001146937,0.9181352,0.000252487,0.00005186859,0.000190641,0.0001509346,0.002452448,0.00135175],"genre_scores_gemma":[0.7931048,0.0001258208,0.2048298,0.0001583015,0.00004008785,0.0002923487,0.0003314634,0.0002382678,0.0008791029],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.01080618,"threshold_uncertainty_score":0.05714929,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.2684335454673087,"score_gpt":0.3914422192825324,"score_spread":0.1230086738152237,"validation_status":"score_only:v0-immature-baseline","note":"Baseline scores from an immature model (maturity gate not passed). Scores rank; they never assert a category."}}