{"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":"metacan-v3-hybrid-931329e0061c","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.008106193,0.001641196,0.00144808,0.002991338,0.001258714,0.003432382,0.003845726,0.001763169,0.005249583],"category_scores_gemma":[0.03484001,0.001623049,0.003377285,0.002419559,0.005528235,0.009750882,0.006420494,0.005205478,0.0009561746],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.001736437,"about_ca_system_score_gemma":0.00289491,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.003490327,"about_ca_topic_score_gemma":0.003048197,"domain_scores_codex":[0.9913693,0.003300776,0.0007333376,0.001294448,0.002796743,0.0005054129],"domain_scores_gemma":[0.9650836,0.02589614,0.001647098,0.005233979,0.001718241,0.0004209621],"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.0006734086,0.0002677476,0.002942641,0.001012972,0.0002900989,0.001152461,0.001755689,0.08064788,0.01791601,0.6163363,0.01572727,0.2612774],"study_design_scores_gemma":[0.0001570236,0.0001491202,0.000233536,0.0001991135,0.0001178575,0.0005478488,0.0001946078,0.5701344,0.02741492,0.3762074,0.02454856,0.00009561584],"study_design_candidate":"simulation_or_modeling","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.001950414,0.00009049918,0.9902238,0.0002543266,0.00002799582,0.00009045768,0.0001415946,0.006410328,0.0008105014],"genre_scores_gemma":[0.1111023,0.0002703744,0.8848001,0.0003835187,0.00007700578,0.0004222654,0.0005573101,0.001161602,0.001225354],"genre_candidate":"empirical","genre_consensus":null,"teacher_disagreement_score":0.008106193,"threshold_uncertainty_score":0.0428701,"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."}}