{"id":"W2131659851","doi":"10.1109/real.1989.63560","title":"Real-time temporal logic decision procedures","year":2003,"lang":"en","type":"article","venue":"","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":12,"is_retracted":false,"has_abstract":true,"ca_institutions":"York University","funders":"","keywords":"Reachability; Temporal logic; Model checking; Class (philosophy); Computer science; Linear temporal logic; Theoretical computer science; Graph; State (computer science); Algorithm; 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":"metacan-v3-hybrid-931329e0061c","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.006001117,0.00140843,0.0008467647,0.001865356,0.001029031,0.004875117,0.002237837,0.001399099,0.01401295],"category_scores_gemma":[0.01221555,0.0007356181,0.001910797,0.001172218,0.002621571,0.005442495,0.001769921,0.0025178,0.004347967],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.002439051,"about_ca_system_score_gemma":0.00327822,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.003126018,"about_ca_topic_score_gemma":0.002588178,"domain_scores_codex":[0.9936889,0.00246726,0.0006383394,0.001099984,0.0014943,0.0006110346],"domain_scores_gemma":[0.9932877,0.004361019,0.0006281094,0.0006596324,0.0008474768,0.0002160475],"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.0002107827,0.0001055632,0.0003089121,0.0002834966,0.00006316586,0.0003127204,0.0003032167,0.02527643,0.002766176,0.9129814,0.006215912,0.0511723],"study_design_scores_gemma":[0.0003279786,0.0001064434,0.0001173447,0.0001786138,0.0001317755,0.0003119713,0.0001085176,0.2386985,0.01641679,0.6683816,0.07513456,0.00008582041],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":"theoretical_or_conceptual","genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.00489603,0.0005498045,0.968983,0.0007151734,0.0001579542,0.0003972235,0.0007823923,0.004415162,0.01910328],"genre_scores_gemma":[0.2615691,0.001196077,0.7199838,0.0007041687,0.0002531562,0.0009404965,0.001523631,0.0006361894,0.01319341],"genre_candidate":"empirical","genre_consensus":null,"teacher_disagreement_score":0.01401295,"threshold_uncertainty_score":0.04687804,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.03066513431433942,"score_gpt":0.3148106458169055,"score_spread":0.2841455115025661,"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."}}