Journal of Logic and Computation, Volume 11, Issue 2, pp. 201-228: Abstract.
Which Branching-Time Properties are Effectively Linear?
Orna Grumberg1, and Robert P. Kurshan2
We characterize three successively more restrictive classes of `effectively linear' CTL* formulas, with and without fairness: the equi-linear formulas, which do not distinguish among models with the same language, the sub-linear formulas, which are preserved under model language inclusion and the strong linear formulas, which are characterized by a given [omega]-regular language. Moreover, strong linearity characterizes those CTL* formulas equivalent to LTL formulas. This taxonomy helps to clarify the expressive distinctions between CTL*, LTL and [omega]-regular languages. It has also practical implications. Verification tools based on language inclusion can handle any CTL* formula which is equi-linear, for purposes of model checking, and sub-linear for purposes of abstraction. Furthermore, minimization techniques that preserve the subset of CTL* which consists of only effectively linear formulas, result in smaller structures than bisimulation minimization.
Keywords: Temporal logic, linear temporal logic, branching temporal logic, fairness, characterization