A concurrent branching time temporal logic
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.
KeywordsTemporal Logic Proof System Atomic Proposition Interior Node Dynamic Logic
Unable to display preview. Download preview PDF.
- [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
- [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
- [KP88]Katz, S., Peled, D., "An Efficient Verification Method for Parallel and Distributed Programs", LNCS 354, (1988).Google Scholar
- [MOP89]Mazurkiewicz, A., Ochmański, E., Penczek, W., "Concurrent Systems and Inevitability", TCS 64, pp. 281–304, (1989).Google Scholar
- [MP88]Manna, Z., Pnueli, A., "The Anchored Version of the Temporal Framework", LNCS 354, (1988).Google Scholar
- [Pa85]Parikh, R., "The Logic of Games and its Applications", Annalsof Discrete Mathematics 24, pp. 111–140, (1985).Google Scholar
- [Pe87]Peleg, D., "Concurrent Dynamic Logic", Journal of the ACM 34 (2), pp. 450–479, (1987).Google Scholar
- [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
- [Re88]Reisig, W., "Towards a Temporal Logic of Causality and Choice in Distributed Systems", LNCS 354, pp. 606–627 (1988).Google Scholar