The Common Fragment of ACTL and LTL
The paper explores the relationship between tree languages definable in LTL, CTL, and ACTL, the fragment of CTL where only universal path quantification is allowed. The common fragment of LTL and ACTL is shown to be strictly smaller than the common fragme
- PDF / 215,952 Bytes
- 14 Pages / 430 x 660 pts Page_size
- 92 Downloads / 211 Views
Abstract. The paper explores the relationship between tree languages definable in LTL, CTL, and ACTL, the fragment of CTL where only universal path quantification is allowed. The common fragment of LTL and ACTL is shown to be strictly smaller than the common fragment of LTL and CTL. Furthermore, an algorithm is presented for deciding if an LTL formula can be expressed in ACTL. This algorithm uses an effective characterization of level 3/2 of the concatenation hierarchy for infinite words, also a new result.
Two of the most commonly used logics in verification are LTL and CTL. The first is a linear time logic, a formula of LTL describes a property of words. To describe properties of trees, one applies universal path quantification: an LTL formula is valid in a tree if it is valid in all paths. CTL, on the other hand, is a branching time logic. A formula of CTL refers explicitly to the branching in the tree, by using both universal and existential path quantification. What is the relationship between the two logics? Which LTL definable properties can be defined in CTL, and which CTL definable properties can be defined in LTL? In other words, what is the common fragment of CTL and LTL? There is a well known algorithm, which given an automaton on infinite trees, determines if its language can be defined in LTL (basically, a tree constructed by mixing paths of different trees accepted by the automaton, must still be accepted by the automaton; furthermore, the appropriate word language must be aperiodic). For tree languages defined in CTL* there is also a simple characterization of Clarke and Draghilescu: a CTL* formula is equivalent to an LTL formula, if and only if it is equivalent to the one obtained by removing the path quantifiers [3]. Maidl [6] has shown that if the input is given as a CTL formula, then problem of LTL definability becomes PSPACE complete. The converse question, however, remains an open problem: is it decidable if a given LTL formula can be equivalently written as a CTL formula? A second, more general, problem is to decide if an arbitrary regular language of infinite trees can be defined in CTL. It seems a good idea to begin with the first problem before tackling the second one. If an LTL formula with universal path semantics can be defined by a CTL formula, then why should the CTL formula use existential modalities, such as “exists a successor with ϕ”? Shouldn’t it be enough to consider ACTL formulas, where only universal path quantification is used? The first result of this paper is
Author supported by Polish government grant no. N206 008 32/0810.
R. Amadio (Ed.): FOSSACS 2008, LNCS 4962, pp. 172–185, 2008. c Springer-Verlag Berlin Heidelberg 2008
The Common Fragment of ACTL and LTL
173
that, possibly surprisingly, this assumption is wrong. Indeed, a very simple LTL property, “all paths belong to (ab)∗ a(ab)∗ cω ”, can be defined in CTL but not ACTL. Intuitively speaking, to catch the extra a on every path, existential path quantification is needed. Therefore, two distinct questions can be investigated: which LTL
Data Loading...
