{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,15]],"date-time":"2026-05-15T18:22:50Z","timestamp":1778869370851,"version":"3.51.4"},"publisher-location":"California","reference-count":0,"publisher":"International Joint Conferences on Artificial Intelligence Organization","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024,11]]},"abstract":"<jats:p>We study synthesis and verification of probabilistic models \n\nand specifications over finite traces. Probabilistic models\n\nare formalized in this work as Markov Chains and Markov\n\nDecisions Processes. Motivated by the recent attention given\n\nto, and importance of, finite-trace specifications in AI, we\n\nuse linear-temporal logic on finite traces as a specification\n\nformalism for properties of traces with finite but unbounded\n\ntime horizons. Since there is no bound on the time horizon,\n\nour Markov chains generate infinite traces, and we consider\n\ntwo possible semantics: \u201cexistential (resp. universal) prefix-\n\nsemantics\u201d which says that the finite-trace property holds\n\non some (resp. every) finite prefix of the trace. For both\n\ntypes of semantics, we study two computational problems:\n\nthe verification problem \u2014 \u201cdoes a given Markov chain \n\nsatisfy the specification with probability one?\u201d; and the \n\nsynthesis problem \u2014 \u201cfind a strategy (if there is one) that ensures\n\nthe Markov decision process satisfies the specification with\n\nprobability one\u201d. We provide optimal algorithms that \n\nfollow an automata-theoretic approach, and prove that the \n\ncomplexity of the synthesis problem is 2EXPTIME-complete\n\nfor both semantics, and that for the verification problem it\n\nis PSPACE-complete for the universal-prefix semantics, but\n\nEXPSPACE-complete for the existential-prefix semantics.<\/jats:p>","DOI":"10.24963\/kr.2024\/3","type":"proceedings-article","created":{"date-parts":[[2024,10,26]],"date-time":"2024-10-26T06:30:28Z","timestamp":1729924228000},"page":"27-37","source":"Crossref","is-referenced-by-count":1,"title":["Probabilistic Synthesis and Verification for LTL on Finite Traces"],"prefix":"10.24963","author":[{"given":"Benjamin","family":"Aminof","sequence":"first","affiliation":[{"name":"TU Wien"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Linus","family":"Cooper","sequence":"additional","affiliation":[{"name":"The University of Sydney"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sasha","family":"Rubin","sequence":"additional","affiliation":[{"name":"The University of Sydney"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Moshe Y.","family":"Vardi","sequence":"additional","affiliation":[{"name":"Rice University"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Florian","family":"Zuleger","sequence":"additional","affiliation":[{"name":"TU Wien"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"10584","event":{"name":"21st International Conference on Principles of Knowledge Representation and Reasoning {KR-2023}","theme":"Artificial Intelligence","location":"Hanoi, Vietnam","acronym":"KR-2024","number":"21","sponsor":["Artificial Intelligence Journal","Principles of Knowledge Representation and Reasoning Inc.","Academic College of Tel-Aviv","European Association for Artificial Intelligence","National Science Foundation"],"start":{"date-parts":[[2024,11,1]]},"end":{"date-parts":[[2024,11,8]]}},"container-title":["Proceedings of the TwentyFirst International Conference on Principles of Knowledge Representation and Reasoning"],"original-title":[],"deposited":{"date-parts":[[2024,10,26]],"date-time":"2024-10-26T06:30:29Z","timestamp":1729924229000},"score":1,"resource":{"primary":{"URL":"https:\/\/proceedings.kr.org\/2024\/3"}},"subtitle":[],"proceedings-subject":"Artificial Intelligence Research Articles","short-title":[],"issued":{"date-parts":[[2024,11]]},"references-count":0,"URL":"https:\/\/doi.org\/10.24963\/kr.2024\/3","relation":{},"subject":[],"published":{"date-parts":[[2024,11]]}}}