{"id":"W1735022296","doi":"10.1007/978-3-540-45187-7_18","title":"Multi-valued Model Checking via Classical Model Checking","year":2003,"lang":"en","type":"book-chapter","venue":"Lecture notes in computer science","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":67,"is_retracted":false,"has_abstract":false,"ca_institutions":"University of Toronto","funders":"","keywords":"Model checking; Abstraction model checking; Computer science; Symbolic trajectory evaluation; Reuse; Extension (predicate logic); Theoretical computer science; Context (archaeology); Algorithm; Programming language","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":["metaepi_narrow"],"consensus_categories":[],"category_scores_codex":[0.002474148,0.0008840915,0.0008168833,0.000961314,0.0004869761,0.0007015474,0.005154382,0.0007494215,0.00000617875],"category_scores_gemma":[0.0002885216,0.0008664243,0.0002606025,0.0008507716,0.0009197972,0.001415581,0.001654468,0.001770014,0.00003844957],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.0008272792,"about_ca_system_score_gemma":0.0006781772,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.000006620177,"about_ca_topic_score_gemma":0.00001290362,"domain_scores_codex":[0.9935486,0.0001008392,0.0009775623,0.002546287,0.001648397,0.001178367],"domain_scores_gemma":[0.9960173,0.0001643787,0.0005831363,0.002523095,0.0003990305,0.0003130513],"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.00000480735,0.00004643658,0.000005154509,0.00003714208,0.00000896816,0.00001688006,0.0009093508,0.7425615,0.001282999,0.06827597,0.000009760548,0.186841],"study_design_scores_gemma":[0.0002948041,0.00005237076,0.00001026388,0.00022353,0.00001086386,0.00005261763,9.093679e-8,0.8702775,0.004047384,0.1240792,0.0001095295,0.0008418508],"study_design_candidate":"simulation_or_modeling","study_design_consensus":"simulation_or_modeling","genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.00004440554,0.0002240839,0.9943593,0.000291391,0.001634997,0.0005535077,0.000003883448,0.0003362822,0.002552122],"genre_scores_gemma":[0.01497092,0.0000305688,0.9820687,0.002176142,0.0002098014,0.00002281391,0.000003787837,0.0000749929,0.0004423404],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.1859992,"threshold_uncertainty_score":0.9993786,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.0640061665801301,"score_gpt":0.3078150874879148,"score_spread":0.2438089209077847,"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."}}