{"id":"W2034102118","doi":"10.1145/990010.990011","title":"Multi-valued symbolic model-checking","year":2003,"lang":"en","type":"article","venue":"ACM Transactions on Software Engineering and Methodology","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":188,"is_retracted":false,"has_abstract":true,"ca_institutions":"University of Toronto","funders":"","keywords":"Model checking; Computer science; CTL*; Computation tree logic; Theoretical computer science; Generalization; Kripke structure; Symbolic trajectory evaluation; Abstraction model checking; Class (philosophy); Temporal logic; Extension (predicate logic); Algorithm; Programming language; Artificial intelligence; 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.005600933,0.001132307,0.00147992,0.001512904,0.001264736,0.003920918,0.003476509,0.001557758,0.004792453],"category_scores_gemma":[0.01655601,0.0007470801,0.002841321,0.001349346,0.003900097,0.006764889,0.004209601,0.002886376,0.0005700552],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.003185109,"about_ca_system_score_gemma":0.003867555,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.003913706,"about_ca_topic_score_gemma":0.004841553,"domain_scores_codex":[0.9928832,0.00228974,0.0005339594,0.001093258,0.002634537,0.0005652841],"domain_scores_gemma":[0.9868034,0.008081825,0.00086336,0.002661633,0.001341709,0.0002481412],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"theoretical_or_conceptual","study_design_gemma":"simulation_or_modeling","study_design_scores_codex":[0.000223964,0.0001096801,0.001543814,0.0003566549,0.0001391397,0.0004598579,0.0004512782,0.2755729,0.005388716,0.6705075,0.001877678,0.04336882],"study_design_scores_gemma":[0.0000582361,0.00003594123,0.00007916423,0.00006606608,0.00005094384,0.00009422375,0.00004556232,0.7462946,0.008944369,0.2389122,0.005389352,0.00002948721],"study_design_candidate":"simulation_or_modeling","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.01120479,0.000171009,0.9820306,0.0003902851,0.00009396883,0.0001082942,0.0001807664,0.001993113,0.003827104],"genre_scores_gemma":[0.4159349,0.0003185491,0.5790212,0.0003638101,0.00006672918,0.0003392937,0.0005335012,0.0003952394,0.003026759],"genre_candidate":"empirical","genre_consensus":null,"teacher_disagreement_score":0.005600933,"threshold_uncertainty_score":0.02962089,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.153068929282084,"score_gpt":0.3447623535611903,"score_spread":0.1916934242791064,"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."}}