{"id":"W7124280466","doi":"10.65109/azkd1797","title":"Managing an Agent's Changing Intentions Using ltlf Synthesis","year":2025,"lang":"","type":"article","venue":"","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":0,"is_retracted":false,"has_abstract":true,"ca_institutions":"York University","funders":"","keywords":"Exploit; Nondeterministic algorithm; Domain (mathematical analysis); Linear temporal logic; Temporal logic; Domain knowledge; Multi-agent 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":["metaepi_narrow"],"consensus_categories":[],"category_scores_codex":[0.002423397,0.0003065544,0.0003064356,0.001406752,0.001059008,0.0009208283,0.001592,0.0001401087,0.0001985903],"category_scores_gemma":[0.0003909918,0.0003424913,0.0001797108,0.00260933,0.0001488811,0.002348552,0.001030032,0.0002665466,0.00006640093],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.0003423477,"about_ca_system_score_gemma":0.0001911148,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.0001136684,"about_ca_topic_score_gemma":0.0000120559,"domain_scores_codex":[0.9967015,0.000537743,0.0006466561,0.0008885944,0.0004376406,0.0007879142],"domain_scores_gemma":[0.9977484,0.0001506172,0.0002159987,0.001524239,0.0002106137,0.0001501837],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"design_other","study_design_gemma":"simulation_or_modeling","study_design_scores_codex":[0.000006352935,0.0001252439,0.0001187718,0.0001268348,0.0000697342,0.000006166483,0.00112424,0.001528741,0.004178778,0.4358191,0.00003035696,0.5568658],"study_design_scores_gemma":[0.00008824176,0.00002432922,0.0005629828,0.0004338082,0.0001090195,0.0000115591,0.001356215,0.9694365,0.02137326,0.005633157,0.0006456813,0.0003253027],"study_design_candidate":"simulation_or_modeling","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.00529392,0.0002330651,0.9544999,0.000888021,0.003659966,0.0003371634,0.000002042666,0.0002765267,0.03480937],"genre_scores_gemma":[0.3454964,0.00006712791,0.652241,0.0004058091,0.00007850703,0.00002468936,6.936865e-7,0.00001490651,0.001670871],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.9679077,"threshold_uncertainty_score":0.9999027,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.08121746610711375,"score_gpt":0.3566752332864925,"score_spread":0.2754577671793788,"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."}}