{"id":"W3049098040","doi":"10.1145/605466.605488","title":"Model exploration with temporal logic query checking","year":2002,"lang":"en","type":"article","venue":"ACM SIGSOFT Software Engineering Notes","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":4,"is_retracted":false,"has_abstract":true,"ca_institutions":"University of Toronto","funders":"Natural Sciences and Engineering Research Council of Canada","keywords":"Temporal logic; Computer science; Computation tree logic; Model checking; Interval temporal logic; Linear temporal logic; Programming language; Set (abstract data type); Theoretical computer science; Computation","routes":{"ca_aff":true,"ca_fund":true,"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":["metaresearch"],"consensus_categories":[],"category_scores_codex":[0.000270544,0.0002336209,0.0001833154,0.0001488217,0.0001079126,0.0001458482,0.0009134393,0.0001016077,0.00001103487],"category_scores_gemma":[0.01944624,0.000214999,0.00004754885,0.000429478,0.00002524366,0.001713852,0.0001958179,0.000220712,0.00005344235],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.00007297864,"about_ca_system_score_gemma":0.00001994071,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.000008288185,"about_ca_topic_score_gemma":0.000001140201,"domain_scores_codex":[0.9986703,0.00002616996,0.0002487426,0.0004057558,0.000313008,0.0003360122],"domain_scores_gemma":[0.9958712,0.002848498,0.000103478,0.0009891747,0.00009688619,0.00009071277],"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.00001717841,0.0002008129,0.06281815,0.000280696,0.00006260566,0.00004663095,0.005113733,0.7978116,0.004676629,0.05124788,0.0004663986,0.07725775],"study_design_scores_gemma":[0.0002258226,0.0001054008,0.004168972,0.00008818471,0.000008954434,0.00002622294,0.000008453183,0.9878253,0.006168114,0.0006087894,0.0002792458,0.0004865503],"study_design_candidate":"simulation_or_modeling","study_design_consensus":"simulation_or_modeling","genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.02208219,0.0001855739,0.9758283,0.0002402296,0.0001989289,0.0001473268,0.000001809918,0.001305211,0.00001040331],"genre_scores_gemma":[0.4786982,0.000009186114,0.5211084,0.00006661774,0.00003975242,0.00003341772,0.000003834699,0.00001868759,0.00002195035],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.456616,"threshold_uncertainty_score":0.9888134,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.0878801679724055,"score_gpt":0.2611513623034099,"score_spread":0.1732711943310044,"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."}}