Which Branching-Time Properties are Effectively Linear?

摘要

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 character- ized by a given ω-regular language. Moreover, strong linearity characterizes those CTL~* formulas equivalent to LTL formulas.