{"id":"W2807813222","doi":"10.24963/ijcai.2018/651","title":"LTL Realizability via Safety and Reachability Games","year":2018,"lang":"en","type":"article","venue":"","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":13,"is_retracted":false,"has_abstract":true,"ca_institutions":"University of Toronto","funders":"Natural Sciences and Engineering Research Council of Canada","keywords":"Realizability; Reachability; Computer science; Bounded function; Duality (order theory); Theoretical computer science; Mathematical optimization; Mathematics; Algorithm; Discrete mathematics","routes":{"ca_aff":true,"ca_fund":true,"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.001715236,0.00008298923,0.0001106191,0.00002960641,0.0001156218,0.00005063714,0.0004067724,0.00005525678,0.00005004036],"category_scores_gemma":[0.0003260163,0.00006799172,0.0000228931,0.0002146897,0.0003025262,0.000469899,0.000253599,0.0000648268,0.00003695193],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.00004408034,"about_ca_system_score_gemma":0.00002153354,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.0002426126,"about_ca_topic_score_gemma":0.0000302264,"domain_scores_codex":[0.9988574,0.0002026496,0.0002247091,0.0004052887,0.0001454313,0.0001644783],"domain_scores_gemma":[0.9986593,0.00009535489,0.000054665,0.000991005,0.0001221151,0.00007762513],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"design_other","study_design_gemma":"observational","study_design_scores_codex":[0.0000276679,0.00005324611,0.006046406,0.0000209102,0.000004730285,2.625034e-7,0.001021424,5.975658e-7,0.001015964,0.4169435,0.0002018538,0.5746635],"study_design_scores_gemma":[0.0003061959,0.0003982454,0.6145822,0.00000965394,0.000005368921,0.00002978529,0.00004611747,0.2129662,0.02338017,0.115389,0.03252953,0.0003574126],"study_design_candidate":"observational","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.02202219,0.00001541297,0.9481994,0.0004955287,0.0002287384,0.0001356169,8.399075e-7,0.0002143734,0.02868793],"genre_scores_gemma":[0.3758611,0.000006610437,0.6237515,0.0001603628,0.00004138133,0.000002269371,4.754241e-7,0.000002531621,0.0001738403],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.6085358,"threshold_uncertainty_score":0.2772622,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.01935773119505705,"score_gpt":0.2962855395209094,"score_spread":0.2769278083258523,"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."}}