Computation Tree Logic with Deadlock Detection

Details Computation Tree Logic with Deadlock Detection Computation Tree Logic with Deadlock Detection

2009-12-10

arxiv.org/abs/0912.2109v2

LMCS 5 (4:5) 2009

Computer Science

Logic in Computer Science

Scientific paper

10.2168/LMCS-5(4:5)2009

We study the equivalence relation on states of labelled transition systems of satisfying the same formulas in Computation Tree Logic without the next state modality (CTL-X). This relation is obtained by De Nicola & Vaandrager by translating labelled transition systems to Kripke structures, while lifting the totality restriction on the latter. They characterised it as divergence sensitive branching bisimulation equivalence. We find that this equivalence fails to be a congruence for interleaving parallel composition. The reason is that the proposed application of CTL-X to non-total Kripke structures lacks the expressiveness to cope with deadlock properties that are important in the context of parallel composition. We propose an extension of CTL-X, or an alternative treatment of non-totality, that fills this hiatus. The equivalence induced by our extension is characterised as branching bisimulation equivalence with explicit divergence, which is, moreover, shown to be the coarsest congruence contained in divergence sensitive branching bisimulation equivalence.

Affiliated with

Also associated with

No associations

Rating

Computation Tree Logic with Deadlock Detection does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with Computation Tree Logic with Deadlock Detection, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Computation Tree Logic with Deadlock Detection will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-467515