Compositionality of fixpoint logic with chop

Abstract. Compositionality plays an important role in designing reac-tive systems as it allows one to compose/decompose a complex system from/to several simpler components. Generally speaking, it is hard to de-sign 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 pa-per, 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 termi-nation (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