Journal of Logic and Computation, Volume 11, Issue 2, pp. 201228: Abstract.
Which BranchingTime Properties are Effectively Linear?Orna Grumberg^{1}, and Robert P. Kurshan^{2}
^{1}Computer Science Department, The Technion, Haifa 32000, Israel. Email: orna@cs.technion.ac.il
We characterize three successively more restrictive classes of `effectively linear' CTL* formulas, with and without fairness: the equilinear formulas, which do not distinguish among models with the same language, the sublinear 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 equilinear, for purposes of model checking, and sublinear 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
