{"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":"codex-gemma-dda1882f352a","candidate_categories":["metaresearch"],"consensus_categories":[],"category_scores_codex":[0.005757476,0.00006912347,0.0001515225,0.00019581,0.0001765607,0.00005706864,0.000310389,0.00005501023,0.000001117925],"category_scores_gemma":[0.01288704,0.0000499468,0.00001887661,0.000414727,0.0002331704,0.002388553,0.0001352331,0.0003746083,0.000001057442],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.00005591648,"about_ca_system_score_gemma":0.0004945759,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.0001089928,"about_ca_topic_score_gemma":0.000005875219,"domain_scores_codex":[0.9984053,0.0003827677,0.0003433366,0.0001442326,0.0004833778,0.0002409894],"domain_scores_gemma":[0.9957622,0.0003860941,0.000402183,0.0001675466,0.00315922,0.0001228117],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"theoretical_or_conceptual","study_design_gemma":"theoretical_or_conceptual","study_design_scores_codex":[0.01905311,0.002512849,0.02572511,0.01179682,0.0004823631,0.0001975419,0.1003047,0.0004530742,0.02856136,0.4911035,0.005815276,0.3139943],"study_design_scores_gemma":[0.00708465,0.01945127,0.08750575,0.01272973,0.0001928126,0.01248141,0.03926904,0.2565345,0.08463302,0.4594931,0.01850013,0.00212461],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":"theoretical_or_conceptual","genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.02593185,0.007444673,0.9635695,0.002410668,0.0000815538,0.0001566364,0.000001353423,0.0000186589,0.0003851191],"genre_scores_gemma":[0.5993611,0.001643835,0.3988659,0.00004398065,0.00001797129,0.000003501096,5.585873e-8,0.000003347077,0.00006037264],"genre_candidate":"methods","genre_consensus":null,"teacher_disagreement_score":0.5734292,"threshold_uncertainty_score":0.9954278,"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."}}