ePrints

Axiom System Induced by CTL Logic

Lookup NU author(s): Professor Maciej KoutnyORCiD

Downloads

• Published version [.pdf]

Abstract

We discuss some of the problems conerning bisimulation relations over behaviour expressions representing non-sequential systems. The kind of bisimulation we investigate is derived from the notion of bisimulation relation betwenn 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.

Publication metadata

Author(s): Koutny M

Publication type: Report

Publication status: Published

Series Title: Computing Laboratory Technical Report Series

Year: 1990

Pages: 26

Print publication date: 01/06/1990

Source Publication Date: June 1990

Report Number: 313

Institution: Computing Laboratory, University of Newcastle upon Tyne

Place Published: Newcastle upon Tyne

URL: http://www.cs.ncl.ac.uk/publications/trs/papers/313.pdf

Share