Journal of the Association for Computing Machinery, Vol. 42, No. 2, March 1995, pp. 458–487.

Three Logics for Branching Bisimulation

ROCCO DE NICOLA

AND

FRITS VAANDRAGER

Abstract. Three temporal logics are introduced that induce on labeled transition systems the same identifications as branching bisimulation, a behavioral equivalence that aims at ignoring invisible transitions while preserving the branching structure of systems. The first logic is an extension of Hennessy-Milner Logic with an “until” operator. The second one is another extension of Hennessy-Milner Logic, which exploits the power of backward modalities. The third logic is CTL* without the next-time operator. A relevant side-effect of the last characterization is that it sets a bridge between the state- and action-based approaches to the semantics of concurrent systems.

Categories and Subject Descriptors. F.1.1, F.3.1

General Terms. Theory, verification

Additional Key words and Phrases. Backward modalities, branching bisimulation equivalence, concurrency, CTL*, doubly labeled transition systems, Hennessy-Milner logic, Kripke structures, labeled transition systems, reactive systems, semantics, stuttering equivalence, until operations

Copyright 1995 by ACM, Inc. Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or direct commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, to republish, to post on servers, or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from Publications Dept, ACM Inc., fax +1 (212) 869-0481, or permissions@acm.org.