Multi-modal CTL: completeness, complexity, and an application (Q1037587)

The authors introduce MCLT, or Multi-Modal CTL, a generalization of CTL (Computation Tree Logic), using a set \(\Delta\) of indices to let the modal operators \(E^\delta\) and \(A^\delta\), \(\delta\in\Delta\), take the place of the modal operators \(E\) and \(A\) of CTL. Intuitively, every member of \(\delta\) is associated with an agent. A formula of the form \(E^\delta\phi\) then expresses that agent \(\delta\) can act in such a way that \(\phi\) holds, whereas a formula of the form \(A^\delta\phi\) expresses that \(\phi\) is true irrespective of how agent \(\delta\) acts. The tense operators are the same in MCLT as in CTL: \(\phi_1\mathcal U\phi_2\) expresses that \(\phi_1\) holds till some state where \(\phi_2\) holds, and \(\bigcirc\phi\) expresses that \(\phi\) holds in the next state. The classical axiomatization of CTL is generalized to an axiomatization of MCTL by replacing every axiom with an axiom for every \(\delta\in\Delta\), where all occurrences of \(E\) and \(A\) are replaced by \(E^\delta\) and \(A^\delta\), respectively. That axiomatization is shown to be complete, and the satisfiability problem EXPTIME-complete, similarly to CTL. Before giving the formal proof, the authors provide the main intuitions and illustrate them with an example. Essentially, to prove the satisfiabiltity of a given formula \(\phi\) of the form \(E^\delta\psi\) or \(A^\delta\psi\), all subformulas of \(\phi\) of the form \(E^{\delta'}\psi\) and \(A^{\delta'}\psi\) are replaced by extra propositional letters, resulting in a formula \(\widetilde{\phi}\). The completeness result of CLT then provides a model of \(\widetilde{\phi}\) (where the index \(\delta\) is ignored) each of whose states is labelled with the propositional letters that have been introduced and that have to be true in that state. Then the procedure is applied recursively to each state \(s\) and each formula of the form \(E^{\delta'}\psi\) or \(A^{\delta'}\psi\) associated with that state, giving a model that can be glued to \(s\), in particular thanks to a normal form that allows one to have every occurrence of \(E^\delta(\phi_1\mathcal U\phi_2)\) or \(A^\delta(\phi_1\mathcal U\phi_2)\) in a formula be preceded with \(E^\delta\bigcirc\) or \(A^\delta\bigcirc\), respectively. In the last part of the paper, the authors discuss normative systems that impose constraints on the behavior of agents in a system. They indicate that the language of MCTL can be redesigned and reinterpreted, with \(P^\eta\phi\) instead of \(E^\eta\phi\) to express that the norm \(\eta\) is permitted, and with \(O^\eta\phi\) instead of \(A^\eta\phi\) to express that the norm \(\eta\) is obligatory. They discuss a special norm \(\eta_0\) such that \(E^\eta_0\) captures what is physically possible and \(A^\eta_0\) what is physically inevitable, together with a couple of axioms that express that what is permitted under a norm is physically possible, and what is physically inevitable is obligatory under a norm. They illustrate these concepts with an example where trains coming from opposite directions have to go through a tunnel and avoid crashing, with two norms taking care of the behaviour of traffic lights at both ends of the tunnel, and the presence of absence of a train in the tunnel. They conclude with comparisons with other approaches.