{"id":"W2115995803","doi":"10.1109/ismvl.2001.924571","title":"Model checking with multi-valued temporal logics","year":2002,"lang":"en","type":"article","venue":"","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":18,"is_retracted":false,"has_abstract":true,"ca_institutions":"University of Toronto","funders":"","keywords":"Computation tree logic; Model checking; Kripke structure; Computer science; Kripke semantics; Linear temporal logic; Temporal logic; Binary decision diagram; Theoretical computer science; Atomic sentence; Truth value; Extension (predicate logic); Semantics (computer science); Algorithm; Symbolic trajectory evaluation; Programming language; Intermediate logic; Description logic; Artificial intelligence","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":[],"consensus_categories":[],"category_scores_codex":[0.0002597358,0.00008750146,0.00008137979,0.0000452296,0.00007630555,0.00007892851,0.0005236131,0.0000419699,0.00002186098],"category_scores_gemma":[0.00002956557,0.00006344515,0.00002093696,0.0002377987,0.00003416168,0.0005450768,0.00009054649,0.00008934028,0.00006555],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.00002769627,"about_ca_system_score_gemma":0.00001070842,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.000009913751,"about_ca_topic_score_gemma":0.000003841008,"domain_scores_codex":[0.9992294,0.00003582803,0.0001289768,0.0002393842,0.0001900796,0.0001762914],"domain_scores_gemma":[0.9993603,0.000007860482,0.00005881156,0.0004682381,0.00005421099,0.00005064146],"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.000005440179,0.0001982838,0.001799512,0.00001500375,0.0000118877,0.000008045933,0.00175986,0.02396083,0.0007894163,0.9357275,0.0005761369,0.03514808],"study_design_scores_gemma":[0.0001883336,0.00003718569,0.0002980766,0.000004371821,0.00000140421,0.000008198306,0.00001164776,0.9966098,0.001933438,0.0006647308,0.0001297454,0.0001130525],"study_design_candidate":"simulation_or_modeling","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.00348677,0.0000199709,0.9830971,0.0001050709,0.00006371264,0.00009424592,2.052432e-7,0.0002630617,0.01286989],"genre_scores_gemma":[0.275014,0.000003072144,0.7236436,0.0002178135,0.000009348382,0.000006004675,2.569573e-7,0.00000445742,0.00110147],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.972649,"threshold_uncertainty_score":0.2587218,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.1960418190841804,"score_gpt":0.3158974532877719,"score_spread":0.1198556342035915,"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."}}