Axiom System Induced by CTL* Logic

Article type: Research Article

Authors: Koutny, Maciej

Affiliations: Computing Laboratory, The University of Newcastle upon Tyne, Newcastle upon Tyne NE1 7RU, UK

Abstract: We discuss some of the problems concerning bisimulation relations over behaviour expressions representing non-sequential systems. The kind of bisimulation we investigate is derived from the notion of bisimulation relation between two Kripke structures, which provides a full characterisation of semantical equivalence of such structures w.r.t. the CTL* branching time temporal logic without the next-time operator. This new bisimulation on behaviour expressions, called CTL*-bisimulation, induces a congruence on recursion-free behaviour expressions, and in this paper we derive a sound and complete axiom system for this congruence.

DOI: 10.3233/FI-1991-14205

Journal: Fundamenta Informaticae, vol. 14, no. 2, pp. 235-253, 1991