Plan Logic

Strategy logics has two major flaws: the decision problems associated have a high complexity (model checking is non elementary and satisfiability is undecidable) and the strategy quantified might not be feasible. However, these drawbacks appear to be related as the fragment One Goal has a 2-EXPTIME complexity and feasible strategies suffice to verify a formula. In this work, we propose an approach to define a logic suited to reason about feasible strategies by changing the domain of quantification. We replace strategies with plans (sequences of actions) and define a behavioral compositional semantics to ensure feasibility. This allows for the definition of an equivalent game-theoretic semantics and then, 2-EXPTIME decision procedures. Contributed talk given by Dylan Bellier

Authors

• Dylan Bellier

Keywords

No keywords are indexed for this paper.