{"id":"W3158643107","doi":"10.1145/3412841.3442138","title":"Offline monitoring of LTL with bit vectors","year":2021,"lang":"en","type":"article","venue":"","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":0,"is_retracted":false,"has_abstract":true,"ca_institutions":"Université du Québec à Chicoutimi","funders":"","keywords":"Bitmap; Computer science; Extension (predicate logic); Linear temporal logic; Event (particle physics); Throughput; Temporal logic; Programming language; Algorithm; Real-time computing; Theoretical computer science; Artificial intelligence; Operating system","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.0001480798,0.00004215049,0.00006816856,0.00003090133,0.00001980522,0.00002087593,0.0002349138,0.00001810031,0.00001308524],"category_scores_gemma":[0.00005000822,0.00003280444,0.00001507972,0.0003868309,0.00001673962,0.0002187355,0.00007345569,0.00004202928,0.00000735072],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.00001237079,"about_ca_system_score_gemma":0.00004408922,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.00000805494,"about_ca_topic_score_gemma":8.65801e-7,"domain_scores_codex":[0.9995003,0.00003190216,0.0001052414,0.0001339396,0.0001478603,0.00008078106],"domain_scores_gemma":[0.9994124,0.00003042137,0.00004378665,0.0003721101,0.0001154608,0.00002581432],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"theoretical_or_conceptual","study_design_gemma":"bench_or_experimental","study_design_scores_codex":[0.00001513556,0.0001774674,0.0498226,0.00008498128,0.00004772111,0.00002742278,0.001145094,0.0004666908,0.07181902,0.7122889,0.0001140327,0.163991],"study_design_scores_gemma":[0.00009836291,0.000052999,0.02428308,0.00002049215,0.000002312189,0.00001086853,0.00005000054,0.008702615,0.9654364,0.0005450539,0.000731518,0.00006631322],"study_design_candidate":"bench_or_experimental","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.1274012,0.00004392966,0.8664072,0.00009080979,0.0002578571,0.00002607157,1.72708e-7,0.00005940583,0.005713414],"genre_scores_gemma":[0.2103888,0.000004731559,0.7890081,0.00001196145,0.0000268708,0.000001815841,2.112034e-7,0.000002420041,0.0005550818],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.8936174,"threshold_uncertainty_score":0.1337726,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.03018059981207601,"score_gpt":0.2873061213270114,"score_spread":0.2571255215149354,"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."}}