Compositionality of Fixpoint Logic with Chop.

Compositionality plays an important role in designing reactive systems as it allows one to compose/decompose a complex system from/to several simpler components. Generally speaking, it is hard to design a complex system in a logical frame in a compositional way because it is difficult to find a connection between the structure of a system to be developed and that of its specification given by the logic. In this paper, we investigate the compositionality of the Fixpoint Logic with Chop (FLC for short). To this end, we extend FLC with the nondeterministic choice "+" (FLC+ for the extension) and then establish a correspondence between the logic and the basic process algebra with deadlock and termination (abbreviated BPAεδ). Subsequently, we show that the choice "+" is definable in FLC. As an application of the compositionality of FLC, an algorithm is given to construct characteristic formulae of BPAεδ up to strong bisimulation directly from the syntax of processes in a compositional manner. Keywords: FLC, compositionality, verification, bisimulation, characteristic formula, basic process algebra. [ABSTRACT FROM AUTHOR]