{"id":"W2116117396","doi":"10.1109/tse.2003.1237171","title":"Temporal logic query checking: a tool for model exploration","year":2003,"lang":"en","type":"article","venue":"IEEE Transactions on Software Engineering","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":67,"is_retracted":false,"has_abstract":true,"ca_institutions":"University of Toronto","funders":"","keywords":"Computer science; Temporal logic; Model checking; Kripke structure; Theoretical computer science; Query optimization; Computation tree logic; Linear temporal logic; Interval temporal logic; Query language; Set (abstract data type); Programming language; Information retrieval","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.0003882326,0.0001713351,0.0001393492,0.0001774914,0.0001390742,0.00008302315,0.00025991,0.00009933687,0.000003665897],"category_scores_gemma":[0.0001086109,0.0001865779,0.0001047273,0.0003299566,0.00001094128,0.001033037,0.000001102925,0.0001746276,0.00001123838],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.0001117557,"about_ca_system_score_gemma":0.00005803399,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.000001413983,"about_ca_topic_score_gemma":5.765879e-7,"domain_scores_codex":[0.9989728,0.0000290533,0.0002520865,0.0003157709,0.0001779108,0.0002523824],"domain_scores_gemma":[0.9992771,0.0001064769,0.00005316676,0.0004250885,0.00008056447,0.00005766384],"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.000005544655,0.0000451715,0.000003311314,0.0000337616,0.00001022009,5.704845e-7,0.000228378,0.9652297,0.0009111373,0.02635517,0.00001965651,0.007157341],"study_design_scores_gemma":[0.000226273,0.00006420879,0.000007647496,0.00002337023,0.000007775653,0.000007105452,0.000008358098,0.9439422,0.05362055,0.001267581,0.0005931261,0.0002318121],"study_design_candidate":"simulation_or_modeling","study_design_consensus":"simulation_or_modeling","genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.001168264,0.00001810847,0.9967959,0.00002619429,0.0008999251,0.0003312548,0.000006387062,0.0007340842,0.00001989177],"genre_scores_gemma":[0.2911915,0.000005216846,0.7083837,0.00004905716,0.00001593222,0.0002480019,0.000001289689,0.00001948356,0.00008585965],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.2900232,"threshold_uncertainty_score":0.7608427,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.05622366089218801,"score_gpt":0.2785760117045132,"score_spread":0.2223523508123252,"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."}}