Compositionality of Fixpoint Logic with Chop

  • Naijun Zhan
  • Jinzhao Wu
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3722)


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\(^{\epsilon}_{\delta}\)). 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\(^{\epsilon}_{\delta}\) up to strong bisimulation directly from the syntax of processes in a compositional manner.


FLC compositionality verification bisimulation characteristic formula basic process algebra 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Aceto, L., Hennessy, M.: Termination, deadlock, and divergence. Journal of ACM 39(1), 147–187 (1992)zbMATHCrossRefMathSciNetGoogle Scholar
  2. 2.
    Andersen, H.R., Stirling, C., Winskel, G.: A compositional proof system for the modal mu-Calculus. In: LICS 1994, pp. 144–153 (1994)Google Scholar
  3. 3.
    Barringer, H., Kuiper, R., Pnueli, A.: Now you compose temporal logic specifications. In: Proc. 16th STOC, may 1984, pp. 51–63 (1984)Google Scholar
  4. 4.
    Barringer, H., Kuiper, R., Pnueli, A.: A compositional temporal approach to a CSP-like language. In: Proc. IFIP conference, The Role of Abstract Models in Information Processing, pp. 207–227 (1985)Google Scholar
  5. 5.
    Bergstra, J.A., Klop, J.W.: Algebra of communication processes with abstraction. Theoretical Computer Science 37, 77–121 (1985)zbMATHCrossRefMathSciNetGoogle Scholar
  6. 6.
    Chandra, A., Halpern, J., Meyer, A., Parikh, R.: Equations between regular terms and an application to process logic. In: Proc. 13th STOC, pp. 384–390 (1981)Google Scholar
  7. 7.
    Dutertre, B.: On first order interval logic. In: LICS 1995, pp. 36–43 (1995)Google Scholar
  8. 8.
    Emerson, E.A., Jutla, C.S.: Tree automata, μ-calculus, and determinacy. In: Proc. 33rd FOCS, pp. 368–377 (1991)Google Scholar
  9. 9.
    Graf, S., Sifakis, J.: A modal characterization of observational congruence on finite terms of CCS. Information and Control 68, 125–145 (1986)zbMATHCrossRefMathSciNetGoogle Scholar
  10. 10.
    Graf, S., Sifakis, J.: A logic for the description of non-deterministic programs and their properties. Information and Control 68, 254–270 (1986)zbMATHCrossRefMathSciNetGoogle Scholar
  11. 11.
    Halpern, J., Moskowski, B., Manna, Z.: A hardware semantics based on temporal intervals. In: Díaz, J. (ed.) ICALP 1983. LNCS, vol. 154, pp. 278–291. Springer, Heidelberg (1983)CrossRefGoogle Scholar
  12. 12.
    Harel, D., Kozen, D., Parikh, R.: Process Logic: Expressiveness, decidability, completeness. In: IEEE FOCS 1980, pp. 129–142 (1980)Google Scholar
  13. 13.
    Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1985)zbMATHGoogle Scholar
  14. 14.
    Janin, D., Walukiewicz, I.: On the expressive completeness of the propositional μ-calculus with respect to monadic second order logic. In: Sassone, V., Montanari, U. (eds.) CONCUR 1996. LNCS, vol. 1119, pp. 263–277. Springer, Heidelberg (1996)Google Scholar
  15. 15.
    Kozen, D.: Results on the propositional mu-calculus. Theoretical Computer Science 27, 333–354 (1983)zbMATHCrossRefMathSciNetGoogle Scholar
  16. 16.
    Lange, M., Stirling, C.: Model checking fixed point logic with chop. In: Nielsen, M., Engberg, U. (eds.) FOSSACS 2002. LNCS, vol. 2303, pp. 250–263. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  17. 17.
    Lange, M.: Local model checking games for fixed point logic with chop. In: Brim, L., Jančar, P., Křetínský, M., Kucera, A. (eds.) CONCUR 2002. LNCS, vol. 2421, pp. 240–254. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  18. 18.
    Larsen, K.G., Thomsen, B.: A modal process logic. In: The proc. of LICS 1988, pp. 203–210 (1988)Google Scholar
  19. 19.
    Larsen, K.G., Liu, X.X.: Compositionality through an operational semantics of contexts. In: Paterson, M. (ed.) ICALP 1990. LNCS, vol. 443, pp. 526–539. Springer, Heidelberg (1990)CrossRefGoogle Scholar
  20. 20.
    Larsen, K.G., Liu, X.X.: Equation solving using modal transition systems. In: LICS 1990, pp. 108–107 (1990)Google Scholar
  21. 21.
    Müller-Olm, M.: A modal fixpoint logic with chop. In: Meinel, C., Tison, S. (eds.) STACS 1999. LNCS, vol. 1563, pp. 510–520. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  22. 22.
    Milner, R.: Communication and Concurrency. Prentice Hall, Englewood Cliffs (1989)zbMATHGoogle Scholar
  23. 23.
    Pnueli, A.: The temporal logic of programs. In: Proc. 18th STOC, pp. 232–239 (1977)Google Scholar
  24. 24.
    Rosner, R., Pnueli, A.: A choppy logic. In: The proc. of LICS 1986, pp. 306–313 (1986)Google Scholar
  25. 25.
    Steffen, B., Ingólfsdóttir, A.: Characteristic formulae for processes with divergence. Information and Computation 110, 149–163 (1994)zbMATHCrossRefMathSciNetGoogle Scholar
  26. 26.
    Viswanathan, M., Viswanathan, R.: Foundations for circular compositional reasoning. In: Orejas, F., Spirakis, P.G., van Leeuwen, J. (eds.) ICALP 2001. LNCS, vol. 2076, pp. 835–847. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  27. 27.
    Zhan, N.: Compositional properties of sequential processes. In: The proc. of SVV 2003. ENTCS, vol. 118, pp. 111–128 (2005)Google Scholar
  28. 28.
    Zhou, C.C., Hoare, C.A.R., Ravn, A.: A calculus of durations. Information Processing Letters 40(5), 269–276 (1991)zbMATHCrossRefMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Naijun Zhan
    • 1
  • Jinzhao Wu
    • 2
  1. 1.Lab. of Computer Science, Institute of SoftwareChinese Academy of SciencesBeijingP.R. China
  2. 2.Lehrstuhl für Praktische Informatik II, Fakultät für Mathematik und InformatikUniversität MannheimMannheim

Personalised recommendations