Parallel action: Concurrent dynamic logic with independent modalities (Q1207436)

Regular dynamic logic is extended by the program construct \(\alpha\cap\beta\), meaning ``\(\alpha\) and \(\beta\) executed in parallel''. In a semantics due to Peleg, each program \(\alpha\) is interpreted as a relation \(R_ \alpha\) on a set of pairs \((s,T)\), with \(s\in S\) and \(T\subseteq S\), where \(S\) is the set of states and \(T\) is the set of states reachable from the state \(s\) by a single execution of \(\alpha\), possibly involving several processes acting in parallel. The modalities \(\langle \alpha\rangle\) and \([\alpha]\) are given as follows: \[ \begin{aligned} \langle \alpha\rangle A &\text{ is true at } s\text{ iff there exists } T\text{ with } sR_ \alpha T\text{ and }A\text{ true throughout }T,\quad \text{and}\\ [\alpha]A &\text{ is true at }s\text{ iff for all }T,\;\text{if }sR_ \alpha T\text{ then }A\text{ is true throughout } T,\end{aligned} \] which make \(\langle \alpha\rangle\) and \([\alpha]\) no longer interdefinable via negation. It is proved that the logic defined in this modeling is finitely axiomatizable and has the finite model property, hence is decidable. This requires the development of a new theory of canonical models and filtrations for ``reachability'' relations.