Strategic Knowledge of the Past - Expressivity and Complexity

Abstract In this article we present theoretical results for an epistemic strategy logic with past operators, \(\text {PKSL}\). In \(\text {PKSL}\), agents are able to choose their strategies depending on past moves of other agents. This strictly extends the expressive power of some well-known epistemic strategy logics, which we illustrate by modelling forward induction: a rationality criterion, called admissibility, may be defined over agent’s strategies. Admissibility specifies coherence conditions between past and future actions, inducing new conditions for the availability of optimal strategies. We also give a resolution algorithm for \(\text {PKSL}\) model-checking. It runs in exponential time, while the satisfiability problem is undecidable, as is the case for similar logics for strategies such as Strategy Logic.

Authors

• Christophe Chareton

Keywords

No keywords are indexed for this paper.