The situation calculus: a case for modal logic (Q616039)

The paper starts with a reminder on Reiter's situation calculus and basic action theories, illustrated with blocks-world examples. Knowledge can be expressed by introducing a special binary predicate \(K\) -- the intended interpretation of \(K(s',s)\) being ``situation \(s'\) is (epistemically) accessible from situation \(s\)'', which allows one to formalise knowledge of \(\phi\) in situation \(s\) as \(\forall s'.K(s',s)\supset\phi[s']\) --, not requesting that there be a unique initial situation, and adding a successor state axiom expressing that the situations which are accessible after doing an action are the successors of the situations which are accessible before doing the action and in which the action can be performed. Time can be modelled either by adding a new kind of individuals, or by making use of the implicit temporal structure of the tree of situations; both approaches are sketched, and the limitations emphasised, for instance, their inability to express that there is a path such that eventually \(\phi\) becomes true on this path. These considerations support the proposal for a modal language, less fine-grained in that it does not give access to situations, but expressive enough and allowing one to embed temporal aspects in a style similar to existing temporal logic. In the second part of the paper, such a modal language, \(\mathcal{E\!S}\), is introduced. It contains formulas of the form Know\((\alpha)\), \(\square\alpha\) to express that ``\(\alpha\) holds after any sequence of actions'', and \([t]\alpha\) to express that ``\(\alpha\) holds after action \(t\)''. A classical Kripke semantics is presented. More precisely, defining an epistemic state as a subset of the set of worlds \(W\), and denoting by \(\mathcal Z\) the set of finite sequences of standard action names, the semantics determines whether or not \(e,w,z\models\phi\) holds for \(e\subseteq W\), \(w\in W\), and \(z\in\mathcal Z\). The key clauses are: \(e,w,z\models\text{Know}(\alpha)\) if \(e,w',z\models\alpha\) for all members \(w'\) of \(e\) that agree with \(w\) on the interpretation of all primitive rigid terms (a particular kind of terms); \(e,w,z\models\square\alpha\) if \(e,w,z\cdot z'\models\alpha\) for every \(z'\in\mathcal Z\); \(e,w,z\models[t]\alpha\) if \(e,w,z\cdot n\models\alpha\) where \(n\) is a standard name for the interpretation of \(t\) in \(w\). The usual properties of knowledge in weak S5 or K45 are proved to hold. It is shown with a one-line proof that if \(\alpha\) and \(\beta\) are formulas with no occurrence of Know and \(\models\alpha\supset\beta\), then \(\models\text{ Know}(\alpha)\supset\text{ Know}(\beta)\), a result which ``in the original calculus, requires a complicated multi-page argument involving Craig's interpolation lemma''. Then the connection is made with Reiter's situation calculus, thanks to a translation that maps the ``situation-suppressed'' formulas of \(\mathcal{E\!S}\) into formulas of that calculus. An appropriate set of axioms is introduced before the statement of the key ``embedding theorem'', according to which for every basic sentence \(\alpha\) of \(\mathcal{E\!S}\) without standard names, \(\alpha\) is valid iff \(\alpha\)'s translation is a logical consequence of those axioms together with Reiter's set of foundational axioms (it is observed that the latter can actually be replaced by a weaker set of axioms). In the last part of the paper, it is shown how to integrate branching time into \(\mathcal{E\!S}\), by introducing new modal operators, and in particular a path quantifier \(\mathbb E\). The semantics then determines whether or not \(e,w,z,\pi\models\phi\) holds for \(e\), \(w\) and \(z\) as before and \(\pi\) a path. In the extended language, one can formalise for instance that ``there is a path such that whenever an object is on the table, then it will be on the floor some time after that'' as \[ \mathbb{E}(\forall x.\mathbb{G}(\text{OnTable}(x)\supset\mathbb{F}\text{OnFloor}(x))). \]