{"id":"W3041597941","doi":"10.24963/ijcai.2020/690","title":"Pure-Past Linear Temporal and Dynamic Logic on Finite Traces","year":2020,"lang":"en","type":"article","venue":"","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":43,"is_retracted":false,"has_abstract":true,"ca_institutions":"York University","funders":"European Commission","keywords":"TRACE (psycholinguistics); Exponential function; Computer science; Exploit; Expressive power; Linear temporal logic; Temporal logic; Theoretical computer science; Algorithm; Markov decision process; Discrete mathematics; Algebra over a field; Mathematics; Markov process; Pure mathematics; Statistics","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.0001784905,0.00008126171,0.0000861368,0.00003219966,0.00005305678,0.00007043023,0.0003518238,0.00004121902,0.00001370634],"category_scores_gemma":[0.00009281707,0.00006420622,0.00001795036,0.000207177,0.00003482693,0.0002759306,0.00009100713,0.0001044287,0.00009148248],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.000008932872,"about_ca_system_score_gemma":0.000011408,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.000002984147,"about_ca_topic_score_gemma":0.00000158542,"domain_scores_codex":[0.9993057,0.00005797041,0.0001271767,0.000263523,0.0001302296,0.0001154178],"domain_scores_gemma":[0.9995805,0.00006420487,0.00004579408,0.0002119193,0.00002045898,0.00007713064],"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.0000776504,0.0001700243,0.002408243,0.0001299138,0.00002657713,0.00005160428,0.004667822,0.002735645,0.003799585,0.7095399,0.001752062,0.2746409],"study_design_scores_gemma":[0.0001562417,0.0003556248,0.002109361,0.000006223504,0.000001720077,0.000005362465,0.0000482803,0.9895764,0.001622226,0.002674887,0.00330611,0.00013755],"study_design_candidate":"simulation_or_modeling","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.02134781,0.00003759527,0.9686542,0.005957611,0.0001261211,0.0001054335,0.000001286386,0.0002119357,0.003557964],"genre_scores_gemma":[0.4661525,0.000007553742,0.532154,0.00150852,0.00003104339,0.000003278681,0.000001195269,0.000003205656,0.0001386561],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.9868408,"threshold_uncertainty_score":0.2618254,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.05130476406004403,"score_gpt":0.3058876475245288,"score_spread":0.2545828834644848,"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."}}