Compositional Properties of Sequential Processes

It is widely agreed that the modular method is one of the most effective methods to specify and verify complex systems in order to avoid combinatorial explosion. FLC ( Fixpoint Logic with Chop) is an important modal logic because of its expressivity and logic properties, e.g., it is strictly more expressive than the μ-calculus. In this paper, we study the compositionality of FLC, namely, to investigate the connection between the connectives of the logic and the constructors of programs. To this end, we first extend FLC with a nondeterministic operator “+” (FLC+ for the extension) and then establish a correspondence between the logic and the basic process algebra with deadlock and termination (abbreviated by BPAδε). Finally, we show that as a by-product of the correspondence characteristic formulae for processes of BPAδε up to strong (observational) bisimulation can be constructed compositionally directly from the syntax of processes.