{"id":"W2101814946","doi":"10.1145/2071368.2071369","title":"Robust Vacuity for Branching Temporal Logic","year":2012,"lang":"en","type":"article","venue":"ACM Transactions on Computational Logic","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":25,"is_retracted":false,"has_abstract":true,"ca_institutions":"University of Toronto","funders":"","keywords":"Computer science; Temporal logic; Bisimulation; Linear temporal logic; Atomic sentence; Theoretical computer science; Model checking; TRACE (psycholinguistics); Algorithm; Artificial intelligence; Linguistics; Philosophy","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.006492449,0.0008373233,0.001214874,0.002289176,0.001604398,0.003914874,0.002262538,0.001567117,0.003407867],"category_scores_gemma":[0.02658142,0.0009051015,0.002881663,0.00221052,0.005675228,0.007189348,0.004038026,0.007060933,0.0004777341],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.004897924,"about_ca_system_score_gemma":0.001864402,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.004446039,"about_ca_topic_score_gemma":0.002770606,"domain_scores_codex":[0.9915425,0.001895305,0.0006450305,0.00164278,0.003670331,0.000604025],"domain_scores_gemma":[0.9799981,0.01386851,0.001454474,0.002652949,0.001630238,0.0003956754],"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.0002402801,0.00009103791,0.00153434,0.0003936453,0.0001151969,0.0004386149,0.0008785572,0.04344482,0.009325893,0.9018469,0.002403465,0.03928721],"study_design_scores_gemma":[0.00003017305,0.00002844583,0.0001892776,0.00003680553,0.00003446091,0.0001161017,0.00006429678,0.1305026,0.003386937,0.8633698,0.002213591,0.00002754718],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":"theoretical_or_conceptual","genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.04186722,0.0007565185,0.9402775,0.002352326,0.00007621609,0.0002403025,0.0003304723,0.003253418,0.01084619],"genre_scores_gemma":[0.6629657,0.0008502139,0.3295902,0.001190078,0.0002849209,0.000348734,0.0009333211,0.0004355907,0.003401311],"genre_candidate":"empirical","genre_consensus":null,"teacher_disagreement_score":0.006492449,"threshold_uncertainty_score":0.03553706,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.1477206214645475,"score_gpt":0.3420534356106389,"score_spread":0.1943328141460914,"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."}}