{"id":"W2617541639","doi":"10.1145/3019612.3019827","title":"Runtime verification of LTL on lossy traces","year":2017,"lang":"en","type":"article","venue":"","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":20,"is_retracted":false,"has_abstract":true,"ca_institutions":"University of Waterloo","funders":"","keywords":"Soundness; Runtime verification; Computer science; Lossy compression; TRACE (psycholinguistics); Linear temporal logic; Temporal logic; Real-time computing; Programming language; Formal verification; Artificial intelligence","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.005376361,0.001017164,0.0008305598,0.001052709,0.0009921853,0.002275069,0.002051401,0.0009960158,0.002950343],"category_scores_gemma":[0.0341646,0.0008435055,0.001531995,0.0007182128,0.003146301,0.004887654,0.002706336,0.00246055,0.00076898],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.002222053,"about_ca_system_score_gemma":0.003341546,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.004563096,"about_ca_topic_score_gemma":0.005230231,"domain_scores_codex":[0.9913287,0.002678779,0.0006789545,0.001390133,0.002966776,0.00095675],"domain_scores_gemma":[0.9669538,0.02056848,0.00232122,0.006873101,0.00292794,0.0003554746],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"simulation_or_modeling","study_design_gemma":"theoretical_or_conceptual","study_design_scores_codex":[0.0014962,0.0003559493,0.01423628,0.001200313,0.000244397,0.001755966,0.00223966,0.4704746,0.08445522,0.1842564,0.005690246,0.2335947],"study_design_scores_gemma":[0.0001124601,0.0001495032,0.0005287268,0.0001005213,0.00007121167,0.0001816206,0.0001312265,0.8575576,0.06228913,0.07520817,0.003630604,0.00003923093],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.03905689,0.0001131578,0.9491255,0.0002524617,0.00003165684,0.00009176071,0.0002339204,0.009535251,0.00155949],"genre_scores_gemma":[0.7580211,0.0001485152,0.2366878,0.0002712109,0.00004279703,0.0002670836,0.0007559,0.001763293,0.002042164],"genre_candidate":"empirical","genre_consensus":null,"teacher_disagreement_score":0.005376361,"threshold_uncertainty_score":0.0284332,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.04724271600627607,"score_gpt":0.3400370377423821,"score_spread":0.2927943217361061,"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."}}