KR Conference 2018 Conference Paper
- Bastien Maubert
- Aniello Murano
Distributed systems are often open systems, i. e., they interact with an environment and must react appropriately to actions taken by this environment. As a result, if we take the analogy where processors are players of a game, and processes are strategies for the processors, the task of synthesising distributed protocols can be seen as synthesising winning strategies in multi-player games with imperfect information. This analogy between the two settings is well known, and Ladner and Reif already wrote in (Ladner and Reif 1986) that “Distributed protocols are equivalent to (i. e., can be formally modelled as) games”. To reason about a certain type of game-related properties in distributed systems, Alternating-time Temporal Logic (ATL) was introduced (Alur, Henzinger, and Kupferman 2002). It can express the existence of strategies for coalitions of players in multi-player games, but cannot express some important game-theoretic concepts, such as the existence of Nash equilibria. To remedy this, Strategy Logic (SL) (Chatterjee, Henzinger, and Piterman 2010; Mogavero et al. 2014) was defined. Treating strategies as explicit first-order objects makes it very expressive, and it can for instance talk about Nash equilibria in a very natural way. These logics have been studied both for players with perfect information and players with imperfect information, and in the latter case either with the assumption that agents have no memory, or that they remember everything they observe. This last assumption, called perfect recall, is the one usually considered in distributed synthesis (Pnueli and Rosner 1990) and games with imperfect information (Reif 1984), and it is also central in logics of knowledge and time (Fagin et al. 1995). It is the one we consider in this work. In order to reason about knowledge and strategic abilities in distributed systems, epistemic temporal logics and strategic logics have been combined. In particular, both ATL and SL have been extended with knowledge operators (van der Hoek and Wooldridge 2003; Jamroga and van der Hoek 2004; Belardinelli 2015; Dima, Enea, and Guelev 2010; Belardinelli et al. 2017a; 2017b). However, few decidable cases are known for the model checking of these logics with imperfect information and perfect recall. This is not surprising since strategic logics typically can express the existence of distributed strategies, a problem known to be undecidable for perfect recall, already for purely temporal specifications (Peterson and Reif 1979; Pnueli and Rosner 1990). Two distinct semantics have been considered for knowledge in the context of strategic reasoning, depending on whether players know each other’s strategy or not. In the former case, that we call the informed semantics, distributed synthesis for epistemic temporal specifications is undecidable, already on systems with hierarchical information. However, for the other, uninformed semantics, the problem is decidable on such systems. In this work we generalise this result by introducing an epistemic extension of Strategy Logic with imperfect information. The semantics of knowledge operators is uninformed, and captures agents that can change observation power when they change strategies. We solve the model-checking problem on a class of “hierarchical instances”, which provides a solution to a vast class of strategic problems with epistemic temporal specifications, such as distributed or rational synthesis, on hierarchical systems.