{"id":"W1581031502","doi":"10.3990/1.9789036529754","title":"Model checking nondeterministic and randomly timed systems","year":2009,"lang":"en","type":"dissertation","venue":"","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":58,"is_retracted":false,"has_abstract":true,"ca_institutions":"ImmunoPrecise (Canada)","funders":"Nederlandse Organisatie voor Wetenschappelijk Onderzoek","keywords":"Nondeterministic algorithm; Dependability; Computer science; Model checking; Markov decision process; A priori and a posteriori; Set (abstract data type); Markov process; Algorithm; Theoretical computer science; Mathematics","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.004201853,0.0008374091,0.0008807875,0.000812396,0.0006304738,0.001800233,0.001849866,0.001080195,0.001423832],"category_scores_gemma":[0.0175688,0.0007675945,0.001781296,0.0007678896,0.002549461,0.002431224,0.001691522,0.002019598,0.0002005832],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.001772346,"about_ca_system_score_gemma":0.002356282,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.003488755,"about_ca_topic_score_gemma":0.003565203,"domain_scores_codex":[0.994395,0.002093654,0.000333319,0.0008614926,0.001959085,0.0003573653],"domain_scores_gemma":[0.9882746,0.008758219,0.0009253575,0.001304094,0.000609844,0.0001278702],"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.00007214409,0.0000450148,0.001505896,0.00009976928,0.00006277134,0.00009042823,0.0001331509,0.8097051,0.004162557,0.169504,0.0002003286,0.01441876],"study_design_scores_gemma":[0.00001750857,0.0000183739,0.00008384563,0.000008065066,0.00001223711,0.00001902639,0.00001026476,0.9460207,0.003135227,0.05021858,0.0004493803,0.000006672747],"study_design_candidate":"simulation_or_modeling","study_design_consensus":"simulation_or_modeling","genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.03902032,0.00008627099,0.9587877,0.0001229887,0.0000221879,0.00004507576,0.00006116597,0.0004825569,0.001371832],"genre_scores_gemma":[0.6997463,0.0002114354,0.2979578,0.00008092139,0.00002853783,0.000249308,0.000242558,0.000173591,0.001309465],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.004201853,"threshold_uncertainty_score":0.0222218,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.03412737241085146,"score_gpt":0.3127440207977744,"score_spread":0.278616648386923,"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."}}