Hanoi, Vietnam. November 2-8, 2024.
ISSN: 2334-1033
ISBN: 978-1-956792-05-8
Copyright © 2024 International Joint Conferences on Artificial Intelligence Organization
We study synthesis and verification of probabilistic models
and specifications over finite traces. Probabilistic models
are formalized in this work as Markov Chains and Markov
Decisions Processes. Motivated by the recent attention given
to, and importance of, finite-trace specifications in AI, we
use linear-temporal logic on finite traces as a specification
formalism for properties of traces with finite but unbounded
time horizons. Since there is no bound on the time horizon,
our Markov chains generate infinite traces, and we consider
two possible semantics: “existential (resp. universal) prefix-
semantics” which says that the finite-trace property holds
on some (resp. every) finite prefix of the trace. For both
types of semantics, we study two computational problems:
the verification problem — “does a given Markov chain
satisfy the specification with probability one?”; and the
synthesis problem — “find a strategy (if there is one) that ensures
the Markov decision process satisfies the specification with
probability one”. We provide optimal algorithms that
follow an automata-theoretic approach, and prove that the
complexity of the synthesis problem is 2EXPTIME-complete
for both semantics, and that for the verification problem it
is PSPACE-complete for the universal-prefix semantics, but
EXPSPACE-complete for the existential-prefix semantics.