Which Branching-Time Properties are Effectively Linear?
O. Grumberg · Journal of Logic and Computation · 2001
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 ω‐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 ω‐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.