O(N³) Algorithm for Bisimulation Equivalence w.r.t CTL* without the Next-Time Operator between Kripke Structures

Concurrent systems are often modeled by labeled state--transition graphs called Kripke Structures [5]. To reason about such systems, one standard approach is to provide a temporal semantic for the structure. Properties of interest regarding concurrency can then be expressed using a temporal logic formula. In this paper we consider the following problem: Given a Kripke structure, determine for all pairs of states s and s 0 whether they are equivalent with respect to CTL =X (i.e. s and s 0 model the same set of formulas in CTL =X). CTL [3], a new logic, incorporates the features of both Linear Temporal Logic and Branching Temporal Logic. In Logic CTL =X, the nexttime operator is discarded, since if this operator is used indiscriminately, it can lead to a "misleading" specification of a concurrent property [6, 5]. In [5], an O(N 5 ) algorithm is presented for the all state pairs equivalence problem, where N the number of states in the structure. The primary contributio..