Description

Draft submitted to LFCS'97, Yaroslavl Interpretation of the Full Compation Tree Logic CTL Λ on Sets of Infinite Sequences (Extended Abstract) Ulrich Nitsche? Comper Science Department University ofzürich

Information

Category:
## Recruiting & HR

Publish on:

Views: 95 | Pages: 7

Extension: PDF | Download: 0

Share

Transcript

Draft submitted to LFCS'97, Yaroslavl Interpretation of the Full Compation Tree Logic CTL Λ on Sets of Infinite Sequences (Extended Abstract) Ulrich Nitsche? Comper Science Department University ofzürich Winterthurerstr. 190 CH-8057 Zürich Switzerland phone: Introduction The semantics of the branching-time temporal logic CTL Λ (full compation tree logic) is originally defined with respect to infinite tree-languages. Tointerpret a CTL Λ -formula on a set of infinite sequences, i.e. on an!-language, one cannot directly represent the!-language by a tree of infinite depth. Acceptance conditions needed to represent an!-languages prevent itstree representation. Only Eilenberg-limits of prefix-closed languages can be easily represented as infinite trees. We start with this tree representation of Eilenberg-limits of prefix-closed regular languages with respect to CTL Λ 's semantics to define a semantics for CTL Λ on sets of infinite sequences, i.e. on!-languages. To do so, we use the notion of an!-language's leftquotient byaword. The leftquotient represents the possible suffixes of a finitary word with respect to a given!-language. Using the terminology of trees, the finitary word determines a node in a tree and the leftquotient represents the subtree having the current node as its root. As already explained in the above remark on representability of!-languages by infinite trees, the!-language semantics for CTL Λ is, in the considered cases, a little more general than the usual tree semantics. We check our!-language semantics definition for CTL Λ to be meaningful regarding that, for the case of regular!-languages which are Eilenberg-limits of prefix-closed languages,!-language semantics and tree semantics coincide. 2 Preliminaries Regular languages and the basic properties of regular languages are assumed to be known as well as the representation of regular languages using finite aomata [1, 6, 7].? Former address: GMD, Rheinstr. 75, D Darmstadt, Germany. 1 Let ± be a finite set, called an alphabet. The set of all finite sequences over ± is denoted by ± Λ and the set of all infinite sequences over ± is denoted by ±!. A subset L of ± Λ is called a (finitary) language over ± and a subset L! of ±! is called an!-language over ± [12]. Let ± be an alphabet, and let L ± Λ and L! ±! be a finitary language and an!-language over ± respectively. The set of prefixes of L is pre(l) = fv 2 ± Λ j 9w 2 ± Λ : vw 2 Lg. The set of prefixes of L! is pre(l! )=fw 2 ± Λ j9x 2 ±! : wx 2 L! g.wecalll prefix-closed if and only if pre(l) =L. We define the limit of L to be [4, 12] lim(l) =fx 2 ±! j infinitely many different finite prefixes of x are in L.g: For an!-word x 2 ±!, x i designates the ith letter of x and x (i:::) designates the suffix of x starting with the ith letter: 8j 2 IN : x (i:::)j = x i+j 1.Letw be a word in ± Λ. Then, the leftquotient of L! by w is w 1 (L! )=fv 2 ±! j wv 2 L! g [1, 6].We can think of the leftquotient w 1 (L! )tobethecontinuation of w in L!. The leftquotient ofan!-word x 2 ±! byaword w 2 ± Λ is defined via the equation w w 1 (x) =x. 3 Interpretation of!-languages Let L ± Λ be a prefix-closed regular language. We represent lim(l) by a finitely branching tree T lim(l) of infinite depth (if lim(l) is not empty). We define T lim(l) in such a way that all finitely long sequences of labels of node along a finitely long path in T lim(l) starting at T lim(l) 's root are in L. All infinitely long paths of labels of nodes along infinitely long paths starting at T lim(l) 's root are in lim(l). Definition 1. For all w 2 L, letsucc(w) =w 1 (L) ±, i.e.succ(w) is the set of all letters in ± that can follow w in L. We define T lim(l) recursively: The root of T lim(l), denoted by root(t lim(l) ) is labelled with . If ν is a node in T lim(l),such that the path from the root is labelled with w, then ν has jsucc(w)j many child nodes and each child node is labelled with an element ofsucc(w) respectively. The set of all child nodes of a node ν is designated children(ν). T lim(l) does not contain any other nodes than the ones described. Foranodeν in T lim(l), label(ν) designates the label of ν. To be precise, T lim(l) is in fact a forest of jsucc( )j many trees. Each of these trees represents all!-words in lim(l) that start with the same letter. To have a single representation of lim(l), we have linked these trees to a particular node (T lim(l) 's root) which has to be labelled with the empty word for not changing the fact that path labels correspond to words in the language. 2 4 Defining CTL Λ with respect to T lim(l) We give CTL Λ syntax definition and afterwards present the definition of its semantics with respect to T lim(l), whichistheobvious adaption of CTL Λ semantics [2, 3, 5] to the structure of T lim(l). Definition 2. We define the syntaxofctl Λ with respect to a set AP of atomic propositions [5]. All atomic propositions are state formulae. If ο and are state formulae then so are (ο) ^ ( ) and:(ο). If ο is a path formula then A(ο) ande(ο) are state formulae. Each state formula is also a path formula. If ο and are path formulae then so are (ο) ^ ( ) and :(ο). If ο and are path formulae then so are (ο) U( ) andx (ο). No other formulae are CTL Λ -formulae. Defining the semantics of CTL Λ with respect to T lim(l),wehave to take care abo T lim(l) 's root ρ, because it is the only node with label(ρ) 62 ±. We define the satisfaction relation j= between nodes of T lim(l) and CTL Λ -formulae such that T lim(l) satisfies a CTL Λ -formula if and only if its root does (initial satisfaction). The satisfaction relation is defined with respect to a labelling function : ±! 2 AP that takes node-labels to the set of atomic propositions that determines to be satisfied for the node-label. Definition 3. Let, ο and be CTL Λ -formulae and let ν be a node in T lim(l). Let, for all nodes fl of T lim(l), path(fl) designate the set of all infinite paths in T lim(l) that start at fl. If 2 AP and label(ν) = , thenν j= if and only if 8fl 2 children(ν) : 2 (label(fl)). If 2 AP and label(ν) 6= , thenν j= if and only if 2 (label(ν)). ν j= :(ο) if and only if it is not the case that ν j= ο. ν j= (ο) ^ ( ) if and only if ν j= ο and ν j=. If label(ν) = , then ν j= E(ο) if and only if 9ff 2 S fl2children(ν) path(fl) : ff j= ο. If label(ν) 6= , thenν j= E(ο) if and only if 9ff 2 path(fl) :ff j= ο. If label(ν) = , then ν j= A(ο) if and only if 8ff 2 S fl2children(ν) path(fl) : ff j= ο. If label(ν) 6= , thenν j= A(ο) if and only if 8ff 2 path(fl) :ff j= ο. Let ff = s 1 s 2 s 3... be an infinite path in T lim(l) starting at a node s 1 with label(s 1 ) 6= , i.e.s 1 is not the root of T lim(l). If 2 AP, then ff j= if and only if 2 (label(s 1 )). ff j= :(ο) if and only if it is not the case that ff j= ο. ff j= (ο) ^ ( ) if and only if ff j= ο and ff j=. 3 ff j= X (ο) if and only if ff (2:::) j= ο. ff j= (ο) U( ) if and only if there exist an i 2 IN such that ff (i:::) j= and, for all j i, ff (j:::) j= ο. ff j= E(ο) if and only if 9ff 0 2 path(s 1 ):ff 0 j= ο. ff j= A(ο) if and only if 8ff 0 2 path(s 1 ):ff 0 j= ο. We use this satisfaction relation on nodes of T lim(l) to define the satisfaction relation on T lim(l) itself as satisfaction in T lim(l) 's root (intial satisfaction). Definition 4. Let be a CTL Λ -formula and let : ±! 2 AP be a labelling function of node-labels with atomic propositions. Then T lim(l) j= (with respect to ) if and only if root(t lim(l) ) j= (with respect to ). In Definition 3, we have adapted usual CTL Λ semantics to fit to T lim(l). We can use the previous definition to define a CTL Λ semantics with respect to general!-languages. Before we do so, we first give an example why we cannot always represent languages by a tree as presented above. 5 Not All!-Languages Have a Tree Representation If we consider the!-language lim(fa; bg Λ )whichisfa; bg!, then T lim(fa;bg Λ ) is the complete binary tree with nodes labelled with a and b such that its root is labelled with . Obviously, fa; bg Λ is prefix-closed. lim(fa; bg Λ ) is obtained by thesetof all infinite sequences of node-labels along infinite paths in T lim(fa;bg Λ ). Hence we have a nice one-to-one correspondence between lim(fa; bg Λ )andt lim(fa;bg Λ ). If we consider the!-language lim((fa; bg Λ a) Λ ) (all!-words must contain infinitely many occurences of letter a), then (fa; bg Λ a) Λ is not prefix-closed anymore. Nevertheless lim((fa; bg Λ a) Λ ) is not very different from lim(fa; bg Λ ). If wewant to construct a tree corresponding to Definition 1 for lim((fa; bg Λ a) Λ ), we would have to replace L by pre(l) in Definition 1. B pre((fa; bg Λ a) Λ ) = fa; bg Λ and hence lim((fa; bg Λ a) Λ ) would be presented by the same binary tree as lim(fa; bg Λ ) is. So the resulting tree does not correspond precisely to lim((fa; bg Λ a) Λ ) and therefore we cannot evaluate a CTL Λ -formula with respect to lim((fa; bg Λ a) Λ ) using this tree representation. 2 Using the notion of leftquotients we can relax the CTL Λ semantics definition to be suitable for all!-languages (ignoring decidability questions for the moment). 6 Satisfaction of CTL Λ -Formulae with Respect to!-languages We can use the fact that the leftquotient of an!-language by a word extracts exactly the information abo suffixes of the word in the!-language to define a 2 In general, languages L that require accepting states for there representation (i.e. that are not prefix-closed) have a tree representation equivalent to pre(l). 4 CTL Λ semantics on!-languages. Definition 5. Let L! ±! be an!-language. Let, ο and be CTL Λ -formulae. Let : ±! 2 AP be a labelling function. Let w be a (finitary) word in pre(l! ). If w 6= , letlast(w) designate the last letter in w and let short(w) be the word that we obtain by removing w's last letter. For an!-word x 2 ±!, let first(x) designate x's first letter. We define the satisfaction relation with respect to L! and : If 2 AP and w = , then w j= if and only if 8x 2 L! : 2 (first(x)). If 2 AP and w 6= , then w j= if and only if 2 (last(w)). w j= :(ο) if and only if it is not the case that w j= ο. w j= (ο) ^ ( ) if and only if w j= ο and w j=. If w = , then w j= E(ο) if and only if 9x 2 L! :(w; x) j= ο. If w 6= , then w j= E(ο) if and only if 9x 2 w 1 (L! ):(short(w); last(w)x) j= ο. If w = , then w j= A(ο) if and only if 8x 2 L! :(w; x) j= ο. If w 6= , then w j= A(ο) if and only if 8x 2 w 1 (L! ):(short(w); last(w)x) j= ο. Let u 2 ± Λ be a word and let x 2 ±! be an!-word over ±. If 2 AP, then (u; x) j= if and only if 2 (first(x)). (u; x) j= :(ο) if and only if it is not the case that (u; x) j= ο. (u; x) j= (ο) ^ ( ) if and only if (u; x) j= ο and (u; x) j=. (u; x) j= X (ο) if and only if (ufirst(x);first(x) 1 (x)) j= ο. (u; x) j= (ο) U( ) if and only if there exist an w 2 pre(x) suchthat(uw; w 1 (x)) j= and such that, for all v 2 pre(x) withjvj jwj, (uv; v 1 (x)) j= ο. (u; x) j= E(ο) if and only if 9x 0 2 (u first(x)) 1 (L! ):(u; first(x)x 0 ) j= ο. (u; x) j= A(ο) if and only if 8x 0 2 (ufirst(x)) 1 (L! ):(u; first(x)x 0 ) j= ο. L! satisfies with respect to if and only if the empty word satisfies with respect to L! and (the modified version of initial satisfaction). For prefix-closed L ± Λ, the above definition with respect to lim(l) is(not astonishingly) equivalent to the definition with respect to T lim(l) : Lemma 6. Let L ± Λ be a prefix-closed language, let be a CTL Λ -formula, and let : ±! 2 AP be a labelling function. Then lim(l) j= if and only if T lim(l) j= : 7 Conclusions We have defined a semantics for CTL Λ on!-languages instead of infinite trees. The definition is a slight modification of CTL Λ 's usual semantics definition, using the notion of an!-language's leftquotient by a word to adapt the logical terminology on branching processes to the notations of formal language theory. 5 The way wehave looked at CTL Λ in this paper has the advantage to relate property classes defined in terms of formal language theory to logical notions. E.g., using the!-language semantics for CTL Λ allows to identify always possibly properties of [8] with eventuality properties in [9], that are represented by the AGEF-fragment of CTL Λ. Since always possibly properties are proven in [8] to be algorithmically complex with respect to model checking versus different environments (called: module checking), the identification with eventuality properties reveals a verification using abstraction -concept as presented in [11] based on results in [10]. The topic of decidability of the satisfaction of a CTL Λ -formula on a given!-language is not discussed in this extended abstract. It is highly probable that this problem is decidable for regular!-languages, related to the usual model checking algorithm [2, 3, 5]. Defining the model checking algorithm precisely for the!-language semantics of CTL Λ is a topic for further study. Another topic of interest is the question of checking CTL Λ -formulae on homomorphic abstractions of!-languages to obtain information abo the!-language itself. This is also a question for further study, only partly solved in [9, 11]. References 1. J. Berstel. Transductions and Context-Free Languages. Studienbücher Informatik. Teubner Verlag, Sttgart, first edition, E. M. Clarke and E. A. Emerson. Design and synthesis of synchronization skeletons using branching-time temporal logic. In D. Kozen, editor, Logic of Programs 1981, volume 131 of Lecture Notes in Comper Science, pages Springer Verlag, E. M. Clarke, E. A. Emerson, and A. P. Sistla. Aomatic verification of finitestate concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems, 8(2): , S. Eilenberg. Aomata, Languages and Machines, volume A. Academic Press, New York, E. A. Emerson. Temporal and modal logic. In van Leeuwen [13], pages M. A. Harrison. Introduction to Formal Language Theory. Addison-Wesley, Reading, Mass., first edition, J. E. Hopcroft and J. D. Ullman. Introduction to Aomata Theory, Languages and Compation. Addison-Wesley, Reading, Mass., first edition, O. Kupferman and M. Y. Vardi. Module checking. In R. Alur and T. A. Henzinger, editors, CAV'96, volume 1102 of Lecture Notes in Comper Science, pages 75 86, New Brunswick, N.J., Springer Verlag. 9. U. Nitsche. Verification of Co-Operating Systems and Behaviour Abstraction. PhD thesis, University offrankfurt, Germany. submitted U. Nitsche. Propositional linear temporal logic and language homomorphisms. In A. Nerode and Y. V. Matiyasevich, editors, Logical Foundations of Comper Science '94, St. Petersburg, volume 813 of Lecture Notes in Comper Science, pages Springer Verlag, U. Nitsche. Verification and behavior abstraction towards a tractable verification technique for large distribed systems. Journal of Systems and Software, 33(3): , June 12. W. Thomas. Aomata on infinite objects. In van Leeuwen [13], pages J. van Leeuwen, editor. Formal Models and Semantics, volume B of Handbook of Theoretical Comper Science. Elsevier, This article was processed using the LaT E X macro package with LLNCS style 7

Related Search

Similar documents

We Need Your Support

Thank you for visiting our website and your interest in our free products and services. We are nonprofit website to share and download documents. To the running of this website, we need your help to support us.

Thanks to everyone for your continued support.

No, Thanks