Skip to main content
SpringerLink
Log in

An expressive logic for Basic Process Algebra

  • Conference paper
  • First Online:
Mathematical Foundations of Computer Science 1993 (MFCS 1993)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 711))

  • 188 Accesses

Abstract

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.

The third author contributed to the paper when she was a student at University of Pisa

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  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. 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. 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. 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. J. A. Bergstra & J. W. Klop: Process theory based on bisimulation semantics. LNCS 354, pp. 50–122, 1988.

    Google Scholar 

  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. O. Burkart, B. Steffen: Model Checking for Context-Free Processes. Proceedings CONCUR 92, LNCS 630, pp.123–137, 1992.

    Google Scholar 

  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. 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. A. Fantechi, S. Gnesi, G. Ristori: Compositionality and Bisimulation: a Negative Result. Information Processing Letters, vol. 39, pp. 109–114, 1991.

    Google Scholar 

  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. 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. M. Hennessy: Algebraic Theory of Processes.MIT Press, Cambridge, 1988.

    Google Scholar 

  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. 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. D. Kozen: Results on the Propositional μ-calculus. Theor. Comp. Sci. vol. 27, pp. 333–354, 1983.

    Google Scholar 

  17. R. Milner: A calculus of communicating system. LNCS 92, 1980.

    Google Scholar 

  18. D. M. R. Park: Concurrency and automata on infinite sequences. Proc. 5th GI Conference, LNCS 104, pp. 167–183 1981.

    Google Scholar 

  19. A. Pnueli: The Temporal Semantics of Concurrent Programs Theor. Comp. Sci., vol.13, 1981, pp.45–60.

    Google Scholar 

  20. A. Pnueli: Linear and Branching Structures in the Semantics and Logic of Reactive Systems. Proc. 12th ICALP, LNCS 194, 1985.

    Google Scholar 

  21. B. Steffen: Characteristic Formulae. Proc. 16th ICALP, LNCS 372, pp.723–732, 1989.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Dipatrtimento di Ingegneria dell'Informazione, Università di Pisa, Italy

    A. Fantechi

  2. IEI-CNR, Pisa, Italy

    S. Gnesi

  3. SIP, Bologna, Italy

    V. Perticaroli

Authors
  1. A. Fantechi
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. S. Gnesi
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. V. Perticaroli
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Andrzej M. Borzyszkowski Stefan Sokołowski

Rights and permissions

Reprints and permissions

Copyright information

© 1993 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Fantechi, A., Gnesi, S., Perticaroli, V. (1993). An expressive logic for Basic Process Algebra. In: Borzyszkowski, A.M., Sokołowski, S. (eds) Mathematical Foundations of Computer Science 1993. MFCS 1993. Lecture Notes in Computer Science, vol 711. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-57182-5_37

Download citation

  • DOI: https://doi.org/10.1007/3-540-57182-5_37

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-57182-7

  • Online ISBN: 978-3-540-47927-7

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation