An expressive logic for Basic Process Algebra

  • A. Fantechi
  • S. Gnesi
  • V. Perticaroli
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 711)


In this paper we present a branching time temporal logic for Basic Process Algebra. This logic is an enrichment of the branching temporal logic CTL with a branching sequential composition operator, named chop branching. The logic so obtained is proved to be expressive with respect to the bisimulation semantics defined on BPAδ, rec terms, and is able to describe context-free properties of systems.


Temporal Logic Operational Semantic Linear Temporal Logic Sequential Composition Logic Formula 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    J. C. M. Baeten, J. A. Bergstra, J. W. Klop: Decidibility of bisimulation equivalence for processes generating context-free languages. Tech. Rep. CS-R8632, CWI, 1987.Google Scholar
  2. 2.
    B. Banieqbal, H. Barringer: Temporal Logic Fixed Point Calculus. Proc. Colloquium on Temporal Logic and Specification, LNCS 398, pp. 62–74, 1989.Google Scholar
  3. 3.
    H. Barringer, R. Kuiper, A. Pnueli: Now You May Compose Temporal Logic Specifications. Proceedings 16th ACM Symposium on the Theory of Computing, 1984.Google Scholar
  4. 4.
    J. A. Bergstra, J. W. Klop: Process algebra: specification and verification in bisimulation semantics. In: CWI Monograph 4, Proc. of the CWI Symposium Mathematics and Computer Science II, North-Holland, pp. 61–94, Amsterdam 1986.Google Scholar
  5. 5.
    J. A. Bergstra & J. W. Klop: Process theory based on bisimulation semantics. LNCS 354, pp. 50–122, 1988.Google Scholar
  6. 6.
    M. C. Browne, E. M. Clarke, O. Grümberg: Characterizing Finite Kripke Structures in Propositional Temporal Logic. Theor. Comp. Sci. vol. 59, pp. 115–131, 1988.Google Scholar
  7. 7.
    O. Burkart, B. Steffen: Model Checking for Context-Free Processes. Proceedings CONCUR 92, LNCS 630, pp.123–137, 1992.Google Scholar
  8. 8.
    E. A. Emerson, J. Y. Halpern: “Sometimes” and “Not Never” Rivisited: On Branching versus Linear Time Temporal Logic. Journal of ACM vol. 33, pp.151–178, 1986.Google Scholar
  9. 9.
    E. A. Emerson, C. Lei: Efficient Model Checking in Fragments of the Propositional Mu-Calculus, Proc. Symposium on Logics in Computer Science, 1986, pp. 267–278.Google Scholar
  10. 10.
    A. Fantechi, S. Gnesi, G. Ristori: Compositionality and Bisimulation: a Negative Result. Information Processing Letters, vol. 39, pp. 109–114, 1991.Google Scholar
  11. 11.
    S. Graf, J, Sifakis: A Logic for Specification and Proof of Regular Controllable Processes of CCS. Acta Informatica, vol 23, pp. 507–527, 1986.Google Scholar
  12. 12.
    J. F. Groote, F. W. Vaandrager: Structured Operational Semantics and Bisimulation as a Congruence. Proc. 16th ICALP, LNCS 372, pp.423–438, 1989.Google Scholar
  13. 13.
    M. Hennessy: Algebraic Theory of Processes.MIT Press, Cambridge, 1988.Google Scholar
  14. 14.
    H. Hüttel, C. Stirling: Actions Speak Louder than Words: Proving Bisimilarity of Context-Free Processes. Proc. LICS 91, Computer Society Press, 1991.Google Scholar
  15. 15.
    B. Jonsson, H. Khan, J. Parrow: Implementing a Model Checking Algorithm by Adapting Existing Automated Tools. In: Automatic Verification Methods for Finite State Systems, LNCS 407, pp. 179–188, 1990.Google Scholar
  16. 16.
    D. Kozen: Results on the Propositional μ-calculus. Theor. Comp. Sci. vol. 27, pp. 333–354, 1983.Google Scholar
  17. 17.
    R. Milner: A calculus of communicating system. LNCS 92, 1980.Google Scholar
  18. 18.
    D. M. R. Park: Concurrency and automata on infinite sequences. Proc. 5th GI Conference, LNCS 104, pp. 167–183 1981.Google Scholar
  19. 19.
    A. Pnueli: The Temporal Semantics of Concurrent Programs Theor. Comp. Sci., vol.13, 1981, pp.45–60.Google Scholar
  20. 20.
    A. Pnueli: Linear and Branching Structures in the Semantics and Logic of Reactive Systems. Proc. 12th ICALP, LNCS 194, 1985.Google Scholar
  21. 21.
    B. Steffen: Characteristic Formulae. Proc. 16th ICALP, LNCS 372, pp.723–732, 1989.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1993

Authors and Affiliations

  • A. Fantechi
    • 1
  • S. Gnesi
    • 2
  • V. Perticaroli
    • 3
  1. 1.Dipatrtimento di Ingegneria dell'InformazioneUniversità di PisaItaly
  2. 2.IEI-CNRPisaItaly
  3. 3.SIPBolognaItaly

Personalised recommendations