Advertisement

A concurrent branching time temporal logic

  • Wojciech Penczek
Conference paper
Part of the Lecture Notes in Computer Science book series (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.

Keywords

Temporal Logic Proof System Atomic Proposition Interior Node Dynamic Logic 
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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [BMP81]
    Ben-Ari, M., Manna, Z., Pnueli, A., "The Temporal Logic of Branching Time", Acta Informatica 20, 207–226, (1983).CrossRefGoogle Scholar
  2. [EH85]
    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).CrossRefGoogle Scholar
  3. [EH86]
    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).CrossRefGoogle Scholar
  4. [FL79]
    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. [KP87]
    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. [KP88]
    Katz, S., Peled, D., "An Efficient Verification Method for Parallel and Distributed Programs", LNCS 354, (1988).Google Scholar
  7. [MOP89]
    Mazurkiewicz, A., Ochmański, E., Penczek, W., "Concurrent Systems and Inevitability", TCS 64, pp. 281–304, (1989).Google Scholar
  8. [MP88]
    Manna, Z., Pnueli, A., "The Anchored Version of the Temporal Framework", LNCS 354, (1988).Google Scholar
  9. [Pa85]
    Parikh, R., "The Logic of Games and its Applications", Annalsof Discrete Mathematics 24, pp. 111–140, (1985).Google Scholar
  10. [Pe87]
    Peleg, D., "Concurrent Dynamic Logic", Journal of the ACM 34 (2), pp. 450–479, (1987).Google Scholar
  11. [PW84]
    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. [Re88]
    Reisig, W., "Towards a Temporal Logic of Causality and Choice in Distributed Systems", LNCS 354, pp. 606–627 (1988).Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1990

Authors and Affiliations

  • Wojciech Penczek
    • 1
    • 2
  1. 1.Institute of Computer SciencePolish Academy of SciencesWarsaw, PKiNPoland
  2. 2.Department of Computing ScienceEindhoven University of TechnologyEindhovenThe Netherlands

Personalised recommendations