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. © Springer-Verlag Berlin Heidelberg 2005.

Zhan N., Wu J.

702.pdf    Gửi cho bạn bè

Từ khóa : Algebra; Computer simulation; Computer system recovery; Large scale systems; Logic design; Basic process algebra; Bisimulation; Characteristic formula; Compositionality; FLC; Verification; Formal logic