Modal logics for communicating systems (Q578896)

This very interesting paper, which is a generalization of the author's [Lect. Notes Comput. Sci. 194, 475-486 (1985; Zbl 0584.68028)], consists of two major parts. Part one discusses transition systems, bisimulation, their modal characterizations and sound are complete axiomatizations of these: classical Hennessy-Milner logic characterizes bisimulation equivalence, intuitionistic Hennessy-Milner logic does the same for partial bisimulation preorder on finitely branching transition systems. Part two is concerned with compositional modal proof systems for SCCS and CCS, and their soundness and (weak) completeness. These systems contain Gentzen-like introductions rules, including those for the program combinators of (S)CCS. The compositional rules for the parallel operators and restriction (hiding) are inspired by an idea from temporal logic literature (viz. [\textit{H. Barringer}, \textit{R. Kuiper} and \textit{A. Pnueli}, Proc. ACM Symp. on Theory of Computing, 51-63 (1984)]), where a compositional temporal logic for the specification of parallel programs is proposed. The basic idea is to extend the Hennessy-Milner language in order to cope with ``environments''.