SVV Preliminary Version Compositional Properties of Sequential Processes

It is widely agreed that the modular method is one of the most eective 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 rst 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. Key words: chop operator, modal logic, compositionality, veri cation, bisimulation, characteristic formula, process algebra