{"id":"W4414783286","doi":"10.1145/3769868","title":"The Complexity of Linear Temporal Verification for Continuous Counter Systems","year":2025,"lang":"en","type":"article","venue":"ACM Transactions on Computational Logic","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":0,"is_retracted":false,"has_abstract":true,"ca_institutions":"Université de Sherbrooke","funders":"","keywords":"Linear temporal logic; Temporal logic; Fragment (logic); Constant (computer programming); Computational complexity theory; Time complexity; Hybrid system; Linear logic","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.0006792683,0.0001168573,0.0001690594,0.0001188114,0.0005194441,0.00008844816,0.0009088375,0.00006649319,0.000002464149],"category_scores_gemma":[0.0001325876,0.00009248945,0.0000994646,0.0004027657,0.000257322,0.0001925703,0.00001285277,0.0001214767,0.00001001872],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.00007541801,"about_ca_system_score_gemma":0.0001181442,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.00002566352,"about_ca_topic_score_gemma":0.000004098447,"domain_scores_codex":[0.9987251,0.0001542745,0.0004442731,0.0002716735,0.0002508501,0.0001538904],"domain_scores_gemma":[0.9977494,0.0009270685,0.000194362,0.0006121709,0.0004897245,0.00002724732],"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.00006621976,0.0001215427,0.00002532381,0.0000433867,0.00004509299,1.371581e-7,0.00008078528,0.1138963,0.00007344703,0.8691935,0.0001919963,0.01626225],"study_design_scores_gemma":[0.0004319587,0.0001608878,0.002083858,0.00003227884,0.00001560889,0.000004085791,0.00007300682,0.8059425,0.0006853429,0.1853676,0.005095368,0.0001075245],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.0006808552,0.00008895381,0.9947813,0.002366949,0.001029264,0.000605603,0.00004265775,0.00009911075,0.000305334],"genre_scores_gemma":[0.5465728,0.000006351252,0.4529447,0.0001483596,0.00001602945,0.0001226516,0.00001793856,0.000004086412,0.0001670451],"genre_candidate":"methods","genre_consensus":null,"teacher_disagreement_score":0.6920462,"threshold_uncertainty_score":0.3995196,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.08437898775922498,"score_gpt":0.3436640172484169,"score_spread":0.2592850294891919,"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."}}