KR Conference 2014 Conference Paper
- Xiaowei Huang
- Ron van der Meyden
logics. In particular, for dealing with epistemic reasoning in strategic settings, there are multiple proposals, with different semantic and syntactic bases, for how to capture reasoning about the availability to groups of agents of strategies for achieving particular goals (Jonker 2003; Schobbens 2004; van Otterloo and Jonker 2005; Jamroga 2003; Jamroga and Ågotnes 2007). We argue in this paper that this proliferation is unnecessary, and that an appropriate application of temporal epistemic logic, with a minor innovation, already has the power to deal with many issues of concern when dealing with epistemic reasoning in strategic settings. In particular, whereas logics in this area frequently leave strategies implicit in the semantic modelling, we propose to work in an instance of a standard semantic framework for temporal epistemic logic, but with strategies explicitly represented in the semantic model. In fact, we are not the first to have applied this instance of the standard temporalepistemic model (Halpern and O’Neill 2008). Our main innovation is small but, we claim, powerful: we introduce new agent names that refer to the strategies being used by the main players, and allow these new agent names to be included in (otherwise standard) operators for group knowledge. We argue that this gives a logical approach with broad applicability. In particular, it can express many of the subtly different notions that have been the subject of proposals for alternating temporal epistemic logics. We demonstrate this by results that show how such logics can be translated into our setting. We also present a number of other examples including reasoning about possible implementations of knowledge-based programs, game theoretic solution concepts, and issues of concern in computer security. Moreover, as we show, our approach retains from alternating temporal epistemic logic the desirable property that model checking is decidable, in the case of an imperfect recall semantics for knowledge. We show that it is in fact PSPACE-complete, no more than the complexity of model checking the temporal logic LTL, on which we build, although we have a much richer expressiveness. The structure of the paper is as follows. We first recall some standard definitions from temporal epistemic logic. We then present a semantic model (also standard) for the environments in which agents choose their actions. Build- The paper presents an extension of temporal epistemic logic that adds “strategic” agents in a way that allows standard epistemic operators to capture what agents could deduce from knowledge of the strategies of some subset of the set of agents. A number of examples are presented to demonstrate the broad applicability of the framework, including reasoning about implementations of knowledge-based programs, game theoretic solution concepts and notions from computer security. It is shown that notions from several variants of alternating temporal epistemic logic can be expressed. The framework is shown to have a decidable model checking problem.