KR2024Proceedings of the 21st International Conference on Principles of Knowledge Representation and ReasoningProceedings of the 21st International Conference on Principles of Knowledge Representation and Reasoning

Hanoi, Vietnam. November 2-8, 2024.

Edited by

ISSN: 2334-1033
ISBN: 978-1-956792-05-8

Sponsored by
Published by

Copyright © 2024 International Joint Conferences on Artificial Intelligence Organization

Probabilistic Synthesis and Verification for LTL on Finite Traces

  1. Benjamin Aminof(TU Wien)
  2. Linus Cooper(The University of Sydney)
  3. Sasha Rubin(The University of Sydney)
  4. Moshe Y. Vardi(Rice University)
  5. Florian Zuleger(TU Wien)

Keywords

  1. Reasoning about actions and change, action languages-General

Abstract

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.