Skip to main content
SpringerLink
Log in
Book cover

International Workshop on Computer Science Logic

CSL 1989: CSL '89 pp 337–354Cite as

A concurrent branching time temporal logic

  • Conference paper
  • First Online:

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

Abstract

In this paper we show that a computation tree logic (CTL) can be very naturally extended to distinguish concurrency from non — determinism by using a frame of the form (S,R), where\(R \subseteq S \times 2^S\). We call a new logic a concurrent computation tree logic (CCTL) and we prove that CCTL is finitely axiomatizable, decidable and it has the finite model property. We also show that CCTL contains CTL and moreover, new important properties for concurrent systems can be expressed in CCTL.

This paper was partly supported by the Warsaw University and the Netherlands NWO NF 3/62 — 500 & NF 64/62 — 519.

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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Ben-Ari, M., Manna, Z., Pnueli, A., "The Temporal Logic of Branching Time", Acta Informatica 20, 207–226, (1983).

    Article  Google Scholar 

  2. Emerson, E.A., Halpern, J.Y., "Decision Procedures and Expressiveness in the Temporal Logic of Branching Time", Journal of Computer and System Sciences 30, 1–24, (1985).

    Article  Google Scholar 

  3. Emerson, E.A., Halpern, J.Y., "“Sometimes” and “Not Never” Revisited: On Branching versus Linear Time Temporal Logic", Journal of the ACM 33 (1), pp. 151–178, (1986).

    Article  Google Scholar 

  4. Fischer, M.J., Ladner, R.E., "Propositional Dynamic Logic of Regular Programs", J. of Comput. System Sci. 18(2), pp. 194–211, (1979).

    Google Scholar 

  5. Katz, S., Peled, D., "An Interleaving Set Temporal Logics", Proc. of 6th ACM Symposium on Principles of Distributed Computing, Vancouver Canada, pp. 178–190, (1987).

    Google Scholar 

  6. Katz, S., Peled, D., "An Efficient Verification Method for Parallel and Distributed Programs", LNCS 354, (1988).

    Google Scholar 

  7. Mazurkiewicz, A., Ochmański, E., Penczek, W., "Concurrent Systems and Inevitability", TCS 64, pp. 281–304, (1989).

    Google Scholar 

  8. Manna, Z., Pnueli, A., "The Anchored Version of the Temporal Framework", LNCS 354, (1988).

    Google Scholar 

  9. Parikh, R., "The Logic of Games and its Applications", Annalsof Discrete Mathematics 24, pp. 111–140, (1985).

    Google Scholar 

  10. Peleg, D., "Concurrent Dynamic Logic", Journal of the ACM 34 (2), pp. 450–479, (1987).

    Google Scholar 

  11. Pinter, S.S., Wolper, P., "A Temporal Logic for Reasoning about Partially Ordered Computations", Proc. 3rd Symp. on Principles of Distributed Computing, pp. 28–37, Vancouver (1984).

    Google Scholar 

  12. Reisig, W., "Towards a Temporal Logic of Causality and Choice in Distributed Systems", LNCS 354, pp. 606–627 (1988).

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institute of Computer Science, Polish Academy of Sciences, P.O. Box 22, 00-901, Warsaw, PKiN, Poland

    Wojciech Penczek

  2. Department of Computing Science, Eindhoven University of Technology, Den Dolech 2, P.O. Box 513, 5600 MB, Eindhoven, The Netherlands

    Wojciech Penczek

Authors
  1. Wojciech Penczek
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Egon Börger Hans Kleine Büning Michael M. Richter

Rights and permissions

Reprints and permissions

Copyright information

© 1990 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Penczek, W. (1990). A concurrent branching time temporal logic. In: Börger, E., Büning, H.K., Richter, M.M. (eds) CSL '89. CSL 1989. Lecture Notes in Computer Science, vol 440. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-52753-2_49

Download citation

  • DOI: https://doi.org/10.1007/3-540-52753-2_49

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-52753-4

  • Online ISBN: 978-3-540-47137-0

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation