Home  Online Resources  Table of Contents

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

1Computer Science Department, The Technion, Haifa 32000, Israel. E-mail: orna@cs.technion.ac.il
2Bell Laboratories, Murray Hill, NJ 07974, USA. E-mail: k@research.bell-labs.com

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

  Full-Text PDF  (315 KB)


[ Oxford University Press]   [ Oxford Journals]   [ Comments & Feedback]   Copyright© Oxford University Press, 2001.