Probabilistic Synthesis and Verification for LTL on Finite Traces

Abstract

We study synthesis and verifcation of probabilistic models and specifcations over fnite 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, fnite-trace specifcations in AI, we use linear-temporal logic on fnite traces as a specifcation formalism for properties of traces with fnite but unbounded time horizons. Since there is no bound on the time horizon, our Markov chains generate infnite traces, and we consider two possible semantics: “existential (resp. universal) prefxsemantics” which says that the fnite-trace property holds on some (resp. every) fnite prefx of the trace. For both types of semantics, we study two computational problems: the verifcation problem — “does a given Markov chain satisfy the specifcation with probability one?”; and the synthesis problem — “fnd a strategy (if there is one) that ensures the Markov decision process satisfes the specifcation 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 verifcation problem it is PSPACE complete for the universal-prefx semantics, but EXPSPACE complete for the existential-prefx semantics