Modal logics on rational Kripke structures Wilmari Bekker Student Number: 0616713N Supervisor: Associate Professor Valentin Goranko Masters Dissertation School of Mathematics Faculty of Science University of the Witwatersrand Johannesburg South Africa November 2007 ii Declaration I declare that this dissertation is my own, unaided work. It is being submitted for the Degree of Master of Science in the University of the Witwatersrand, Johannesburg. It has not been submitted before for any degree or examination in any other University. Wilmari Bekker 26th day of November 2007, Johannesburg iii Acknowledgments I would to thank my supervisor, Valentin Goranko, for his instruction and guidance. He has made many opportunities available to me and has pushed me to make full use of them. Some of the work in this dissertation has been co-authored by Valentin Goranko and myself. Furthermore, I would like to thank the National Research Foundation of South Africa for the funding provided during 2006 which made it possible to focus on my studies. Many thanks to Arnaud Carayol, Christophe Morvan and Stephane Demri for some useful remarks and suggestions. I would like to thank all my friends and family for their endless support and encour- agement. In particular, I would like to thank my husband for his support and useful insight: ?Diamonds belong on a ring in a Box.? Thank you Grant. Finally I give thanks to my Lord Jesus for giving me the talent and perseverance to see this study through. iv Abstract This dissertation is a contribution to the study of infinite graphs which can be presented in a finitary way. In particular, the class of rational graphs is studied. The vertices of a rational graph are labeled by a regular language in some finite alphabet and the set of edges of a rational graph is a rational relation on that language. While the first-order logics of these graphs are generally not decidable, the basic modal and tense logics are. A survey on the class of rational graphs is done, whereafter rational Kripke models are studied. These models have rational graphs as underlying frames and are equipped with rational valuations. A rational valuation assigns a regular language to each propo- sitional variable. I investigate modal languages with decidable model checking on ra- tional Kripke models. This leads me to consider regularity preserving relations to see if the class can be generalised even further. Then the concept of a graph being rationally presentable is examined - this is analogous to a graph being automatically presentable. Furthermore, some model theoretic properties of rational Kripke models are examined. In particular, bisimulation equivalences between rational Kripke models are studied. I study three subclasses of rational Kripke models. I give a summary of the results that have been obtained for these classes, look at examples (and non-examples in the case of automatic Kripke frames) and of particular interest is finding extensions of the basic tense logic with decidable model checking on these subclasses. An extension of rational Kripke models is considered next: omega-rational Kripke models. Some of their properties are examined, and again I am particularly interested in finding modal languages with decidable model checking on these classes. Finally I discuss some applications, for example bounded model checking on rational Kripke models, and mention possible directions for further research. Contents 1 Introduction 1 2 Preliminaries 5 2.1 Monoids . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 2.2 Languages . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 2.3 Automata and Transducers . . . . . . . . . . . . . . . . . . . . . . . . . 8 2.4 Recognisable, rational, and regular sets . . . . . . . . . . . . . . . . . . 11 2.5 Recognisable, and rational relations . . . . . . . . . . . . . . . . . . . . 14 2.6 Modal logics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17 2.6.1 Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17 2.6.2 Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19 2.7 Bisimulation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20 2.8 Petri nets . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 3 Rational Kripke Structures 25 3.1 Rational graphs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 3.1.1 Results on rational graphs . . . . . . . . . . . . . . . . . . . . . 26 3.2 Introducing rational Kripke structures . . . . . . . . . . . . . . . . . . 31 3.3 Model checking . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 3.3.1 Synchronised products of transducers and automata . . . . . . . 34 3.3.2 Model checking of Kt in rational Kripke models . . . . . . . . . 37 3.3.3 Complexity . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 3.3.4 Hybrid logics . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 3.4 Regularity preserving relations . . . . . . . . . . . . . . . . . . . . . . . 44 3.4.1 An algebraic view . . . . . . . . . . . . . . . . . . . . . . . . . . 49 3.5 Rationally presentable structures . . . . . . . . . . . . . . . . . . . . . 50 3.6 Model constructions . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 3.6.1 Disjoint unions . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 3.6.2 Generated substructures . . . . . . . . . . . . . . . . . . . . . . 54 3.6.3 Unfoldings . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 3.7 Bisimulation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 v vi CONTENTS 3.7.1 Bisimulation between two rational Kripke structures. . . . . . . 56 3.7.2 The finite bisimilarity problem . . . . . . . . . . . . . . . . . . . 62 4 Subclasses of Rational Kripke Structures 67 4.1 Automatic Kripke structures . . . . . . . . . . . . . . . . . . . . . . . . 67 4.1.1 Examples and non-examples of automatic frames . . . . . . . . 69 4.1.2 Model checking on Automatic structures . . . . . . . . . . . . . 76 4.2 Rational Kripke trees . . . . . . . . . . . . . . . . . . . . . . . . . . . . 77 4.2.1 Model checking on rational Kripke trees . . . . . . . . . . . . . 80 4.3 Monotonous rational Kripke structures . . . . . . . . . . . . . . . . . . 81 4.3.1 Model checking on monotonous rational Kripke structures. . . . 82 5 An extension of rational Kripke structures 85 5.1 ?-rational languages . . . . . . . . . . . . . . . . . . . . . . . . . . . . 85 5.2 ?-rational relations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 89 5.3 ?-rational Kripke structures . . . . . . . . . . . . . . . . . . . . . . . . 92 5.4 Model checking on ?-rational Kripke models . . . . . . . . . . . . . . . 94 6 Conclusion 97 6.1 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 97 6.2 Applications . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 98 6.2.1 Regular model checking . . . . . . . . . . . . . . . . . . . . . . 98 6.2.2 Bounded model checking . . . . . . . . . . . . . . . . . . . . . . 98 6.3 Open problems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 100 List of Figures 2.1 The automaton A recognising the regular set 0 (101)? 0. . . . . . . . . . 9 2.2 The transducer T which recognises pairs of words of either the form (u, u0) or (u, u1) where u ? ?? and ux denotes the concatenation of the word u and the letter x. . . . . . . . . . . . . . . . . . . . . . . . . . . 11 2.3 The Petri net N = (Nl,M0). . . . . . . . . . . . . . . . . . . . . . . . . 23 2.4 N after transition t1 is fired. . . . . . . . . . . . . . . . . . . . . . . . . 23 2.5 N after transition t2 is fired. . . . . . . . . . . . . . . . . . . . . . . . . 23 3.1 The infinite grid with set of vertices S = 0?1?. . . . . . . . . . . . . . . 26 3.2 A transducer that recognises the infinite grid. . . . . . . . . . . . . . . 26 3.3 The complete binary tree ?. . . . . . . . . . . . . . . . . . . . . . . . . 27 3.4 A labeled transducer recognising the complete binary tree ?. . . . . . . 27 3.5 A transducer associated with an instance of the PCP. . . . . . . . . . . 28 3.6 The finite transducer T . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 3.7 A finite degree rational graphs with the vertices at a distance n from any chosen vertex u having out-degree 22n+1 . . . . . . . . . . . . . . . . . . 30 3.8 The transducer recognising the relation Ri associated with the transition ti. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 3.9 A finite presentationM: A1, A2 and A3 recognises S, V (q1) and V (q2) respectively, and T recognises R. . . . . . . . . . . . . . . . . . . . . . 33 3.10 The automaton A before reduction . . . . . . . . . . . . . . . . . . . . 35 3.11 The automaton A|2, the 2-reduction of A . . . . . . . . . . . . . . . . . 35 3.12 The transducer T used in the synchronised product. . . . . . . . . . . . 37 3.13 The automaton A used in the synchronised product. . . . . . . . . . . 37 3.14 The synchronied product T iA. . . . . . . . . . . . . . . . . . . . . . 37 3.15 A presentation of S which is not rational. . . . . . . . . . . . . . . . . . 51 3.16 A rational presentation of S. . . . . . . . . . . . . . . . . . . . . . . . . 51 3.17 The transducer reconising R = {(xn, yn) |n ? 0}. . . . . . . . . . . . . . 51 3.18 The subframe generated by the regular set X = {0}. . . . . . . . . . . 55 3.19 The net N constructed to simulate C. Suppose Sc is a command of the first type using c1 and Sd of the second type using c2 where 1 ? c, d < n. 58 vii viii LIST OF FIGURES 3.20 The newly constructed nets N1 and N2. . . . . . . . . . . . . . . . . . . 59 4.1 The synchronous transducer T recognising ?R. . . . . . . . . . . . . . 68 4.2 An automatic Kripke frame. . . . . . . . . . . . . . . . . . . . . . . . . 68 4.3 The Collatz?s graph. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 72 4.4 A finite transducer that recognises the relation of an elementary congru- ential graph. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 72 4.5 A transducer recognising R = {(u, v) |u ? {a, bb}? , v ? {ba?b}?}. . . . . 73 4.6 A transducer recognising R = {(An, u) |n ? 0, u ? B? (AB?)n}. . . . . . 74 4.7 A finite degree rational graph with the vertices at a distance n from any chosen vertex r having out-degree 2n2 . . . . . . . . . . . . . . . . . . . 75 4.8 A transducer recognising the relation R. . . . . . . . . . . . . . . . . . 76 4.9 A non-automatic rational Kripke frame with finite out-degree. . . . . . 76 4.10 A finite transducer that produces a rational Kripke frame with finite, but unbounded degree. . . . . . . . . . . . . . . . . . . . . . . . . . . . 78 4.11 The forest such that every vertex at a depth n has 2n successors. . . . . 79 4.12 A transducer which produces a graph connecting the roots. . . . . . . . 79 4.13 The rational graph relating all the roots of the forest. . . . . . . . . . . 80 4.14 A transducer T producing a monotonous rational Kripke frame. . . . . 82 4.15 A monotonous rational Kripke frame. . . . . . . . . . . . . . . . . . . . 82 5.1 A non-deterministic Bu?chi automaton and a Muller automaton both recognising ? = (1?0?01)? (0? + 1?). . . . . . . . . . . . . . . . . . . . . 87 5.2 The finite automaton A and the Bu?chi automaton A?. . . . . . . . . . 88 5.3 A transducer T which can be equipped with either Bu?chi or Muller acceptance conditions in order for it to recognise the ?-rational relation R. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 91 5.4 A transducer T recognising R = ((0, 1) (1, 1)? (0, 1))?. . . . . . . . . . . 91 5.5 A transducer T? recognising R?. . . . . . . . . . . . . . . . . . . . . . . 91 5.6 Bu?chi automata and transducers representing the ?-rational Kripke model M. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 93 5.7 The Bu?chi transducer recognising the relation {(CX , CY ) |X ? Y }. . . . 94 5.8 The Bu?chi automaton A and the Bu?chi transducer T . . . . . . . . . . . 94 5.9 A Bu?chi automaton B. . . . . . . . . . . . . . . . . . . . . . . . . . . . 95 Chapter 1 Introduction Verification of models with infinite state spaces using algorithmic symbolic model check- ing techniques has attracted considerable attention in recent years. Verifying safety, liveness, reachability, and other such properties, specified in some formal language, for computer programs is one of the main contributers that sparks interest in this field. There are many examples of infinite graphs stemming from computer science. At least five such ?sources of infinity? have been identified by Esparza in [38]: 1. Data manipulation: this includes unbounded counters, integer variables, lists, trees, more general pointer structures, etc. 2. Control structures: for example the dynamic creation of processes or unbounded call stacks. 3. Asynchronous communication: unbounded FIFO queues serves as an example. 4. Parameters: the parameterisation describing generic systems for example the number of processes, gates or buffers, or the duration of delays. 5. Real time: timing constraints in real-time systems with discrete or dense domains. Verification is not possible on all infinite structures. It is not always possible to get a handle on an infinite structure which enables algorithmic verification and therefore verifying properties specified in some formal language is often undecidable. In [17] Blumensath and Gra?del mention two fundamental conditions which must be satisfied by infinite structures on which verification is to be done : 1. The structure must be representable in a finite way. 2. The model checking problem of a relevant logic must be decidable on the domain of the structure. 1 2 CHAPTER 1. INTRODUCTION One important development in infinite state verification has been Caucal?s hier- archy [28], consisting of structures with decidable monadic second-order theories. In fact, the formal language in which the properties are specified here is very expressive. Reachability, liveness, safety, etc. properties can all be specified in second-order logic. Verifying these properties on graphs in Caucal?s hierarchy is therefore decidable. Another very successful approach to infinite state verification is based on represen- tation of sets of states and transitions by means of various automata. The task is then to identify large and natural classes of (possibly) infinite structures which are repre- sentable by finite automata. Once such a class has been identified, formal languages that are sufficiently expressive and for which verification is decidable on the class of structures, need to be identified. In [69] Morvan describes the use of various automata to represent infinite structures as an internal characterisation of the structure as opposed to an external characterisa- tion where the structure (up to isomorphism) of the system is produced. Various automata-based techniques for model checking are based on the use of finite machines to present an infinite structure. Some examples include model checking of linear and branching-time temporal logics on finite transition systems [90, 59], regular model checking [20], pushdown systems [19, 92, 40], and automatic structures [54, 16]. The temporal logics are sufficiently expressive for various reachability properties in most of the studied cases of infinite-state symbolic model checking. Unfortunately, each of these classes of models are relatively restricted. In [70] Morvan studies a large and natural class of infinite graphs . The transition relations of rational graphs can be presented by finite asynchronous automata which are called transducers in the sequel. Automata-based techniques for model checking can therefore be applied to rational graphs. To this end, rational Kripke models are introduced in [46]. Rational Kripke models are based on rational graphs and every atomic proposition is evaluated is a regular set of states. In this dissertation I study the class of rational Kripke models, on which global model checking of the basic tense1 logicKt (with forward and backward one step modal- ities) and some hybrid extensions thereof, is decidable. The language of Kt is sufficient for expressing local properties, in particular pre-conditions and post-conditions, but not reachability properties. Kesten et al [53] have formulated the following minimal requirements for an asser- tional language L to be adequate for symbolic model checking: 1. The property to be verified and the initial conditions (i.e., the set of initial states) should be expressible in L. 2. L should be effectively closed under the boolean operations, and should possess an algorithm for deciding equivalence of two assertions. 1The term ?tense? rather than ?temporal? is used, to emphasize that the accessibility relation is not assumed transitive, as in a usual flow of time. 3 3. There should exist an algorithm for constructing the predicate transformer pred, where pred(?) is an assertion characterizing the set of states that have a successor state satisfying ?. The first condition depends on the property to be verified while the set of initial states is usually assumed to be at least regular, if not a singleton, and can be represented by a special modal constant S. K is clearly closed under boolean operations if the equivalence is assumed to be with respect to the model on which the verification is being done. Finally, pred(?) = ?R?? and an algorithm constructing it is presented in this dissertation. Thus, the basic modal logic K is the minimal natural logical language satisfying these requirements, and hence it suffices at least for specification of pre-conditions verified over regular sets of states. The tense extension Kt is the basic adequate logic for specifying local properties of transition systems since it enables specification of post-conditions as well. Furthermore, the basic tense logic Kt can easily be extended to very expressive languages: reachability between two given states can be expressed in hybrid extensions of Kt, while reachability, liveness, safety, etc. properties can be expressed in linear- and branching-time temporal logics. The study of these logics has become an increasingly important area of research in recent years. There are a number of ways to deal with the inability of Kt to express important properties like reachability. One way is to consider model constructions which preserve the truth of properties specified in one of the more expressive extensions of Kt. The other is to consider subclasses of the rational Kripke models. Rational graphs have not been studied widely in the literature. The decidability of model checking of Kt (and extensions of it) in rational Kripke structures, however, warrants a closer look these structures. This is exactly the aim of this dissertation, while keeping model checking of modal languages in mind. This dissertation is organised as follows: Chapter 2 contains all the necessary defini- tions and background theory, starting with the abstract structures monoids. Languages and relations which can be finitely presented as well as the machines used to present them are then studied. Basic modal logics is discussed briefly and the definition of the model construction bisimulation is revisited. Lastly Petri nets are presented. These are graphs originally introduced to solve concurrency problems in systems. In Chapter 3 a summary of results on rational graphs is given. Rational Kripke models are studied in more detail for the remainder of that chapter. I consider a number of model checking tasks on these structures and show that local an global model checking Kt are decidable. The complexity of these results are then studied. The decidability of these model checking tasks then gives rise to a class of relations called regularity preserving relations. These relations are studied and as a result two types of two-sorted algebras find new importance. Some model theoretic results of rational Kripke models are presented and in particular the decidability of bisimulation equivalence between rational Kripke models and frames is examined. 4 CHAPTER 1. INTRODUCTION Next, I study three subclasses of rational Kripke models in Chapter 4. Automatic Kripke models (these are Kripke models based on automatic graphs), rational Kripke trees (here the rational graph on which the model is based is acyclic and connected) and finally, monotonous rational Kripke models. Some model checking tasks are discussed for each of these subclasses. In Chapter 5 I study the extension of rational Kripke models to ?-rational Kripke models. This extension forms an even more general class of structures. In conclusion, some potential applications are mentioned and some open problems are discussed in Chapter 6. Chapter 2 Preliminaries 2.1 Monoids Recognisability and rationality of sets and relations are defined over the algebraic struc- tures called monoids ? a subclass of semigroups. In this section I present the relevant definitions. Definition 2.1.1 ([7, 80]) A semigroup is a structure S = (M, ?) where M is a set called the carrier set and ? is an associative binary operation on M (in future referred to as the semigroup product or simply the product), i.e. m1?(m2 ?m3) = (m1 ?m2)?m3 holds for all m1,m2,m3 ?M . Definition 2.1.2 ([7, 36, 80]) Let S = (M, ?, 1M ) where (M, ?) is a semigroup and 1M ? M . If 1M is such that for all m ? M it holds that 1M ?m = m ? 1M = m, then S is called a monoid, and the element 1M is called a unit. The binary relation ? can be extended to operate on subsets of the domain. If S = (M, ?, 1M ) is a monoid and ?,? ?M , then the product of ? and ? is the set: ? ? ? = {u ?M |?x ? ? ?y ? ? : u = x ? y} The product of a subset ? with itself will be denoted by ?2 = ? ? ?. Setting ?0 = {1M} it follows that ?n = ? ? ?n?1 ?n ? 1. Definition 2.1.3 ([7, 36, 80]) A sub-semigroup (submonoid) of a semigroup (re- spectively monoid) S = (M, ?) (S = (M, ?, 1M )) is a subset ? ? M such that ?2 ? ? (respectively 1M ? ? and ?2 ? ?). The least sub-semigroup and submonoid, with respect to set inclusion, that contains a subset ? ?M are the sets ?+ and ?? respectively defined by ?+ = ? n?1 ?n ?? = ? n?0 ?n 5 6 CHAPTER 2. PRELIMINARIES A monoid S = (M, ?, 1M ) is generated by a subset ? ?M , if M = ??. If the subset ? is finite then S is said to be finitely generated. Definition 2.1.4 ([7, 36, 80]) A monoid S = (M, ?, 1M ) is free if there is a non- empty subset ? ?M such that M = ?? and every element in M can either be uniquely expressed as the product of elements in ? or is inexpressible as such a product.1 If ? is finite, S is said to be a finitely generated free monoid. Two or more monoids can now be used to define product monoids. Definition 2.1.5 ([80]) Let S1 = (M1, ?1, 1M1) and S2 = (M2, ?2, 1M2) be two monoids. The cross-product monoid of S1 and S2 is the monoid (M1 ?M2, ?, (1M1 , 1M2)) where ? is the component-wise application of the monoid products, i.e. if (a, b) , (c, d) ? M1 ?M2 then (a, b) ? (c, d) = (a ?1 c, b ?2 d). In conclusion of this section, morphisms are defined. Definition 2.1.6 ([7, 36, 80]) Let S1 and S2 be monoids. A monoid morphism (just morphism for short) is a function ? : M1 ? M2, where M1 and M2 are the respective domains and ?1 and ?2 the product operations of S1 and S2 respectively, which satisfies: 1. ? (u ?1 v) = ? (u) ?2 ? (v) 2. ? (1M) = 1M ? 2.2 Languages For any finite set ?, there is a finitely generated free monoid where the product oper- ation of the monoid is the concatenation of elements, i.e. for (??, ?, 1??) the elements of ?? are tuples of elements from ?: u ? ?? ?? there exists n ? N such that u = x1x2 ? ? ? xn where x1, x2, . . . , xn ? ? Furthermore, if u, v ? ?? where u = x1x2 ? ? ? xn and v = y1y2 ? ? ? ym and n,m ? N then u ? v = x1x2 ? ? ? xny1y2 ? ? ? ym = uv. (The ? sign is omitted since it is known that the product operation is the concatenation of the elements.) The unit 1?? of this monoid will then be the 0-tuple denoted by . Under these circumstances the set ? can be viewed as an alphabet. Words in an alphabet ? are finite sequences of elements from the alphabet which are exactly the 1Clearly the unit cannot be an element of ?, for suppose the element 1M belonged to ? and let x ? ? be an arbitrary element of ?, then x ? M can be expressed as 1M ? x = x = x ? 1M , which is not unique. Therefore 1M /? ?. 2.2. LANGUAGES 7 elements of the monoid ?? as defined above and the unit is the empty word. A language over an alphabet consists of words over an alphabet on which a number of restrictions are placed. Therefore, a language over ? is a subset of ??. I will use ? and ? to denote alphabets, words will be denoted by u, v, w and x, y, z will be used to denote letters in the alphabet. A hierarchy of four families of languages were introduced by Chomsky [66, 84] as syntactic models of natural language. These four families are the regular languages, context-free languages, context-sensitive languages and recursively enumer- able languages - each family strictly including the previous. I will discuss two of these families in this dissertation, namely the context-free and regular languages. Special no- tice will be taken of the latter since it will be particularly useful when doing model checking. The definitions of the other two families of languages can be found in [84]. The strings of a language are formally generated by a set of rules, called a grammar. By placing different restrictions on the rules of grammars, different classes of languages can be generated. Definition 2.2.1 ([7, 66, 84]) A context-free grammar is a quadruple G = ?V,?, P, S? where V is a finite set of variables, the set ? is a finite alphabet, V ?? = ?, the symbol S belongs to V and P is a finite set of rules belonging to ?? (? ? ?)?. The elements of ? are called terminal symbols since they form the indecomposable elements used to construct strings in the languages and S is called the start symbol. Example 2.2.2 Let G = ?V,?, P, S? be defined by 1. V = {A,B} 2. ? = {x, y} 3. P = {A? xB|y; B? Ay} 4. S = A The ?|? sign in the rule referrers to a choice, i.e. the variable A can be replaced by either the symbols xB or by the terminal symbol y. ? A string (word) is generated by a grammar if it can be produced by a finite succession of rules in the grammar starting with the designated starting symbol in the grammar. The set of all such words generated by a grammar is the language generated by the grammar. Definition 2.2.3 ([7, 66, 84]) A language L over some alphabet ? is a context-free language if it is generated by some context-free grammar G. Example 2.2.4 Consider the language L = {xnyn+1|n ? 0}. This is the language generated by the context-free grammar in Example 2.2.2. ? 8 CHAPTER 2. PRELIMINARIES Definition 2.2.5 ([66]) Let G = ?V,?, P, S? be a grammar where ?,? and S are de- fined as before, and where the rules in P are all in one of the following forms. For A,B ? ? and x ? ? 1. A? x 2. A? xB 3. A?  where B 6= A. Under these conditions the grammar G is a right regular grammar. The grammar defined above is also called a right-linear grammar. Left regular grammars can be defined in a similar way. Observe that the rule B ? Ay in Example 2.2.2 is not in the right form for the grammar to be right-regular. In fact, the language generated by this grammar, as given in Example 2.2.4 cannot be generated by either a left- or right-regular grammar. Example 2.2.6 Let G = ?V,?, P, S? be a grammar with V,? and S defined in the same way as in Example 2.2.2. Furthermore, let P = {A? x|xB B? yA}, then G is a regular grammar. ? Definition 2.2.7 ([66]) A language L over some alphabet ? is a regular language if it can be generated by some left or right regular grammar G. Example 2.2.8 {(xy)n x|n ? 0} is the regular language generated by the regular gram- mar shown in Example 2.2.6. ? 2.3 Automata and Transducers In this section classes of machines are defined. These machines will be used as language recognisers. Definition 2.3.1 ([80]) An abstract finite automaton is a quadruple A = ?Q,M, q0, F, ?? where Q is a finite set of states, F ? Q is a set of accepting states, q0 ? Q is a unique initial state, M is the domain of some monoid S = (M, ?, 1M ) and ? : Q?M ? Q is the next state function satisfying: 1. ? (q, 1M) = q holds for all q ? Q 2. ? (q,m1 ?m2) = ? (? (q,m1) ,m2) for all q ? Q and for all m1,m2 ?M . When a finitely generated free monoid is considered, the definition reads as given below. 2.3. AUTOMATA AND TRANSDUCERS 9 Definition 2.3.2 ([7, 36, 80, 84]) Given a finite set of states Q, a finite alphabet ?, a state q0 ? Q, a subset F ? Q and a relation ? : Q ? ? ? Q, then the quadruple A = ?Q,?, q0, F, ?? is a finite deterministic automaton Given an automaton A = ?Q,?, q0, F, ??, then a sequence q1 x1? q2 x2? ? ? ? xn? qn+1 is called a path if qj ? Q for j = 1, 2, . . . , n + 1 and x1, x2, . . . , xn ? ? such that qi+1 ? ? (qi, xi) for i = 1, 2, . . . , n. If q1 = q0 then the path is called a run of the automaton. Definition 2.3.3 ([7, 36, 80, 84]) A word u ? ?? is accepted by A = ?Q,?, q0, F, ?? if and only if there exists a run q1 x1? q2 x2? ? ? ? xn? qn+1 such that qn+1 ? F , n ? N and u = x1x2 ? ? ? xn (Thus the run is labeled by the word u). Such a run is called an accepting run. The set of all words accepted by A, denoted by L (A), is said to be the language recognised by A. Instead, the next state relation can also be defined such that ? : Q ? ? ? P (Q). An automaton with a next state relation is a nondeterministic finite automaton. Another variation of an automaton would be to define the the next state function on words instead of letters, i.e. ? : Q? ?? ? Q. Example 2.3.4 Let A = ?Q,?, q0, F, ?? be a nondeterministic finite automaton with 1. Q = (q0, q1, q2, q3, qf), 2. ? = {0, 1}, 3. F = { qf } , and 4. ? = {(q0, 0, q1) , (q1, 1, q2) , (q2, 0, q3) , (q3, 1, q1) ,(q1, 0, qf)}. A can now be represented by a graph in the following way: Figure 2.1: The automaton A recognising the regular set 0 (101)? 0. q0 q1 qf q3 q2 0 0 1 0 1 The word u = 01011010 is recognised by A since there is an accepting run in A labeled by u. ? 10 CHAPTER 2. PRELIMINARIES Finite automata can now be extended in such a way that the resulting class of machines are able to recognise a more general class of languages. Definition 2.3.5 ([84]) The tuple M = ?Q,?,?, q0, F, ?? is a pushdown automa- ton when ? and ? are finite disjoint alphabets, called the input and stack alphabets respectively, Q is a set of states, q0 ? Q a unique starting state, F ? Q a set of final states, and ? ? Q? (? ? {})? (? ? {?})?Q? (? ? {?}) is a finite transition relation. ( is the empty word in ?? and ? the empty word in ??.) Let u ? ??, then u is accepted by the pushdown automatonM = ?Q,?,?, q0, F, ?? if, starting with an empty stack at the initial state q0 and then reading u letter by letter, following the transition relation ? step by step, the process ends with an empty stack at a final state. Example 2.3.6 M = ?Q,?,?, q0, F, ?? is a pushdown automaton when 1. Q = {q0, qf} 2. ? = {0, 1} 3. ? = {A} 4. F = { qf } ; and 5. ? = {(q0, 0, ?, q0, A) , (q0, 1, A, q0, A) ,(q0, 1, A, qf , ?)} For example, the word 0111 is recognised byM. ? The transition relation of a pushdown automaton can also be denoted as a function: ? : Q ? (? ? {}) ? (? ? {?}) ? P (Q? (? ? {?})). The relation ? in example 2.3.6 would then be denoted as follows: ? ( q0, 0, A ) = {[q1, A]} ? ( q0, 1, A ) = {[ q0, A ] , [qf , ?]} A machine recognising pairs of words is required when cross-product monoids are considered. Definition 2.3.7 ([7, 36, 80]) A tuple T = ?Q,?,?, q0, F, ?? is called a transducer where ? and ? are the input and output alphabets respectively, Q a set of states, q0 ? Q a unique starting state, F ? Q a set of accepting states and ? the finite next-state relation satisfying: ? ? Q? ?? ? ?? ?Q. A run and an accepting run of a finite transducer are defined similar to a run and an accepting run for an automaton. 2.4. RECOGNISABLE, RATIONAL, AND REGULAR SETS 11 Example 2.3.8 For T = ?Q,?,?, q0, F, ?? let: 1. Q = {q1, q2}; 2. ? = {0, 1} = ?; 3. q0 = q1; 4. F = {q2}; and 5. ? = {(q1, 0, 0, q1) , (q1, 1, 1, q1) , (q1, , 0, q2) , (q1, , 1, q2)} Figure 2.2: The transducer T which recognises pairs of words of either the form (u, u0) or (u, u1) where u ? ?? and ux denotes the concatenation of the word u and the letter x. q1 q2 /0 /1 0/0 1/1 In the representation of T there is only one edge between two states but that an edge may have more that one label, i.e. the edge represents multiple transitions. (0100, 01000) and (0100, 01001) are examples of pairs of words recognised by T . ? 2.4 Recognisable, rational, and regular sets In this section I discuss two classes of subsets of arbitrary monoids. When the monoids are free and finitely generated by some alphabet, these are two classes of languages. Definition 2.4.1 ([80]) LetM1 = (M1, ?1, 1M1) be an arbitrary monoid and let A1 ? M1. The set A1 is called a recognisable subset of M1 if there exists a finite monoid, say M2 = (M2, ?2, 1M2), a morphism ? : M1 ? M2 and a subset A2 ? M2 such that A1 = ??1 (A2). Let REC (M) denote the set of all recognizable subsets ofM . Another, perhaps more natural characterisation of recognisable sets is in terms of the machines that recognise them. 12 CHAPTER 2. PRELIMINARIES Theorem 2.4.2 ([7, 80]) A subset A ? M of a monoid is recognisable if and only if it is recognised by some finite abstract automaton over M . Theorem 2.4.3 ([7, 80]) The class REC (M) of recognisable subsets of some monoid (M, ?, 1M ) is closed under the following operations: union, intersection, comple- mentation and set difference. It is also closed under inverse morphisms and isomorphisms. The next family of subsets under consideration can be defined by induction. Definition 2.4.4 ([7, 80]) Again let M = (M, ?, 1M ) be an arbitrary monoid. The family of rational subsets of M , denoted by RAT (M), is the least family R of subsets of M such that: 1. ? ? R; For all x ?M {x} ? R; 2. If X,Y ? R then X ? Y ? R and XY ? R; 3. If X ? R then X+ =?n?1Xn ? R. The next theorem now sums up the closure properties of this class of subsets: Theorem 2.4.5 ([7, 80]) The class RAT (M) of rational subsets of some monoid (M, ?, 1M ) is closed under the following operations: union, the monoid product operation, Kleene?s plus and star operations and morphisms. Proposition 2.4.6 ([7]) Any subset of a finite monoid is rational. Proposition 2.4.7 ([7]) If (M, ?, 1M ) is an arbitrary monoid, X ? RAT (M) and Y ? REC (M) then X ? Y ? RAT (M). The relationship between the recognisable and rational sets of a finitely generated monoid were given by McKnight in 1964. Theorem 2.4.8 (McKnight,[7]) If (M, ?, 1M ) is a finitely generated monoid, then REC (M) ? RAT (M). By imposing a stronger condition on the monoids considered, it can be proved that these two classes of subsets coincide. Theorem 2.4.9 (Kleene,[7, 36, 80]) If (M, ?, 1M ) is a finitely generated free monoid, i.e. there exists a finite alphabet ? such that M = ??, then a subset X ? M is recog- nisable if and only if it is rational. 2.4. RECOGNISABLE, RATIONAL, AND REGULAR SETS 13 Theorem 2.4.2 can now be rephrased since the automata now operate on words and therefore need not be in terms of abstract automata. Theorem 2.4.10 ([7, 80]) A language X ? ?? is rational/recognisable if and only it is accepted by some finite deterministic automaton. In fact, a language X is rational/recognisable if and only if it is accepted by some finite nondeterministic automaton [7]. The theorem above ensures that every rational subset is recognised by a finite deterministic automaton. This class of subsets is a class of languages over the alphabet known as the regular languages over the alphabet. When working on finitely generated free monoids the terms ?rational?, ?recognisable? and ?regular? can be used indistinctly. In the sequel I will use the term regular to emphasize that the monoid is finitely generated and free. A direct consequence of Kleene?s theorem is that all the closure properties of recognisable and rational subsets of monoids carries over to the class of regular subsets. Definition 2.4.11 ([84]) Let u ? ?? for some finite ?, then the reversal uR of u is the word obtained recursively by: 1. If u =  then uR = ; 2. If u = vx for v ? ?? and x ? ?, then uR = xvR. Definition 2.4.12 ([7, 36]) Let X,Y ? ?? for ? finite. The internal shuffle prod- uct of X and Y is the set: X t Y {u ? ??|u = a1b1a2b2 ? ? ? anbn, ai ? X, bi ? Y (i = 1, 2, . . . , n)} Theorem 2.4.13 The class REG (??) of regular sets of ?? is closed under the follow- ing operations: union, product, the Kleene star and plus operations, inter- section, set difference, the reversal operation, regular substitution, mor- phism, inverse morphism [7] and the internal shuffle product [36]. Denote the length of a word (string) u ? X by |u|. Regular sets also have the properties given below. Theorem 2.4.14 (Pumping lemma for regular sets, [7, 84]) Let X be a regular set recognised by the finite deterministic automaton A which has k states. If u ? X is any word such that |u| ? k, then u can be written in terms of some factors w1, w2, w3 ? ??, i.e. u = w1w2w3 where |w1w2| ? k, |w2| > 0 and w1wi2w3 ? X for all i ? 0. The pumping lemma serves as a powerful tool to prove that languages are not regular. To this end it suffices to give one word in the languages which does not satisfy the pumping lemma. 14 CHAPTER 2. PRELIMINARIES Theorem 2.4.15 ([80]) Suppose X,Y ? REG (??) is recognised by the finite deter- ministic automaton A where ? is finite. Then it is decidable whether X is empty, finite or infinite. It is also decidable whether X ? Y . 2.5 Recognisable, and rational relations The recognisable and rational subsets of cross-product monoids form useful classes of relations. For monoids (M, ?1, 1M) and (M ?, ?2, 1M ?), the class REC (M ?M ?) is called the class of recognisable binary relations on M?M ?. Likewise a binary relation on M?M ? is said to be rational if and only if it belongs to the class RAT (M ?M ?). Unless otherwise specified, all the relations in the sequel are assumed to be binary. An alternative characterisation in terms of regular languages exists for recognisable relations. Theorem 2.5.1 (Mezei, [7]) Let (M1, ?1, 1M1) and (M2, ?2, 1M2) be two arbitrary monoids. A subset of the cross-product monoid R ?M1?M2 is recognisable if and only if it is the union of finitely many sets of the form X?Y where X ? REC (M1) and Y ? REC (M2). Only the recognisable and rational subsets of the cross-product of two finitely gen- erated free monoids will be considered in the sequel. Then rational relations (subsets) can be characterised in terms of the machines recognising them. Theorem 2.5.2 ([7]) Let ? and ? be finite alphabets. A relation R ? ?? ? ?? is rational if and only if it is recognised by a finite transducer. Moreover, the existence of a specific type of transducer recognising each rational relation is guaranteed. Corollary 2.5.3 ([7]) Any rational relation R ? ????? can be recognised by a trans- ducer T = ?Q,?,?, qi, F, ?? such that ? ? Q? (? ? {})? (? ? {})?Q and furthermore, F consists of a single state qf 6= qi, and (p1, u, v, p2) ? ? implies p1 6= qf and p2 6= qi. In 1968 Nivat produced a theorem giving four conditions equivalent to a relation being a rational relation. Theorem 2.5.4 (Nivat, [74]) Let ? and ? be finite alphabets. The following are equivalent: 1. R ? RAT (?? ? ??); 2.5. RECOGNISABLE, AND RATIONAL RELATIONS 15 2. There exists an alphabet ?, two morphisms ?1 : ?? ? ??, ?2 : ?? ? ?? and a regular language X ? ?? such that R = {(?1 (u) , ?2 (u)) |u ? X} 3. There exists an alphabet ?, two alphabetic morphisms ?1 : ?? ? ??, ?2 : ?? ? ?? and a regular language X ? ?? such that R = {(?1 (u) , ?2 (u)) |u ? X} 4. There exists an alphabet ?, two alphabetic morphisms ?1 : ?? ? ??, ?2 : ?? ? ?? and a local regular language Y ? ?? such that R = {(?1 (u) , ?2 (u)) |u ? Y } If ? ? ? = ?, then (1) is equivalent to: 5. There exists a regular language X ? (? ? ?)? such that R = {(pi? (u) , pi? (u)) |u ? S} where pi? and pi? are the projections of (? ? ?)? onto ?? and ?? respectively. The last three conditions make use of alphabetic morphisms, local regular languages and projections. These concepts are not used in this study and therefore not defined here. Definition can however be found in [7, 80]. Nivat?s theorem can now be used to produce an iteration lemma for rational relations, which is similar to the pumping lemma for regular sets. Lemma 2.5.5 (Iteration lemma for rational relations, [7]) If R ? RAT (?? ? ??) where ? and ? are finite, then there exists an integer k ? 1 such that if (u, v) ? R with |u|+ |v| ? k, then (u, v) has a factorisation: (u, v) = (a1, a2) (b1, b2) (c1, c2) for a1, b1, c1 ? ?? and a2, b2, c2 ? ?? such that 1. 0 ? |b1|+ |b2| ? k; 2. (a1, a2) (b1, b2)? (c1, c2) ? R. The cross-product monoid of two finitely generated monoids is also finitely generated and therefore it follows from Theorem 2.4.8 that every recognisable relation is also rational. The closure properties described in theorem 2.4.3 and theorem 2.4.5 naturally also apply to the binary relations REC (?? ? ??) and RAT (?? ? ??) respectively. 16 CHAPTER 2. PRELIMINARIES Lemma 2.5.6 ([51]) If X ? RAT (??) then IX = {(u, u) |u ? X} ? RAT (?? ? ??). A rational relation R ? ?? ? ?? can also be seen as a function from ?? into the power set P (??), and is then called a rational transduction. The domain and the range of R are defined by: dom (R) = {u ? ??|R (u) 6= ?} ran (R) = {v ? ??|?u ? ?? : v ? R (u)} Nivat?s theorem can be reformulated for rational transductions. The following useful results are direct consequences of Nivat?s theorem Corollary 2.5.7 ([7]) If R ? RAT (?? ? ??) then dom (R) ? RAT (??) and ran (R) ? RAT (??). Corollary 2.5.8 ([7]) If R ? RAT (?? ? ??) and X ? RAT (??) then R (X) ? RAT (??). In fact, in the theorem above the first monoid need not be free - only the second monoid needs to be free for the result to hold ([36]). Theorem 2.5.9 (Elgot and Mezei, [37]) Let ?,? and ? be finite alphabets, R1 ? RAT (?? ? ??) and R2 ? RAT (?? ???). Then the relations R1 ? R2 ? ?? ? ?? is rational. In general the composition of rational relations does not preserve rationality, but the following result holds. Proposition 2.5.10 (Composition theorem, [7]) Let M1 and M2 be the carrier sets of arbitrary monoids and let ? be a finite alphabet. If R1 ? RAT (M1 ? ??) and R2 ? RAT (?? ?M2), then R1 ? R2 ? RAT (M1 ?M2) - where ? denotes the composi- tions of the relations which can be seen as functions into the power set of the second monoid. Since Elgot and Mezei?s theorem is used to prove this proposition, the condition that the two monoids are finitely generated and free is necessary. In conclusion I present a number of decidability results for recognisable, and rational relations. Definition 2.5.11 ([51]) A rational relation is length-bounded if there is some k ? N such that |v| ? k ? |u| ? |v|+ k for every (u, v) ? R Theorem 2.5.12 ([80]) Let R1, R2 ? RAT (?? ? ??) for finite alphabets ? and ?. Then it is decidable whether or not 1. R1 is finite; 2.6. MODAL LOGICS 17 2. R1 is empty; Theorem 2.5.13 ([80]) Let ? and ? be finite alphabets containing at least two letters and R1, R2 ? RAT (?? ? ??) then it is undecidable whether or not 1. R1 ?R2 = ?; 2. R1 ? R2; 3. R1 = R2; 4. R1 = ?? ? ??; 5. R1 is co-finite; 6. R1 recognisable. On the other hand, if R1, R2 ? REC (?? ? ??) the decision problems listed above become decidable. Finally: Theorem 2.5.14 ([51]) Given a finite transducer for a rational relation R, it is re- cursively undecidable whether R is transitive, symmetric, reflexive or an equivalence relation. On the other hand it is decidable whether or not R is a length-bounded ratio- nal equivalence relation. 2.6 Modal logics In order to be able to adequately describe and reason about relational structures, some- thing needs to be added to propositional languages which will be able to access the nec- essary information of the relational structure. By adding modalities (modal operators) to propositional languages, local properties of the structures can be described. 2.6.1 Syntax Definition 2.6.1 ([12]) Let ? = {p1, p2, . . . , pn} be a set of propositions. A formula ? is in the basic modal language K if it satisfies the rule: ? := p|?|??|? ? ?|3?, where 3 is a unary operator called the diamond operator, and p is an arbitrary element of ?. 18 CHAPTER 2. PRELIMINARIES A dual operator, called the box operator denoted by 2, can be defined for the diamond operator by setting 2? := ?3??. Furthermore the connectives conjunction, implication and bi-implication are abbreviations for the following formulas respectively: ? ? ? := ? (?? ? ??), ? ? ? := ?? ? ? and ? ? ? := (?? ?) ? (?? ?). The constant true, > will abbreviate ??. In the sequel a priority order will be imposed on the connectives, as for propositional logic, and unnecessary parentheses will be omitted. The priority order will be: 1. ?, 2 and 3 2. ? and ? 3. ? 4. ? Example 2.6.2 The following are examples of modal formulas: 1. 2 (2p? p)? 2p 2. ?3 (p ? q) ? (3p ?3q) 3. 32p? 23p ? Consider the formula 33 ? ? ?3 ? ?? ? n ? where the diamond operator is applied n ? 0 times. It can be abbreviated by defining the operator 3n = 33 ? ? ?3 ? ?? ? n . Furthermore, let 3? denote the reachability operator. K can be extended by adding various modal operators. Definition 2.6.3 [10, 91] A formula ? is in the basic tense language Kt if it sat- isfies the rule: ? := p|?|??|? ? ?|3?|3?1?, where p ? ? and 3?1 is a unary modal operator called the backwards diamond operator. The symbols ?R? and ?R?1? may also be used instead of 3 and 3?1. The gener- alization of what follows to the case of languages and models with many relations is straightforward. Temporal logics (see [63, 91]) are also very important extensions of the basic modal logic, used to express successive events along time. The two main frameworks within 2.6. MODAL LOGICS 19 which temporal logics have been studied are linear-time and branching-time. Linear- time temporal logic expresses properties over a single path in a model. The path is often referred to as a time line while branching-time temporal logic is the extension of linear-time temporal logics with path quantifiers A and E expressing ?along all paths? and ?along some path?. These extensions of the basic modal logic are very expressive and important properties such as liveness and safety properties can be expressed in them. Bounded model checking (see chapter 6) of rational Kripke models will provide a method of partial model checking of temporal logic formulas. 2.6.2 Semantics The languages defined above still have no context or interpretation. Modal languages must be interpreted in relational structures (relational structures are tuples contain- ing a nonempty set called the universe and a number of relations on that universe). This is called relational semantics. There are two levels at which modal languages can be interpreted. The first is the level of frames and the second the level of models. Definition 2.6.4 A Kripke frame is a pair F = (S,R) such that S is non-empty, called the universe, and R is a binary relation on S, i.e. R ? S ? S. Definition 2.6.5 M = (S,R, V ) is a Kripke model if (S,R) is a Kripke frame and V : ?? P (S) is a function that assigns a subset of the universe to each propositional variable. A model M can also be written as a pair (F , V ) where F = (S,R) is a Kripke frame. Then M is said to be based on F . Furthermore, let L : S ? P (?) be the function defined by: L (x) = {p ? ?|x ? V (p)} where x ? S. Example 2.6.6 Let S = N and if x, y ? N then xRy if and only if y = x + 2. Then the relational structure F = (S,R) is a Kripke frame. Suppose ? = {p, q} and define V : ?? P (S) to be the function: V (p) := {x ? N|x = 2k, k ? N} V (q) := {y ? N|y = 2k + 1, k ? N} ThenM = (F , V ) is based on F . ? It is not enough to just define relational structures. How to interpret these modal languages on Kripke structures must also be defined. 20 CHAPTER 2. PRELIMINARIES Definition 2.6.7 ([12]) Let M = (S,R, V ) be a Kripke model and let s ? S. Then satisfaction of a formula ? in Kt inM at s is inductively defined by: M, s |= p ?? s ? V (p) , for p ? ? M, s |= ? never M, s |= ?? ?? it is not the case thatM, s |= ? M, s |= ? ? ? ?? M, s |= ? orM, s |= ? M, s |= 3? ?? there is some t ? S such that sRt andM, t |= ? M, s |= 3?1? ?? there is some t ? S such that tRs andM, t |= ? Note that the relation R is not assumed transitive, and therefore the language of Kt cannot express R-reachability properties. On the otherhand, Kt can express local properties. Example 2.6.8 LetM be the model defined in Example 2.6.6 and let ? = 3p. Then M, 2 |= ? andM, 3 2 ?. ? A single R (respectively, R?1) step is made by 3 (3?1), while 3n ((3?1)n) makes n R (R?1) steps, i.e. M, s |= 3n? ?? there is some t ? S such that sRnt andM, t |= ? and M, s |= (3?1)n ? ?? there is some t ? S such that s(R?1)n t andM, t |= ? where Rn ((R?1)n) denotes the composition of R (R?1) with itself i.e. R?R (R?1?R?1) n times. The box operators are interpreted in the following way. M, s |= 2? ?? for every t ? S such that sRt it holds thatM, t |= ? M, s |= 2? ?? for every t ? S such that tRs it holds thatM, t |= ? 2.7 Bisimulation A bisimulation (bisimulation equivalence) is a relation between two Kripke structures that preserves atomic information and transition possibilities ([83]). Bisimulation will prove its usefulness here when modal formulas expressing reachability need to be model checked. Definition 2.7.1 ([12]) Let F1 = (W1, R1) and F2 = (W2, R2) be Kripke frames. A bisimulation (bisimulation equivalence) between F1 and F2 is a non-empty binary relation B ? W1 ?W2 such that the following conditions hold for B: 2.8. PETRI NETS 21 1. If (x, y) ? B then ?x? ? R1 (x) ?y? ? R2 (y) such that (x?, y?) ? B. (This is known as the forth condition and expresses that every transition inM1 can be matched by a transition inM2.) 2. If (x, y) ? B then ?y? ? R2 (y) ?x? ? R1 (x) such that (x?, y?) ? B. (This is the back condition and expresses that every transition inM2 can be matched by a transition inM1.) If M1 = (F1, V1) and M2 = (F2, V2) are two Kripke models based on F1 and F2 respectively, then the non-empty binary relation B ? W1?W2 is a bisimulation between M1 andM2 if: 1. B is a bisimulation from F1 to F2, and 2. if (x, y) ? B then V ?1 (x) = V ?2 (y). (Related states have identical atomic informa- tion) Bisimulation relations are used to define bisimilarity between structures. Definition 2.7.2 ([47]) Let F = (W,R) be a Kripke frame and let w ? W . Then the pair (F , w) is a pointed Kripke frame. Likewise, if M is a Kripke model based on F , then the pair (M, w) is a pointed Kripke model. Definition 2.7.3 ([47]) Let G and H be two Kripke frames (models), with universes W1 and W2 respectively. If x ? W1 and y ? W2, then the pointed frames (models) (G, x) and (H, y) are bisimilar or bisimulation equivalent, if there is a bisimulation B between G and H such that B relates x and y, i.e. xBy. Definition 2.7.4 ([47]) If B is a bisimulation between two Kripke structures G and H, such that every element in G is related to some element in H and vice versa, then B is a global bisimulation between the two structures, and G and H are said to be globally bisimilar. 2.8 Petri nets In this section a class of models, namely that of Petri nets, is introduced. Petri nets are often used to describe and study systems which are characterised as concurrent or asynchronous. Furthermore, Petri nets admit effective verification tasks. For these and other reasons this class of models have been studied extensively in the literature. In the next chapter it will be explained how the configuration graphs of Petri nets can be seen as rational Kripke frames (rational graphs). However, they are not merely an interesting subclass of rational Kripke frames - Janc?ar?s result on the undecidability of bisimilarity for petri nets will be used to establish a similar result for rational Kripke models. 22 CHAPTER 2. PRELIMINARIES Definition 2.8.1 ([2, 49, 61, 67]) A (labeled) net is a tuple (Nl = (P, T, F, L)) N = (P, T, F ) where P and T are finite disjoint sets - the elements of P are called places and those of T transitions; F : (P ? T ) ? (T ? P ) ? N is called the flow function and there is an arc from x to y if F (x, y) > 0 with F (x, y) being the mul- tiplicity of that arc. For a labeled net L : T ? A is a labeling that assigns an action name from the finite set A of actions to each transition. The places in a net can contain tokens - objects added to a net in order to describe its dynamics. The distribution of these tokens in the places of the net defines its configuration state. For the purpose of this study it can be safely assumed that the tokens do not represent specific information and are indistinguishable. Definition 2.8.2 ([2, 61, 67]) A marking M is a function M : P ? N that assigns to each place in a net the number of tokens residing at that place. A marking can also be seen as a finite vector of nonnegative integers where the ith component of M is equal to the number of tokens at the ith place in the net. Definition 2.8.3 ([2, 49, 61, 67]) A (labeled) Petri net is a tuple N = (N,M0) where N is a (labeled) net and M0 is the initial marking of the net. The distribution of the tokens changes by a process called the firing of transitions. A marking M enables a transition t if M (p) ? F (p, t) for all p ? P where F (p, t) > 0. If the transition t is enabled by the marking M the transition may fire, yielding a new marking M ? such that for all p ? P M ? (p) = M (p)? F (p, t) + F (t, p). The firing of a transition t is denoted by M t?N M ?. For labeled Petri nets M a ?N M ? where a ? A is an action name, denotes that M t?N M ? for some transition t such that L (t) = a. Example 2.8.4 Let Nl = (P, T, F, L) be the labeled net such that P = {p1, p2, p3, p4}, T = {t1, t2} and F is given by: F (p1, t1) = 3 F (t1, p2) = 1 F (t1, p3) = 1 F (p2, t2) = 2 F (p3, t2) = 1 F (t2, p4) = 1 and F (p, t) = 0 for all other combinations of t ? T and p ? P . Finally, if A = {a, b}, let L be the labeling given by L (t1) = a and L (t2) = b. Now, let M0 be the marking given by (when seen as a finite vector of nonnegative integers) (3, 1, 0, 0). N = (Nl,M0) is a labeled Petri net. The graph in figure 2.3 represents N . The graphs in figures 2.4 and 2.5 represents the Petri net after the first and the second transition are fired respectively. (Places are represented by circles while the transitions are represented by rectangles.) M0 (p1) = 3 = F (p1, t1) which means that the transition t1 is enabled by M0. The marking obtained after t1 is fired is given by M1 = (0, 2, 1, 0). 2.8. PETRI NETS 23 M1 (p2) = 2 = F (p2, t2) and M1 (p3) = 1 = F (p3, t2) which means that M1 enables t2. After t2 is fired the marking M3 = (0, 0, 0, 1) is obtained. Figure 2.3: The Petri net N = (Nl,M0). p1 p2 p3 p4 t1 a t2 b Figure 2.4: N after transition t1 is fired. p1 p2 p3 p4 t1 a t2 b Figure 2.5: N after transition t2 is fired. p1 p2 p3 p4 t1 a t2 b ? The markings and firing of transitions can now be used to define the configuration graph of a Petri net. Definition 2.8.5 ([67]) The configuration graph (marking graph) G of a Petri net N is the graph G = (M, Rt) where M is the set containing all valid markings of N and R a ordered binary relation relating a marking M to a marking M ? if and only if there is a transition enabled by M that yields M ? when it is fired. 24 CHAPTER 2. PRELIMINARIES Chapter 3 Rational Kripke Structures 3.1 Rational graphs In this section I give a formal definition of rational graphs and present a brief survey of the most important results on this class. This class has been studied by Johnson in [51] and by Morvan in [69, 70]. Definition 3.1.1 A graph is a pair G = (S,E) where S is the set of vertices of G and E is a binary relation on S, called the set of edges of G. Intuitively rational graphs are defined as below: Definition 3.1.2 A graph G = (S,E) is a rational graph, if the set of vertices S is a regular subset of some finitely generated free monoid ?? and the set of edges E is a rational relation on ??. Labeled rational graphs are simply graphs where there are more than one, but finitely many, edge relations. In this case each edge relation is given a label from some finite alphabet ?. From the properties of rational relations (see Chapter 2 on page 14) it then follows that a graph with vertices in ?? is rational if and only if its relation is recognised by a finite transducer. In the case of labeled rational graphs, it must be recognised by a labeled finite transducer. Example 3.1.3 ([69]) The infinite grid is one of the best known rational graphs1. Let ? = {0, 1}, then the infinite grid with vertices in ?? is the graph given by figure 3.1. The edge relation of this graph is recognised by the finite transducer given in figure 3.2. ? 1The transducer given here corrects the transducer given by Morvan 25 26 CHAPTER 3. RATIONAL KRIPKE STRUCTURES Figure 3.1: The infinite grid with set of vertices S = 0?1?.  0 00 1 11 01 001 011 0011 Figure 3.2: A transducer that recognises the infinite grid. q1 q2 q3 q4 /1 /0 1/01 0/0 1/1 0/0 1/1 Example 3.1.4 ([77]) Another very important example of a rational graph is the com- plete binary tree ?. If ? = {0, 1} and ? = {a, b}, then the graph in figure 3.3 is the complete binary tree with vertices in ?? and labeled by ?, while figure 3.4 is the finite labeled transducer recognising it. ? 3.1.1 Results on rational graphs A number of results on rational graphs are given below - some of which are translations of well-known results for rational relations (see Chapter 2). Proposition 3.1.5 ([69]) Every rational graph is recursive: it is decidable whether a specific edge belongs to the graph or not. Proposition 3.1.6 ([69]) It is decidable whether or not a rational graph is determin- 3.1. RATIONAL GRAPHS 27 Figure 3.3: The complete binary tree ?.  a b 0 1 a b 00 01 a b 10 11 Figure 3.4: A labeled transducer recognising the complete binary tree ?. q1 q2 q3 q4 q5 0/0 1/1 0/0 1/1 0/0 1/1 /1 /0 /0 /1/0 /1 a b istic - from its transducer. A rational graph is deterministic if and only if the associated relation on each letter is functional. But functionality is decidable for rational relations. Proposition 3.1.7 ([69, 7]) The inclusion and equality of deterministic rational graphs is decidable. Consider the following questions: 1. Fix a first-order formula ?. Given a rational graph G as input, is ? satisfiable on G? 2. Fix a rational graph G. Given a first-order formula ? as input, is ? satisfiable on G? Negative results have been obtained in answer of both of these questions. 28 CHAPTER 3. RATIONAL KRIPKE STRUCTURES Definition 3.1.8 Let ? be a finite alphabet and (u1, v1) , (u2, v2) , . . . , (un, vn) be ele- ments in ?????. Does there exist a sequence of indecis 0 ? i1, i2, . . . , im ? n such that u1ui1ui2 ? ? ? uin = v1vi1vi2 ? ? ? vin? This is known as Post?s Correspondence Problem abbreviated by PCP. The halting problem for Turing machines is reducible to the PCP and hence the PCP is undecidable. Theorem 3.1.9 ([69]) The problem of establishing for a first order formula, given as input a rational graph G whether or not ? is satisfiable on G is undecidable. Proof.[69] In particular Morvan shows that the query ?x (xRx) on rational graphs is undecidable: Given an instance {(u0, v0) , . . . , (un, vn)} of the PCP, associate the transducer in figure 3.5 with it. Figure 3.5: A transducer associated with an instance of the PCP. q1 q2 u0/v0 ui/vi for i ? {1, 2, . . . , n} Then this instance of the PCP has a solution precisely if a pair (w,w) is accepted by the transducer, i.e. if the first-order formula ?x (xRx) is satisfiable on the graph G which has the relation recognised by the transducer in figure 3.5. qed In fact, in [51], Johnson shows that simple first-order definable properties like reflex- ivity, transitivity and symmetry of a rational relation turn out to be undecidable (with the transducer recognising the relation as input). This was also shown by reduction from the PCP. Theorem 3.1.10 ([86]) There is a single rational graph G for which the problem of establishing whether or not a given first-order formula ? is satisfiable in G is undecid- able. The details of the proof of this result will be discussed later in this chapter when the model checking of a hybrid extension of the basic tense logic is condidered. A very important property to verify for structures is reachability. The following result has been obtained with respect to reachability: 3.1. RATIONAL GRAPHS 29 Theorem 3.1.11 ([69]) Reachability (accessibility) is not decidable for rational graphs. This problem can also be reduced to the PCP and therefore undecidability follows. Definition 3.1.12 [27] The trace of a graph G labeled by ?, from a set of initial vertices I to a set of final vertices F is the language { w ? ?|?u ? I, ?v ? F ( u w ? ? v )} where u w?? v denotes that there is a path in G from vertex u to vertex v such that the concatenation of the labels of the edges in the path forms the word w. Proposition 3.1.13 [27] The traces of rational graphs are exactly the context-sensitive languages. This result was extended by Rispal in [78] to a subclass of rational graphs, namely automatic graphs which will be studied in Chapter 4. Definition 3.1.14 ([66]) Given a vertex u in a graph G, the out-degree (respectively, in-degree) of u is the number of different successors (different predecessors) u has. The degree of u is the sum of its in- and out-degrees. The degree of the graph G is the largest degree over all its vertices, if it exists, otherwise it is said to be infinite. A well-known result for rational relations by Autebert and Boasson in [3] translates into the characterisation of rational graphs with finite out-degree given below. Proposition 3.1.15 ([69]) A rational graph G is of finite out-degree if and only if there exists a transducer T that recognises the relation of G such that every cycle in T labeled with  as input, is labeled with  as output. (i.e. the concatenation of all the input labels on the cycle is just the empty word, then so must the concatenation of all the output labels on the cycle be.) For such graphs with finite out-degree Morvan presents the following property on the growth rate of the out-degree of rational graphs: Theorem 3.1.16 ([69]) For any rational graph G of finite out-degree and any vertex u there exists c ? N, such that the out-degree of vertices at distance n of u is at most cc n . Example 3.1.17 ([66]) Consider the transducer T in figure 3.6. The graph recognised by it is presented in figure 3.7. It consists of infinitely many disconnected subgraphs - only two of which are displayed in the figure2. The vertices of this graph have out-degree 22n+1 at a distance n from any chosen vertex u. ? 2Meyer only displays the first subgraph and makes no reference to the remaining subgraphs. 30 CHAPTER 3. RATIONAL KRIPKE STRUCTURES Figure 3.6: The finite transducer T . qi 0/10 0/11 0/00 0/01 1/10 1/11 1/00 1/01 Figure 3.7: A finite degree rational graphs with the vertices at a distance n from any chosen vertex u having out-degree 22n+1 . 0 1 00 01 10 11 0000 . . . 1000 . . . 1111 0000000 . . . 10001000 . . . 11111111 000 . . . 100 . . . 111 000000 . . . 100000 . . . 111111 . . . Conversely, Meyer also presents a result for the in-degree: Theorem 3.1.18 ([66]) For any rational graph G of finite in-degree and any vertex u there exists a c ? N such that ccn is an upper bound for the in-degree at distance n from u. This follows from the fact that the inverse of a rational relation is itself a rational relation. These properties can be used to show that some classes of graphs are strictly in- cluded in the class of rational graphs, or incomparable with the class of rational graphs. Proposition 3.1.19 ([69]) The configuration graph of a Petri net is a rational graph. Proof. Let N = (P, T, F,M0) be a Petri net with P = {p1, p2, . . . , pn} and T = {t1, t2, . . . , tm} (recall that P and T are both finite by definition). The configuration graph C = (M, R) can now be obtained as follows: In the alphabet {p1, p2, . . . , pn} a 3.2. INTRODUCING RATIONAL KRIPKE STRUCTURES 31 marking M = (k1, . . . , kn) can be represented by the word pk11 pk22 . . . pknn . M is then the set of all finite words in the alphabet (note that this set is more than is required) and R is the relation obtained by the union of the m relations associated with the transitions in N . They are of the form: for 1 ? i ? m let Ri = { pk11 p k2 2 . . . pknn ti ? pl11 p l2 2 . . . plnn } where ti? denotes the firing of the transition ti. For each i ? {1, 2, . . . , n} the relation Ri is rational: since F is a function, i.e. F (pj, ti) and F (ti, pj) have fixed values for each j ? {1, 2, . . . , n}, the value dij = F (ti, pj) ? F (pj, ti) is also fixed. If dij > 0, then let uj =  and vj = pdijj . Else, if dij < 0 let uj = p|dij |j and vj = . Then the relation Ri is recognised by the transducer in figure 3.8. Consequently Ri is a rational relation by Theorem 2.5.2. But then R is the union of a finite number of rational relations and hence R is itself a rational relation. Figure 3.8: The transducer recognising the relation Ri associated with the transition ti. q1 q2 q3 p1/p1 p2/p2 p3/p3 u1/v1 u2/v2 u3/v3 qed 3.2 Introducing rational Kripke structures In Chapter 2 Kripke frames and models (collectively referred to as structures) were in- troduced as the relational structures in which modal languages are interpreted. Rational Kripke structures is a subclass of these structures which are introduced by Goranko in [46]. Definition 3.2.1 F = (S,R) is a rational Kripke frame if there is a finite alphabet ? such that S ? REG (??) and the relation R is rational, i.e. R ? RAT (?? ? ??). From the definition of rational Kripke frames it follows that they form exactly the class of rational graphs. Hence, all the properties and characterisations of rational graphs carry over to rational Kripke frames. Definition 3.2.2 A Kripke model M = (F , V ) = (S,R, V ) is a rational Kripke model if the frame F , on which it is based, is a rational Kripke frame, and the valuation 32 CHAPTER 3. RATIONAL KRIPKE STRUCTURES V assigns a regular language to each propositional variable, i.e. ?p ? ?, V (p) ? REG (??). A valuation satisfying this condition is called a rational valuation. In order for these structures to be useful, they must be effectively finitely pre- sentable. Proposition 3.2.3 ([46]) The class of rational Kripke frames (respectively models) are finitely presentable. Proof. Let F = (??, R) be a rational Kripke frame. Since ? ? REG (??) there is a finite automaton recognising it (see Theorem 2.4.10 on page 13). Furthermore, the rational relation R is recognised by a finite transducers by Theorem 2.5.2. Therefore, F is effectively finitely presentable. If M = (F , V ) now is a rational Kripke model based on F , then all that remains is to show that the valuation V is effectively finitely presentable. The set ? is finite, and V (p) ? REG (??) , ?p ? ?. Thus, V can be presented by a finite number of finite automaton, completing the proof. qed Example 3.2.4 In this example I will present a rational Kripke model based on the configuration graph of a Petri net. Let N = (P, T, F,M0) be a Petri net where P = {p1, p2}, T = {t} and M0 = (2, 2). The flow function is defined by: F (p1, t) = 1, F (t, p2) = 2 and F (t, p1) = F (p2, t) = 0. Let ? = {A,B} and ? = {q1, q2}. Now let M = (S,R, V ) be the Kripke model where S = A?B?, R is the transition relation of N and V is the valuation defined by V (q1) = A+BB+ and V (q2) = A?B+. ThenM is a rational Kripke model which can be presented by the various machines in figure 3.9. ? 3.3 Model checking Model checking is verifying properties of a system specified in some formal language in an algorithmic way. Originally model checking was only developed for finite state systems [30, 31] (see also [32] for more on model checking). However, verification problems can be formulated as algorithmic problems for infinite state systems if the systems are finitely presentable - thus making them model checking problems. In the case of finite systems, doing model checking is always decidable. There is however the problem of state space explosion to complicate matters. For infinite state systems, decidability of model checking is not guaranteed. Thus the aim is to identify classes of structures (systems) on which certain model checking problems do turn out to be decidable. The main problem here is that it is always a trade-off between expressiveness of the formal language and decidability of model checking properties specified in the 3.3. MODEL CHECKING 33 Figure 3.9: A finite presentation M: A1, A2 and A3 recognises S, V (q1) and V (q2) respectively, and T recognises R. A1: q1 q2 A B  A2: p1 p2 p3 A B A BB A3: r1 r2 BA B T : s1 s2 s3 A/A B/B A/ /BB aforementioned language. For a larger class of structures expressiveness of the language, in which the properties are specified, needs to be sacrificed in order to retain the decidability of the model checking of these properties. On the other hand, insisting on high expressive power will automatically reduce the class of structures on which decidability is guaranteed. In this section I am particularly interested in decidable model checking tasks on ra- tional Kripke structures. In chapter 4 subclasses of rational Kripke structures, for which model checking problems in more expressive languages are decidable, are investigated. There are a number of computational tasks, i.e. model checking problems, for modal languages which can be performed on Kripke structures ([46]): 1. Model checking tasks for Kripke models: (a) Local model checking: Determine whether or not M, s |= ? for M a Kripke model, s a state inM and ? a formula. (b) Global model checking: Determine the set of all states where a formula ? is true in a Kripke modelM. Denote the set of all such states by [|?|]M. (c) Satisfiability checking: Determine whether or not [|?|]M = ? for a Kripke modelM and a formula ?. 2. Model checking tasks for Kripke frames: (a) Local validity checking: Determine whether or not F , s |= ? for all possible valuations V on F . 34 CHAPTER 3. RATIONAL KRIPKE STRUCTURES (b) Global validity checking: Determine the set of state in a Kripke frame F at which a formula ? is valid. (c) Rational validity checking: Determine whether or not F , s |= ? for all rational valuations on F . 3.3.1 Synchronised products of transducers and automata Work in this section, as well as the following four sections, appear in [6] co-authored by myself and Goranko. The synchronised product of a transducer and an automaton is introduced in this section. This concept will be used when the model checking of Kt-formulas is considered on rational Kripke models. However, some additional terminology must be introduced before the synchronised product of a transducer and an automaton can be defined. In this section  will denote the empty word, but will also be treated as a special symbol in an extended alphabet. Definition 3.3.1 ([6]) Let u be a word in some alphabet ? and ? ? ?. The ?- reduction of u, denoted u|?, is the word obtained from u after deleting all occurrences of ?. Likewise, if Y is a language in the alphabet ?, then the ?-reduction of Y , denoted Y |?, is the language consisting of all ?-reductions of words in Y . Lemma 3.3.2 ([6]) If Y is a regular language over an alphabet ? then Y|? is a regular language over the alphabet ?? {?}. Proof. An automaton A|? recognising Y|? , called here the ?-reduction of A can be constructed from an automaton A recognising Y as follows: 1. remove all ?-transitions; 2. add (q, ??, q??) as a transition in A|? whenever (q, ?, q?) and (q?, ??, q??) are transi- tions in A and ? 6= ??; 3. Finally, define the accepting states of A|? as all accepting states of A plus those states q such that (q ??? q?) in A and q? is an accepting state in A. qed Example 3.3.3 Let ? = {0, 1, 2} and A the automaton given in figure 3.10. Then the automaton in figure 3.11 is the 2-reduction of A, i.e. A|2. The transitions (p4, 2, p2)) and (p2, 2, p5) are removed from A, the transitions (p4, 1, p4) and (p2, 0, p3) added and p4 is made an accepting state. ? 3.3. MODEL CHECKING 35 Figure 3.10: The automaton A before reduction p1 p2 p3 p4 p5 0 1 0 2 0 1 2 Figure 3.11: The automaton A|2, the 2-reduction of A p1 p2 p3 p4 p5 0 1 0 0 0 1 1 Definition 3.3.4 ([6]) A stuttering run of a finite automaton A = ?Q,?, q0, F, ?? is a sequence q0 x1 ? q1 x2 ? q2 ? ? ? xn ? qn, such that q0 = q0, qj ? Q, and either xj ? ? and qj ? ? (qj?1, xj), or xj =  and qj = qj?1 for every j = 1, 2, . . . , n. Thus, a stuttering run of an automaton can be obtained by inserting -transitions from a state to itself into a run of that automaton. If the latter run is accepting, the stuttering run is said to be an accepting stuttering run. A stuttering word in an alphabet ? is any word in ? ? {}. The stuttering language of the automaton A is the set L(A) of all stuttering words whose -reductions are recognised by A; equivalently, all stuttering words for which there is an accepting stuttering run of the automaton. 36 CHAPTER 3. RATIONAL KRIPKE STRUCTURES Definition 3.3.5 ([6]) Let T = ?QT ,?, q0T , FT , ?T ? be a transducer (here the input and output alphabets coincide, i.e. ? = ?.3), and let A = ?QA,?, q0A, FA, ?A? be a(non-deterministic) finite automaton. The synchronised product of T with A is the finite automaton: T iA = ?QT ?QA,?,(q0T , q0A) , FT ? FA, ?TiA? where ?TiA : (QT ?QA)? (? ? {})? P(QT ?QA) is such that, for any p1T , p2T ? QT and p1A, p2A ? QT then (p2T , p2A) ? ?TiA ((p1T , p1A) , x) if and only if 1. either there exists a y ? ? such that ?A (p1A, y) = p2A and (p1T , x, y, p2T ) ? ?T ; 2. or (p1T , x, , p2T ) ? ?T and p1A = p2A. Note that every run RTiA = (p0T , p0A) u1? (p1T , p1A) u2? ? ? ? un? (pnT , pnT ) of the automa- ton T iA can be obtained from a pair: a run RT = p0T (u1/w1) ? p1T (u2/w2) ? p2T ? ? ? (un/wn) ? pnT in T , and a stuttering run RsA = p0A w1 ? p1A w2 ? p2A ? ? ? wn ? pnA in A, by pairing the respective states pjT and p j A and removing the output symbol wj for every j = 1, 2, . . . , n. Let the reduction of RsA be the run RA = q0A v1 ? q1A v2 ? q2A ? ? ? vm ? qmA , with m ? n. Then the run RTiA is a synchronisation of the runs RT and RA. Note, that the synchronisation of accepting runs of T and A is an accepting run of RTiA. The following lemma is now immediate: Lemma 3.3.6 ([6]) Let T = ?QT ,?, q0T , FT , ?T ? be a transducer recognising the rela- tion R(T ) and let A = ?QA,?, q0A, FA, ?A? be a finite automaton recognising the lan- guage L(A). Then the language recognised by the synchronised product of T and A is L(T iA) = {u | ?w ? L(A)(uR(T )w)}. Example 3.3.7 Consider the transducer T and the automaton A given in figures 3.12 and 3.13 respectively. The regular language X = 1? (1 + 0+) is recognised by A, while R = {(1n0, 10n1)m(1k, 10k) |n,m, k ? N}? {(1n0, 10n1)m(01k, 11k) |n,m, k ? N} is the relation recognised by T . Then their synchronised product T i A is the fi- nite automaton given in figure 3.14. (This automaton can be simplified by removing redundant states and edges.) ? 3Henceforth ? = ?, i.e. the input and output alphabets of transducers considered coincide - unless explicitly specified otherwise 3.3. MODEL CHECKING 37 Figure 3.12: The transducer T used in the synchronised product. T : q1 q2 q3 /1 0/1 0/1 1/0 1/1 Figure 3.13: The automaton A used in the synchronised product. A : p1 p2 p3 0 1 1 0 Figure 3.14: The synchronied product T iA. T iA : q1,p1 q1, p2 q1, p3q2, p1 q2, p2 q2, p3 q3,p1 q3, p2q3, p3  0 0 1 1  0 0 1 1 3.3.2 Model checking of Kt in rational Kripke models Finally, the three model checking tasks for formulas from Kt can be considered in rational Kripke models. 38 CHAPTER 3. RATIONAL KRIPKE STRUCTURES Lemma 3.3.8 ([6]) Let ? be a finite non-empty alphabet, X ? ?? a regular subset, and let R ? ?? ? ?? be a rational relation. Then the sets ?R?X = {u ? ??|?v ? X(uRv)} and ? R?1 ? X = {u ? ??|?v ? X(vRu)} are regular subsets of ??. Proof. This claim essentially follows from Nivat?s theorem (see Theorem 2.5.4). How- ever, using lemmas 3.3.2 and 3.3.6 a constructive proof is given in which automata that recognise the resulting regular languages are explicitly produced: for ?R?X that is the -reduction of the synchronised product of T with A; for ?R?1?X the transducer for R?1 is used instead of T . This transducer is obtained from T by swapping the input and output symbols in the transition relation. Note that, in general the resulting automata may have redundant states and tran- sitions. qed Example 3.3.9 Recall the synchronised product of the automaton recognising the regular language X = 1? (1 + 0+) and the transducer recognising the rational relation: R = {(1n0, 10n1)m(1k, 10k) |n,m, k ? N}? {(1n0, 10n1)m(01k, 11k) |n,m, k ? N} , given in figure 3.14, example 3.3.7. From lemma 3.3.8 it now follows that this synchro- nised product recognises exactly the regular language ?R?X = 0? + 0?1+. ? Theorem 3.3.10 ([46]) Local and global model checking of formulas in Kt in rational Kripke models are decidable. Moreover, for every formula ? ? Kt and rational Kripke modelM, the set [|?|]M is an effectively computable rational language. Proof. LetM = (??, R, V ) be a rational Kripke model over a finite alphabet ? and ? ? Kt. The set [|?|]M is a regular language, by induction on ?: 1. When ? is an atomic proposition, the claim follows from the definition of a rational model. 2. The boolean cases follow from the closure of regular languages under boolean operations. 3. If ? = ?R?? then [|?|]M = ?R? [|?|]M, which is regular by the inductive hypothesis and lemma 3.3.8. Likewise for the case ? = ?R?1??. Finally, decidability of the local model checking follows from the decidability of the non-emptiness of a regular language. qed 3.3. MODEL CHECKING 39 3.3.3 Complexity The complexity of global model checking a formula in Kt on a given rational Kripke model is now analysed, i.e., the expression complexity [58] of Kt on rational Kripke models. A formula ? ? Kt is in negation normal form if every occurrence of the negation immediately precedes a propositional variable. Clearly every formula ? ? Kt is equiv- alent to a formula ? ? Kt in negation normal form, of size linear in the size ?. For the remainder of this section, a formula ? which is to be model checked is assumed to be in a negation normal form. The number of edges in a finite automaton or transducerM is denoted by |M|. Lemma 3.3.11 ([6]) If A is an automaton recognising the regular language X and T a transducer recognising the rational relation R, then O(|T |m|A|) is an upper bound for the time complexity of computing an automaton recognising ?R?mX. Proof. The size of the synchronised product T iA of T and A is bounded above by |T ||A| and it can be computed in time O(|T ||A|). The claim now follows by iterating that procedure m times. qed However, the conjecture is that the time complexity of computing an automaton recognising [R]X is far worse. For a regular languageX recognised by an automatonA, defineRX = {(u, ) |u ? X}. A transducer T recognising RX can be constructed from A by simply replacing every edge (q, x, p) in A with the edge (q, x, , p). Lemma 3.3.12 ([6]) Let X be a regular language. Then the complementation X of X equals [RX ]?. Proof. [RX ]? = {u ? ??|RX (u) ? ?} Thus, [RX ]? will contain only those words in ?? with no RX successors, i.e. exactly the set X. qed Consequently, computing [RX ]? cannot be done in less than exponential time in the size of the (non-deterministic) automaton A for X. This result suggests the following conjecture: Definition 3.3.13 ([6]) The alternating box rank and alternating diamond rank of a formula ? ? Kt, denoted respectively by ar[R](?) and ar?R?(?), are defined by si- multaneous induction as follows, where M? {[R] , ?R?}: 1. if p is an atomic proposition, then arM (p) = 0; 40 CHAPTER 3. RATIONAL KRIPKE STRUCTURES 2. ar[R] (??) = ar?R? (?) and ar?R? (??) = ar[R] (?); 3. arM (?1 ? ?2) = max {arM (?1) , arM (?2)}; 4. ar?R? (?R??) = ar[R] (?) + 1 and ar[R] (?R??) = ar[R] (?). 5. ar[R] ([R]?) = ar?R? (?) + 1 and ar?R? ([R]?) = ar?R? (?). The alternating box (diamond) rank of a formula counts the greatest number of nested alternations of modalities with an outmost box (diamond) in the formula. Conjecture 3.3.14 ([6]) The expression complexity of global model checking of a Kt- formula is non-elementary in terms of the alternating box rank of the formula. 3.3.4 Hybrid logics Hybrid languages One of the main shortcomings of the Kt is its inability to refer to the states of a Kripke structure. Modal semantics evaluate modal formulas at some state in the model, but using standard modal languages, the states themselves cannot be referred to. A remedy to this problem was introduced in the form of hybrid logics. For more on hybrid logics see [11]. In its basic form, a hybrid language is an extention of K or Kt with a new set of symbols which enables one to refer to specific states in a model. Definition 3.3.15 ([11]) Let ? be a set of propositional variables and let ? be a set of symbols called nominals, such that ??? = ?. A formula ? is in the basic hybrid language Ht if it satisfies the rule ? = p | i |??|? ? ?|3?|3?1? where 3 is the unary diamond operator in modal languages, p ? ? and i ? ?. Hence, the only difference between Kt and Ht is the addition of a second type of atomic formula, namely the nominals. The Kripke frames on which hybrid languages are interpreted, called hybrid frames, are exactly the same as the frames on which Kt is interpreted. On the level of models the valuation must be altered slightly: let M = (F , V ) be a hybrid model based on the hybrid frame F , then V is the function V : ? ??? P (S) where S is the domain of the model. A nominal must be true at exactly one state in the model, i.e. V (i) is a singleton for every nominal i in ?. The unique state in V (i) is called the denotation of i. Therefore, if M = (S,R, V ) is a hybrid model and w ? S, then the formula ? = i for i ? ? is satisfied at w in M, i.e. M, w |= i if and only if V (i) = {w} (w is the denotation of i). 3.3. MODEL CHECKING 41 Example 3.3.16 Consider the following formula: 3i. This formula simply states that the denotation of the nominal i is one of the successors. It will be satisfied at all predecessors of the denotation of i. This simple formula expresses a property which cannot be expressed in the basic modal language since there is no way to refer to specific states. ? The basic hybrid language can be extended in a number of ways. Firstly, introduce a unary operator for each nominal i in ?. This makes it possible to evaluate formulas at a specific point. Definition 3.3.17 ([11]) A formula ? is in the hybrid language Ht (@) extended with unary operators - one for each nominal - if it satisfies the rule: ? = p | i |??|? ? ?|3?|3?1?|@i? with i ? ?. The ?@i? operators are called the satisfaction operators. The new formula @i? is read ?? is true at i?. For the modelM (as used earlier in this section), the formula ? = @i? is satisfied at w inM, i.e. M, w |= ? if and only if M, w? |= ? where w? is the denotation of i. Example 3.3.18 The formula ? = @i (3j ? p) with i, j ? ? and p ? ? is another example of a very simple formula showing the increase of expressiveness. Let w ? S, then M, w |= @i (3j ? p) if and only if for V (i) = {w?} it holds that M, w? |= 3j ? p. This formula expresses that the state w? has the denotation of j as a successor and w? ? V (p). Note that the state at which the evaluation of ? is done, does not play a role in the satisfaction. Therefore, formulas of the form @i? are either valid or invalid depending on wheter the formula ? is satisfied at the denotation of i. Next consider the formula: @i?? ?@i?? This formula is valid on all frames and shows that each satisfaction operator is its own dual. Furthermore, the following formula is valid on all hybrid frames for any nominal i and shows that the satisfaction operators act like normal modal operators. @i (?? ?)? (@i?? @i?) ? An even more expressive extension of Ht is obtained when the universal modality [U] is added to the language. 42 CHAPTER 3. RATIONAL KRIPKE STRUCTURES Definition 3.3.19 A formula ? is in Ht (U) if it satisfies the rule: ? = p | i |??|? ? ?|3?|3?1?| [U ]? Semantically: Let M = (S,R, V ) be a hybrid model, then M, v |= [U ]? ?? M, w |= ? for every w ? S. Furthermore, the satisfaction operators @i are definable inHt (U): @i? := [U ] (i? ?). Hybrid languages provide a way to access states which naturally leads to a possible further extension: introduce state variables and then bind these variables to states. Definition 3.3.20 Let Ht (U, ?) be the extension of Ht (U) with the binder. It also contains a new type of atomic formula, namely a set of state variables ?. A formula ? is in Ht (U, ?) if it satisfies the rule: ? = p | i |??|? ? ?|3?|3?1?| [U ]?| ? x.? Satisfaction of formulas in this form is a bit more involved. Let M be a hybrid Kripke model. For a formula ? containing only unbounded occurrences of a state variable x, where w is a state in the model, let ? [x? iw] denote substituting x with the nominal iw in ? where iw is such that w is its denotation. Then the satisfaction of these formulas is defined by: M, w |=? x.? ?? M, w |= ? [x? iw] Ht (U, ?) is a lot more expressive than Ht (U). Example 3.3.21 ? x.@i3x This formula is true at the set of states which are successors of the denotation of the nominal i. ? Model checking of hybrid languages on rational Kripke models Having introduced hybrid languages, an obvious question to ask is whether or not model checking of hybrid logic formulas is decidable. First observe that, as in the case of propositional variables, it is safe to assume that the set of nominals ?, added to the language Ht (U), is finite, since every formula must have finite length and can therefore only contain finitely many nominals. Proposition 3.3.22 ([6]) Global and local model checking the formulas of the hybrid language Ht (U) is decidable on rational Kripke models. As with the basic modal lan- guage the set [|?|]M is effectively computable for every formula ? and every rational Kripke modelM = (S,R, V ). 3.3. MODEL CHECKING 43 Proof. This language contains two new types of formulas: the atomic formulas i with i ? ? and formulas of the form [U ]? where ? is some hybrid formula. For formulas in Ht (U) also contained in Kt the claim follows from Theorem 3.3.10. The set V (i) for i ? ? is a singleton by the definition of nominals. Therefore, [|i|]M is a regular set for every atomic formula i. Next consider a formula of the form [U ]? and suppose [|?|]M is a regular set. If[|?|]M = S then [| [U ]?|]M = S, otherwise [| [U ]?|]M = ?. Either of these are regular sets and the result follows. qed Proposition 3.3.23 ([6]) Model checking the Ht (U, ?)-formula ?x. ?R? x on a given input rational Kripke model is not decidable. Proof. This is an immediate consequence from the earlier mentioned Morvan?s reduc- tion [69] in theorem 3.1.9 of the model checking of ?xRxx to the Post Correspondence Problem. qed Proposition 3.3.24 ([6]) There is a rational Kripke model on which model checking formulas from the hybrid language Ht (U, ?) is undecidable. Proof. I now present the proof by Thomas [87] where he shows that there is a single rational graph with an undecidable first-order theory. I will then show that the condi- tion under which the instance of the PCP has a solution, can not only be expressed by a first-order sentence, but also by a formula in Ht (U, ?). Thomas uses a universal Turing machine M and the encoding of its undecidable halting problem (for different input words u) into a family of instances of the PCP: A Turing machine M with input word u is converted into a PCP instance {(u0, v0) , . . . , (um, v,m)} over an alphabet ?, such that ? contains the state and tape letter of M as well as the symbol # used to separate between M-configurations in M-computations. If the input word is u = a1 ? ? ? an then u0 is the initial configuration word c (u) =#q0a1 ? ? ? an of M. Furthermore, it is always the case that v0=# and u1, . . . , um, v1, . . . , vm only depend on M. Then M halts on the input word u if and only if the PCP instance {(c (U) ,#) , (u1, v1) , . . . (um, vm)} has a solution. Now let G be the rational graph defined from these PCP instances as in the proof of Theorem 3.1.9: The vertices are the words over ?, and there is a single edge relation R such that (w1, w2) ? R if and only if there are indices i1, . . . , il such that w1 = 44 CHAPTER 3. RATIONAL KRIPKE STRUCTURES c (u) ui1 ? ? ? uil and w2 = #vi1 ? ? ? vil . The graph G is rational and has an edge form a word to itself if the instance of the PCP has a solution. To be able to refer to the input word u explicitly in the graph, further vertices and edge relations Rx for x ? ? are added. A c (u)-labeled path via the new vertices will lead to a vertex of G with prefix c (u). If the latter vertex has an edge back to itself a solution for the PCP instance {(c (U) ,#) , (u1, v1) , . . . (um, vm)} can be inferred. The new vertices are words over a copy ? of ?. The alphabet ? consists of un- derlined versions of the letters in ?. For any word c (u) vertices which arise from the underlined versions of the proper prefixes of c (u) are added. In addition a Rx-edge from an underlined word w to a word wx is introduced (also for the case where w = ). There are also edges to non-underlined words: there is a Rx-edge from the underlined version of w to any non-underlined word which has wx as a prefix. The resulting graph is now called G ?. By construction of G ?, the PCP instance {(c (U) ,#) , (u1, v1) , . . . (um, vm)} has a solution if and only if there is a path in G ?, labeled with the word c (u), from the vertex  to a vertex which has an edge back to itself. This conditions can be expressed by a first-order sentence. It can also be expressed by a formula in Ht (U, ?): The vertex  is definable as the only one with outgoing Rx edges but without an ingoing edge of one of the relations Rx: ? x. ( n? i=1 ? ? R?1xi ? x ) ? ( n? i=1 ?Rxi? x ) A path labeled with the word c (u) to a vertex which has an edge back to itself can then be expressed by: ?Ra1? ?Ra2? ? ? ? ?Ran? ? y. ?R? y. The claim then follows. qed 3.4 Regularity preserving relations The fact that the set ?R?X is regular for a rational relation R and a regular set X, sparks the interest to find out what relations satisfy this property, to study them and to explore some of their properties. This leads to the definition below. Definition 3.4.1 A relation R ? ?? ? ?? is regularity preserving if for every regular language X ? REG (??), ?R?X is a regular language. Proposition 3.4.2 A relation R is regularity preserving if and only if the set [R]X is regular for every X ? REG (??). 3.4. REGULARITY PRESERVING RELATIONS 45 Proof. This follows from the fact that [R] is the dual of ?R?, i.e. [R]? = ? ?R? ??. If X ? REG (??) then X ? REG (??) and ?R?X ? REG (??) ?? ?R?X ? REG (??) ?? ?R?X = [R]X ? REG (??) qed Furthermore, for a relation R and a set X it holds that: ?R?X = {u ? ??|?v ? X (uRv)} = R?1 (X) Since ?R?X is a regular language for all X ? REG (??) if R is a rational relation, it follows that every rational relation is a regularity preserving relation. Question 3.4.3 Is every regularity preserving relation a rational relation? Implicitly, the question asked is whether or not there are frames outside of the class of rational Kripke frames for which the model checking of Kt is decidable? The answer to this question is no - there is at least one regularity preserving relation which is not rational. Proposition 3.4.4 Let R = {(xn, ynxn) |n ? 0}. Then ?R?X = R?1 (X) for any X ? REG (??), is a regular language. Proof. Firstly observe that R?1 (X) = R?1 (X ? {ynxn|n ? 0}). A well-known closure property of context-free languages is that the intersection of a context-free language with a regular language is a context-free language [84]. Thus, to prove this claim, I will determine the form of the context-free language L = X ? {ynxn|n ? 0} and then show that the inverse image of L is a regular language. LetM = ?Q1,?,?, q0, F1, ?1? be a pushdown automaton recognising {ynxn|n ? 0}, such that: Q1 = { q0, q1 } ? = {x, y} ? = {Y } F1 = {q0, q1} and ?1 ( q0, y, ? ) = {[ q0, Y ]} ?1 ( q0, x, Y ) = {[q1, ?]} ?1 (q1, x, Y ) = {[q1, ?]} Furthermore, let A = ?Q2,?, p0, F2, ?2? be a finite deterministic automaton that recog- nises the languageX. Using the proof given in [84] that the intersection of a context-free and regular language is context-free, a pushdown automaton can be constructed which 46 CHAPTER 3. RATIONAL KRIPKE STRUCTURES recognises the language L: LetN = ?Q,?,?, (q0, p0) , F, ?? be the pushdown automaton where Q = Q1 ?Q2, F = F1 ? F2 and ?p ? Q2 ? (( q0, p ) , y, ? ) = {[( q0, p? ) , Y ] |?2 (p, y) = p?} ? (( q0, p ) , x, Y ) = {[(q1, p?) , ?] |?2 (p, x) = p?} ? ((q1, p) , x, Y ) = {[(q1, p?) , ?] |?2 (p, x) = p?} From every state in N where q0 is the first component, there are two outgoing edges labeled with x and y respectively. From each state in N with q1 as the first component there is exactly one outgoing edge labeled with an x. This follows from the determinism of the automaton A. If an edge labeled with x or y is followed from one state to another, respectively x or y is read. Clearly all computations must start from the state (q0, p0). Starting at the state (q0, p0) a path can be followed along which every state has q0 as first component, the states passed are pairwise distinct and the path is labeled by a string of y?s. Let the maximum length of such a path be k1 where 0 ? k1 ? |Q2|. Label the states visited by this path of length k1 with A0 to Ak1 according to the number of y?s read to reach the state. Now start at the state (q0, p0) and follow any path p labeled by a string of y?s. Let i be the length of this path. 1. For each i, 0 ? i ? k1, the singleton {yixi} is accepted by N , if and only if the state (q1, p), the state reached after i y?s and then i x?s are read, belongs to F . (It will always be possible to read i x?s form the determinism of the automaton.) Observe that i = 0 is the only case where q = q0, and in fact then p = p0. For all other i, q = q1. 2. If i > k1 let Ac1 be the label of the state reached after k1+1 y?s are read. Observe that 0 ? c1 ? k1. This will require that p ends at one of the states numbered between c1 and k1. Suppose the state labeled by Al is reached, clearly then l y?s were read, after which some multiple of the cycle was read, where m1 = k1+1?c1 is the length of the cycle. Let (q0, p) be the state labeled by Al. If x is read i times it means that the unique edge from (q0, p) to some state (q1, p?) must be followed after which, as before, a finite number of distinct states can be reached until a cycle must be followed. Say k2 distinct states can be reached from (q0, p) (this includes (q1, p?)), then label each of these states with Bj for 1 ? j ? k2. Let c2 be the number such that after reading k2+1 x?s from (q0, p), the state labeled by Bc2 is reached. Thus the cycle reached will have length m2 = k2 + 1? c2. Let t = lcm (m1,m2) then the length of the path p is i = n+st for n = 0, 1, . . . , t? 1 and s ? 0 from number theory. This means that there are t?1 languages of the form {yn (yt)s xn (xt)s |s ? 0} that may be accepted by this pushdown automaton. 3.4. REGULARITY PRESERVING RELATIONS 47 Thus, the context-free language consists of the union of a finite number of sets of the form {yn (yt)s xn (xt)s |s ? 0} and singletons. The inverse image of a singleton is clearly a singleton while the inverse image of a set {yn (yt)s xn (xt)s |s ? 0} is the set {xn (xt)s |s ? 0} which is a regular language. Thus, the inverse image of the language L is the union of a finite number of regular languages - which is regular itself. qed Example 3.4.5 Let X = y (y3)? x (x2)?. For the pushdown automaton constructed using a deterministic automaton for X, it follows that k1 = 3, c1 = 1 and m1 = 3. Then, in the case where i < k1, only the {xy} is accepted by this pushdown au- tomaton. Furthermore, k2 = 2, c2 = 1 and m2 = 2. This means that t = lcm (m1,m2) = 6 and that the languages { yn (y6)s xn (x6)s |s ? 0} for n = 1, 2, . . . , 5 are the languages that may possibly be accepted by the pushdown automaton. Of these only the language{ y (y6)s x (x6)s |s ? 0} is accepted. The inverse image of this language is the language given by { x (x6)s |s ? 0}? {x} which is a regular language. ? The next point of interest is the closure properties of this class of structures. The next theorem presents some positive results. Theorem 3.4.6 The class of regularity preserving relations is closed under union and composition. Proof. Let R1 and R2 be two regularity preserving relations, i.e. for every X ? REG (??) the languages [R1]X and [R2]X are regular. 1. Union: [R1 ?R2]X = {u ? ??| (R1 ?R2) (u) ? X} = {u ? ??| (R1 (u) ?R2 (u)) ? X} = {u ? ??|R1 (u) ? X ?R2 (u) ? X} = [R1]X ? [R2]X This is the intersection of two regular languages, which is itself a regular language. 2. Composition: [R1 ?R2]X = {u ? ??| (R1 ?R2) (u) ? X} = {u ? ??|R1 (R2 (u)) ? X} = {u ? ??|?v ? R2 (u) (R1 (v) ? X)} = {u ? ??|R2 (u) ? {v ? ??|R1 (v) ? X}} = {u ? ??|R2 (u) ? [R1]X} = [R2] [R1]X 48 CHAPTER 3. RATIONAL KRIPKE STRUCTURES But [R1]X is regular language since R1 is regularity preserving. Therefore, it follows from the fact that R2 is regularity preserving that [R1 ?R2]X is a regular language. qed The negative results concerning closure properties now follow: Theorem 3.4.7 The class of regularity preserving relations is not closed under in- tersection, complementation or inverse. Proof. Let R1 = {( ykxn, xn ) |n, k ? 0} and let R2 = {(ynxk, xn) |n, k ? 0}. Then both R1 and R2 are rational relations and therefore regularity preserving. 1. Intersection: The relation R1 ?R2 = {(ynxn, xn) |n ? 0} is not rational and thus it does not necessarily follow that it is regularity preserving. In fact it is not, since ?R1 ?R2? {x}? = {ynxn|n ? 0} which is not a regular language. 2. Complementation: Although rational relations are generally not closed under complementation, the complements of R1 and R2 are both rational relations: R1 = ?? ? (??\ {x}?) ? (, x)? (x, ) ((x, ) + (y, ))? (y, ) ((x, ) + (y, ))? ? (, x)? ((x, ) + (y, ))? (y, )? (y, )? (x, x)? (, x)+ (y, ) ((x, ) + (y, ))?? (, x)+? (y, )? (x, x)? ((x, ) + (y, ))+ ? (y, )? (x, x)? (, x)+ R2 = ???(??\ {x}?)?(x, ) ((x, ) + (y, ))? (, x)??(y, x)? (y, )+ ((x, ) + (y, ))?? (y, x)? (, x)+ (x, )+ ((x, ) + (y, ))? ? (, x)+ ? (y, x)? (x, )? (y, ) ((x, ) + (y, ))? Since rational relations are closed under union, the relation R1 ? R2 is again a rational relation and therefore regularity preserving. But R1 ? R2 = R1 ?R2 which means that R1 ?R2 is regular and by 1 above, the complement of R1?R2, i.e. R1 ?R2 is not regularity preserving. 3. Inverse: Consider the inverse of the regularity preserving relation given in example 3.4.4: R = {(ynxn, xn) |n ? 0}. This is the same relation as in 1 which is not regularity preserving. qed 3.4. REGULARITY PRESERVING RELATIONS 49 3.4.1 An algebraic view These two classes of rational relations and regularity preserving relations enjoy a num- ber of closure properties under some opererations and naturally give rise to algebraic structures. Two new types of relational algebra can now be defined. Definition 3.4.8 A regularity preserving algebra is an algebra A = (R,+, ; , I) satisfying the axioms: for R1, R2, R2 ? R: 1. R1; (R2;R3) = (R1;R2) ;R3 2. R1; I = R1 = I;R1 3. (R1 +R2) ;R3 = R1;R3 +R2;R3 Proposition 3.4.9 The set regularity preserving relations and with the operations ?+? and ?;? interpreted as union and composition respectively and I is the identity relation, form a regularity preserving algebra. Definition 3.4.10 A rational algebra is an algebra A = ( R,+, ; ,? , I ) such that (R,+, ; , I) is a regularity preserving algebra and the additional axioms are satisfied: for R1, R2, R2 ? R 1. ( R?1 ) ? = R1 2. (R1 +R2)? = R?1 +R?2 3. (R1;R2)? = R?2;R?1 Proposition 3.4.11 The set of rational relations forms a rational algebra where ?+?,?;? and ?I? interpreted as in Proposition 3.4.9 and ? interpreted as the inverse. These definitions are needed since neither the regularity preserving relations nor the rational relations form a Boolean algebra (it is not closed under intersection and complementation) and consequently neither of these classes form relation algebras as defined in [22]. Having considered the diamond modal operations and their duals, it becomes appar- ent that an algebra describing a class of relations? interaction with sets will be useful. Besides the modal operators, set operators on sets and relations include: 1. Domain: D = {x|?y (xRy)} 2. Range: W = {y|?x (xRy)} 3. Image: R (X) = {y|?x ? X (xRy)} 50 CHAPTER 3. RATIONAL KRIPKE STRUCTURES 4. Pierce Product: R : (X) = {x|?y ? X (xRy)} In fact, the Pierce product is equivalent to the diamond operation. Moreover, the other operations can be defined in terms of the Pierce-product [22]. In [21] algebras of relations interacting with sets via the Pierce product, called boolean modules, are introduced. The regularity preserving relations as well as the rational relations can however not be used to form boolean models since neither of these classes of relations form relation algebras. Instead, two new two-sorted algebras are defined below. Definition 3.4.12 A regularity preserving- (respectively, rational-) Boolean algebra is a two-sorted algebra A = (R,S, :) where R is a regularity preserving (ratio- nal) algebra, S is a boolean algebra and ?:? is a mapping R?S ? S denoted by R : X such that for any R1, R2 ? R and any X1, X2 ? S the following holds: 1. R1 : (X1 +X2) = R1 : X1 +R1 : X2 2. (R1 +R2) : X1 = R1 : X1 +R2 : X1 3. R1 : (R2 : X1) = (R1;R2)X1 Proposition 3.4.13 The class of regularity preserving (respectively, rational) relations over a finite alphabet ?, together with the class of regular sets over ? (which is a Boolean algebra), form a regularity preserving- (rational-) Boolean algebra. This now enables one to reason about these classes of relations algebraically. 3.5 Rationally presentable structures When talking about structures, it is important to distinguish between abstract struc- tures, and structures with a certain presentation. The same abstract structure may exhibit different properties in different presentations. Example 3.5.1 Recall the counterexample given in the previous section to illustrate that regularity preserving relations are not closed under intersection i.e. the relation R = {(xn, ynxn) |n ? 0}. The fact that this relation is not included in the class of rational relations, greatly depends on the language used and the words assigned to each state in the structure which is equipped with this relation. Let S be the abstract structure under consideration, then figure 3.15 gives this graph with the presentation discussed above. If the states are given labels from a different alphabet, or even just different labels from the same alphabet, the resulting relations may be rational. For example, the fol- lowing presentation can be given to S: let R = {(xn, yn) |n ? 0}. Figure 3.16 describes this graphically. 3.5. RATIONALLY PRESENTABLE STRUCTURES 51 Figure 3.15: A presentation of S which is not rational.  x yx x2 y2x2 x3 y3x3 . . . Figure 3.16: A rational presentation of S.  x y x2 y2 x3 y3 . . . Observe that this graph has the same structure as the previous one - the states have simply been relabeled. To see that this graph is rational observe that it is recognised by the transducer in figure 3.17. Figure 3.17: The transducer reconising R = {(xn, yn) |n ? 0}. q x/y ? In the example above, it is apparent that an abstract structure may have a rational presentation - though not all of its presentations may be rational. The term presentation here refers to the labeling of elements of the abstract structure with words over some alphabet. This calls for the introduction of a new notion that will handle this property. Definition 3.5.2 An abstract structure S = ?D,R1, . . . , Rn? is said to be rationally presentable if it is isomorphic to some rational Kripke frame (rational graph). Thus, the abstract structure in example 3.5.1 is rationally presentable, since it is isomorphic to the rational Kripke frame given in figure 3.16 52 CHAPTER 3. RATIONAL KRIPKE STRUCTURES Distinguishing between these concepts also effects the way relations and their prop- erties are considered. Rational relations have been defined in Chapter 2, but that was within the presentation of the finitely generated free monoid obtained from some finite alphabet. A stronger property can now be identified for relations of abstract structures. Definition 3.5.3 A relation in an abstract structure, is intrinsically rational if, for any regular presentation of the structure, the relation is rational in that presentation. Example 3.5.4 Every finite relation is intrinsically rational. ? In [69] Morvan refers to the concept of a graph being rationally presentable as being structurally rational. He provides an external characterization of rational graphs which produces graphs without assigning names to the vertices. This is done up to isomorphism. The following will be needed for Morvan?s alternate characterisation. Definition 3.5.5 ([69]) A context-free language X ? ?? (see Chapter 2 page 7) is a linear language if it is generated by a grammar which has at most one non-terminal symbol on the right hand side of each of its rules. Definition 3.5.6 Given a graph G = (S,R) and a language X, the restriction of G to X is the graph G|X = ( S|X , R|X ) where S|X = S ?X and R|X = R ? (X ?X). If the language X is a regular language, the restriction is called rational. Definition 3.5.7 A substitution over a free monoid ?? is a morphism ? : ?? ? P (??). Moreover, it maps a language L ? ?? to each letter in ?. Now consider the complete binary tree, ?, given in example 3.1.4. It is labeled by ?1 = {a, b}. In addition use the new alphabet ??2 = {a?,?b} to label the inverse arcs, i.e. x is related to y by Ra? if and only y is related by x by Ra. Given a substitution ? : ?? ? P (?1 ? ?2)? define the graph ??1 (?) by: ??1 (?) = {uRdw|d ? ?, there is a path in ? labeled by ? (d) from u to w} Now let L be a language and define L? = {v| there is a path in ? labeled by a word in L from the rootr to v} . Then the graph ??1 (?)|L? is the image of an inverse substitution of the complete binary tree followed by a restriction. Finally, if ? is a substitution such that ? (d) is a linear language for every d ? ? then ? is called a linear substitution. Furthermore, if the ? (d) is a linear language such that the projections over barred and non-barred letters are rational for every d ? ?, then the languages are called rational-linear and the substitution is also rational-linear. 3.6. MODEL CONSTRUCTIONS 53 Theorem 3.5.8 ([27]) A graph is rationally presentable if and only if it is isomor- phic to a graph obtained from the complete binary tree ? by an inverse rational-linear substitution, followed by a rational restriction. 3.6 Model constructions Model checking of reachability in rational graphs is generally undecidable - as discussed earlier in this chapter. This means that model checking of the formula ?R?? p in a given rational Kripke model as an input is undecidable. Since reachability is the single most important property in infinite-state verification, this fact limits essentially the usability of rational Kripke models for representation and symbolic verification of reachability in infinite transition systems. One way to deal with this problem, is to consider model constructions that do not affect truth of modal formulas expressing reachability. This may enable one to effectively reduce the problem of model checking reachability to model checking reachability in better behaved models where reachability can be com- puted effectively. In [12] disjoint unions, generated submodels, bounded morphisms and ultrafilter extensions are described as ?the big four? operations on Kripke models that do not effect modal satisfaction. A natural question to ask is whether the class of rational Kripke models is closed under these operations. I will answer questions on the first two of these operations as well as the unfolding of models. 3.6.1 Disjoint unions Definition 3.6.1 Two models are disjoint if their domains are disjoint. Let Mi = (Wi, Ri, Vi) be disjoint models for i ? I. Their disjoint union is the model ?iMi =(W,R, V ) where W is the union of the sets Wi, R is the union of the relations Ri and for each p ? ?, V (p) = ?i?I Vi (p). In the case of frames, simply ignore the clause concerning valuations. Question 3.6.2 Is the finite disjoint union of rational Kripke models again a rational Kripke model? If the set I of indices is finite, then the answer to this question is ?yes?. Since the domains are disjoint, it is safe to assume without the loss of generality that the domains contain words over disjoint alphabets, i.e. Wi ? ??i for i ? I. Suppose Wi ? REG (??i ) and Wj ? REG ( ??j ) and ? = ?1 ? ?2 for i, j ? I and i 6= j. Then Wi,Wj ? ?? and moreover they are regular since any regular expression of an alphabet is also a regular expression of an extended alphabet. An alphabet can now be constructed such that for each i ? I the set Wi is a regular set over this alphabet. In this same way the rational relations will also be rational 54 CHAPTER 3. RATIONAL KRIPKE STRUCTURES relations of the extended alphabet. The claim follows from the closure of regular sets and rational relations under finite union. 3.6.2 Generated substructures Definition 3.6.3 Let F = (W,R) and F ? = (W ?, R?) be two Kripke frames, then F ? is a subframe of F if W ? ? W and R? is the restriction of R to W ? i.e. R? = R ? (W ? ?W ?). F ? is a generated subframe of F if F ? is a subframe of F and for all points w ? W the following closure condition holds: If w ? W ? and wRv then v ? W ?. For a model M? = (F ?, V ?) to be a submodel of a model M = (F , V ) the frame F must be a subframe of F and V ? is the restriction of V to W ? i.e. for each p ? ?, V ? (p) = V (p)?W ?. Thus,M? is a generated submodel ofM if it is a submodel and it satisfies the closure condition. Question 3.6.4 Given a rational set X, is the submodel (subframe) of a rational Kripke model (frame) generated by X again a rational model (frame)? Proposition 3.6.5 Given a rational set X, then it is not necessarily the case that the subframe (submodel) of a rational Kripke frame (model) generated by X is again a rational Kripke frame (model). Proof. Consider the rational Kripke frame F , given in Example 3.1.17 on page 29. Let X = {0}. Then the subframe of F generated by X is given in figure 3.18. The set of states of the generated subframe is the set Y = {u ? {0, 1}? |l (u) = 2i, i > 0} ? {0}, containing words with length equal to a power of 2. Suppose Y is regular, then by the pumping lemma, it is possible to express a word u of sufficient length in terms of some factors u1, v and u2 such that every word in u1v?u2 belongs to Y . Since v must be non-empty, it is easy to see that any such expression will produce words which are not of length equal to some power of 2 and therefore not in Y . Therefore Y is not regular. Since the domain of a rational relation is regular (Theorem 2.5.7), the relation of the generated subgraph cannot be rational. qed 3.6.3 Unfoldings Consider the labeled graph G = (S, {Ea}a??) where ? is some finite alphabet of labels. If the set S is finite then the graph is finite, and since every finite set is a regular set, the graph G is a rational graph and therefore a rational Kripke frame. Now, a labeled path in G is a sequence p = (v0, a1, v1, . . . , ak, vk) where ai ? ?, vi ? S and vi?1Eaivi 3.6. MODEL CONSTRUCTIONS 55 Figure 3.18: The subframe generated by the regular set X = {0}. 0 00 01 10 11 0000 . . . 1000 . . . 1111 0000000 . . . 10001000 . . . 11111111 for i = 1, 2, . . . , k. Let f (p) denote the final vertex of the path p. Lastly, denote the set of all paths in the graph G starting at a vertex v0 by P (v0). Definition 3.6.6 The tree unfolding of a graph G = (S, {Ea}a??) is the labeled graph T (G, v0) = (P (v0) , {Epa}a??} where the relation Epa is defined by: Epa := {(p, p ? (a, u)) |p ? P (v0) , f (p)Eau} where the operation denoted by ? is path concatenation. Question 3.6.7 Is the unfolding of a finite Kripke frame always a rational Kripke frame? The answer to this question is ?yes? as explained below. Definition 3.6.8 A tree is a regular tree if and only if it has only finitely many non-isomorphic subtrees. Proposition 3.6.9 The unfolding of a finite Kripke frame is a rational Kripke frame. Proof. While studying Caucal?s hierarchy, Thomas observes in [87] that the set of tree unfoldings of finite graphs is the set of regular trees. Following Caucal?s hierarchy, the class of regular trees are included in the class of prefix-recognisable graphs ([87]). However, in [69] Morvan observes that prefix recog- nisable graphs are included in the class of rational graphs proving the claim. qed In the case of rational Kripke models it is necessary to first describe how the tree unfolding effects the valuation. 56 CHAPTER 3. RATIONAL KRIPKE STRUCTURES LetM = (G, V ) be a rational Kripke model based on the rational Kripke frame G, then the tree unfolding ofM is the Kripke model given by T (M, v0) = (T (G, v0) , V1) where the valuation V1 is given by V1 (p) = {p|f (p) ? V (p)} for p ? ?. Question 3.6.10 Is the unfolding of a finite Kripke model always a rational Kripke model? Again the answer is ?yes?. It has already been shown that tree unfolding preserves rational Kripke frames. Therefore, all that remains to establish is whether or not tree unfoldings preserve the rationality of the valuations. The valuation V1 of a propositional variable contains all the finite paths in a finite graph that end at a state in the regular set V (p). In fact, the set V (p) is finite since the graph is finite. For each state in V (p) the set of paths ending in it is regular since a regular expression can be given for it: It is the union of a finite number of regular sets of the form: v0 ((a1v1)? + (a1v1)) . . . ((akvk)? + (akvk)) where vk ? V (p) and (aivi)? is in the expression if the edge forms a loop. There are finitely many since there are only finitely many edges in G to follow. Thus, V1 (p) is a finite union of regular sets and therefore regular itself. 3.7 Bisimulation Another very important type of relation between models is bisimulation. In fact, the bisimulation preserves the satisfaction of the entire modal ?-calculus - making it a particularly important type of relation to study. The work in the following two subsections also appears in [6]. 3.7.1 Bisimulation between two rational Kripke structures. Consider the following two algorithmic problems: Question 3.7.1 Are two given pointed rational Kripke frames (respectively, models) bisimilar? Question 3.7.2 Are two given rational Kripke frames (respectively, models) globally bisimilar? 3.7. BISIMULATION 57 Definition 3.7.3 A counter machine C is a program containing non-negative counters c1, c2, . . . , cm and commands S1, S2, . . . , Sn, where Sn is the halting command and for 1 ? i < n the command Si is of the form: Si : cj := cj + 1; go to k or Si : if cj = 0 go to k1 else cj := cj ? 1 and go to k2 for 1 ? k, k1, k2 ? n, 1 ? j ? n and ?:=? denoting assignment. A counter machine starts off performing command S1. Proposition 3.7.4 ([6]) It is undecidable whether two given pointed rational Kripke models are bisimilar. Proof. Firstly recall that the configuration graphs of Petri nets are rational Kripke frames (Proposition 3.1.19). In [49], Janc?ar proved that global bisimilarity is undecid- able for labeled Petri nets by constructing, for a fixed (universal) 2-counter machine and a pair of input values, a pair of labeled Petri nets such that their configuration graphs are bisimilar if and only if the counter machine does not halt for the given input. The claim then follows by constructing two rational Kripke models based upon the configuration graphs of the Petri nets from Janc?ar?s proof. I will now present the details of Janc?ar?s construction. Let C be a fixed (universal) counter machine with two counters c1, c2 and commands S1, S2, . . . , Sn, for which the halting problem is undecidable. A net that simulates C can now be constructed. Constuction 3.7.5 Let N = (P, T, F, L) be the labeled net obtained as follows: Let P = {c1, c2, s1, . . . , sn, p, p?}. Assume that all of the places are empty, i.e. they don?t contain any tokens. Adding an arc (q, t) to the net means to increment F (q, t) with one. Begin with T = ? and for each transition t added, let F (q, t) = 0 and F (t, q) = 0 for all q ? P . Transitions and arcs will now be added to the net using the following rules: For 1 ? i < n, 1 ? k, k1, k2 ? n and 1 ? j ? n 1. If command Si is of the form Si : cj := cj + 1; go to k then add the transition ti to the net, as well as the arcs (si, ti) , (ti, cj) and (ti, sk). Let the label be L (ti) = ai 2. If command Si is of the form Si : if cj = 0 goto k1 else cj := cj ? 1 and go to k2 58 CHAPTER 3. RATIONAL KRIPKE STRUCTURES (a) add transition tNZi and arcs ( si, tNZi ) , ( cj, tNZi ) and ( tNZi , sk2 ) to the net. Let L ( tNZi ) = aNZi . (b) add transitions tZi , t?i and t??i to the net. Also add the following arcs: i. ( si, tZi ) and ( tZi , sk2 ) ii. (p, t?i) , (t?i, p?) , (p?, t??i ) and (t??i , p) iii. (si, t?i) , (si, t??i ) , (t?i, sk1) , (t??i , sk1) , (t?i, cj) , (t??i , cj) , (cj, t?i) and (cj, t??i ) Let L ( tZi ) = L (t?i) = L (t??i ) = ai. 3. Lastly, add the transition tF with the label aF and the arcs (sn, tF ) and (p, tF ). Figure 3.19: The net N constructed to simulate C. Suppose Sc is a command of the first type using c1 and Sd of the second type using c2 where 1 ? c, d < n. c1 c2 sc tc sk sd p? p sk1 sk2tNZd tZd t?d t??d sn tF Janc?ar showes that bisimilarity is undecidable for the Petri nets N1 = (N,M1) and N2 = (N,M2), where N is the net constructed above and M1,M2 are the markings M1 = ??x1, x2, 1, 0, . . . , 0 ? ?? ? n , 1, 0 ?? M2 = ??x1, x2, 1, 0, . . . , 0 ? ?? ? n , 0, 1 ?? where the places are arranged in the order {c1, c2, s1, . . . , sn, p, p?}. The values x1 and x2 are the input values for C. 3.7. BISIMULATION 59 Observe that the only difference between these two Petri nets is their initial mark- ings. Hence, their configuration graphs will be exactly the same graph. Let C be that graph. Then it is undecidable whether the pointed rational Kripke frames (C,M1) and (C,M2) are bisimilar or not. qed In [50] Janc?ar and Srba prove the undecidability of bisimilarity for prefix rewrite systems. Since prefix recognisable graphs are rational [29] this serves as another proof of the undecidability of bisimilarity for rational Kripke frames. In [50] the authors reduced a version of the Post?s correspondence problem to the bisimilarity problem for prefix rewrite systems. This result now carries over to global bisimilarity: Corollary 3.7.6 ([6]) It is undecidable whether two given rational Kripke frames are globally bisimilar. Proof. The basic idea is that the bisimilarity of the pointed Kripke frames produced from the configurations graphs of the Petri nets in Janc?ar?s proof can be reduced to the global bisimilarity of two Kripke frames. This can be done by adding a unique appendix to each of the distinguished points of the two pointed Kripke frames, such that every global bisimulation between the resulting frames has to map these appendices to each other. A bisimulation on the respective pointed frames is then produced, and vice versa - every such bisimulation extends to a global bisimulation between the Kripke frames with the appendices. Constuction 3.7.7 Let N be the net constructed to simulate C. Construct the net N1 by adding the place s0, the transition t0 and the arcs (s0, t0) , (t0, s1) and (t0, p) to N . N2 is constructed by adding s0, t0 and the arcs (s0, t0) , (t0, s1) and (t0, p?) to N . In both nets let L (t0) = a0. Figure 3.20: The newly constructed nets N1 and N2. N N p p? s0 s0s1 s1 t0 t0 60 CHAPTER 3. RATIONAL KRIPKE STRUCTURES Let M be the set of all finite words over the alphabet {c1, c2, s0, s1, . . . , sn, p, p?}. Furthermore, for both N1 and N2 let Rt be the rational relation corresponding to the transition t 6= t0. Since the behaviour of the transitions not equal to t0 are the same in both nets, the corresponding rational relations coincide. The different Rt?s are defined as follows where 1 ? c, d < n 1. For tc where the command Sc is of the first type and for instance using the counter c1 Rti = { cx11 c x2 2 s 0 0s 0 1 . . . s 1 c . . . s 0 np rp?s tc? cx1+11 c x2 2 s 0 0s 0 1 . . . s 0 c . . . s 1 k . . . s 0 np rp?s } with r + s = 1. 2. For Sd a command of type two and for instance using counter c2 let r + s = 1 again. (a) The transition tNZd induces the relation RtNZd = { cx11 c x2 2 s 0 0s 0 1 . . . s 1 d . . . s 0 np rp?s tNZd ? cx11 c x2?1 2 s 0 0s 0 1 . . . s 0 d . . . s 1 k2 . . . s 0 np rp?s } (b) tZd induces RtZd = { cx11 c x2 2 s 0 0s 0 1 . . . s 1 d . . . s 0 np rp?s tZd ? cx11 c x2 2 s 0 0s 0 1 . . . s 0 d . . . s 1 k1 . . . s 0 np rp?s } (c) For x2 > 0 the relation induced by t?d is Rt?d = { cx11 c x2 2 s 0 0s 0 1 . . . s 1 d . . . s 0 np 1p?0 t?d ? cx11 c x2 2 s 0 0s 0 1 . . . s 0 d . . . s 1 k1 . . . s 0 np 0p?1 } (d) The relation induced by t??d where x2 > 0 is Rt??d = { cx11 c x2 2 s 0 0s 0 1 . . . s 1 d . . . s 0 np 0p?1 t??d ? cx11 c x2 2 s 0 0s 0 1 . . . s 0 d . . . s 1 k1 . . . s 0 np 1p?0 } 3. Lastly the relation induced by the transition tF is given by RtF = { cx11 c x2 2 s 0 0s 0 1 . . . s 0 n?1s 1 np 1p?0 tF? cx11 c x2 2 s 0 0s 0 1 . . . s 0 np 0p?0 } The valid markings are considered to be those for which at most one of the si?s, for 1 ? i ? n, contains one token and the sum of the tokens in p and p? is 1. This is because the aim for the net N is to simulate the behaviour of the counter machine which can 3.7. BISIMULATION 61 only obey one command at a time. Furthermore, only after the final transition has been fired, do none of the places s1, . . . , sn, p, p? contain any tokens. Now let x, y be specific input values for the machine C and set R1t0 = { cx1c y 2s 1 0s 0 1 . . . s 0 np 0p?0 t0? cx1c y 2s 0 0s 1 1 . . . s 0 np 1p?0 } and R2t0 = { cx1c y 2s 1 0s 0 1 . . . s 0 np 0p?0 t0? cx1c y 2s 0 0s 1 1 . . . s 0 np 0p?1 } R1t0 and R2t0 are rational relations (they are singletons) and thus so are the relations R1 = R1t0 ? ? t 6=t0 Rt and R2 = R 2 t0 ? ? t 6=t0 Rt of the nest N1 and N2 respectively. Consequently the configuration graphs of the nets N1 and N2, say C1 and C2, are rational Kripke frames. Firstly, consider the word u = cx1c y 2s 1 0s 0 1 . . . s 0 np0p?0 in C1. Clearly, there is no bisim- ulation relating any word v 6= u in C2 to u since u has an a0 successor and v not (the forth condition is broken). Hence the only word in C2 a bisimulation can possibly relate to u is the word u. A bisimulation relates u in C1 to u in C2 if and only if the successor v1 = c x 1c y 2s 0 0s 1 1 . . . s 0 np1p?0 of u in C1 (i.e. its only successor in C1) is related to the successor v2 = cx1c y 2s 0 0s 1 1 . . . s 0 np0p?1 of u in C2 (again the only one there is). In these successors the value representing the number of tokens in s0 is zero and there are no transitions in either N1 or N2 that increase the number of tokens in s0. Hence, whether or not v1 and v2 are related by a bisimulation only depends on the transitions in N1 and N2 that coincide - which also coincides with N ?s transitions. Consequently there is a bisimulation relating v1 and v2 if and only if the words cx1c y 2s 1 1 . . . s 0 np1p?0 and cx1c y 2s 1 1 . . . s 0 np0p?1 in C are related by a bisimulation, i.e. if and only if the pointed Kripke models are bisimilar. The latter problem is however undecidable. Next, any word in C1 that does not represent a valid marking will be related to its counterpart in C2 by any bisimulation. In neither of these graph do they have any successors so the back and forth conditions are vacuously satisfied. Now consider a word w 6= u which represents a valid marking. Firstly w has no a0 successor. Secondly, u is not in the image of any of the relations Rt 6=t0 and thus u is not reachable from w. Hence any path leading from the word w in C1 will also be a path in C2 and vice versa. Thus, there will be a bisimulation relating w in C1 and w in C2. In conclusion, whether there exists a global bisimulation between C1 and C2 only depends on whether (C1, v1) and (C2, v2) are bisimilar. Therefore global bisimilarity between C1 and C2 is undecidable. qed Corollary 3.7.8 ([6]) It is undecidable whether two given pointed rational Kripke models are bisimilar, or whether two given rational Kripke models are globally bisimilar. 62 CHAPTER 3. RATIONAL KRIPKE STRUCTURES 3.7.2 The finite bisimilarity problem There are two questions to be answered with respect to deciding whether or not a rational Kripke models is finite up to bisimulation - in [39] Janc?ar called them the equivalence and finiteness problems respectively. Question 3.7.9 The finite equivalence problem: Given an arbitrary pointed ra- tional Kripke modelM and a finite pointed rational Kripke model N , are they bisimilar. Question 3.7.10 The finite bisimilarity problem: Given a pointed rational Kripke model M, is M finite up to bisimulation? In other words, does there exist a finite pointed rational Kripke model N bisimilar toM? A pointed rational Kripke model will be called generated if every state in the model is reachable form the the distinguished one. The first question will be answered here for the case where the pointed model is generated. Suppose the generated rational Kripke modelM has a finite bisimulation quotient. Is there a way to ?effectively produce? classes ofM?s domain? By ?effectively produce? I mean to say that the classes must be symbolically presentable. The answer is ?yes?. The Paige-Tarjan Algorithm is suitable for this. A rational partition of a regular language L is one in which every subset in the partition is a regular sublanguage of L. IfM = (M,R, V ) is a rational Kripke model, the function W : P (?)? P (M) is defined such that for every P ? P (?) W (P ) = {x ?M | ?p ? P (x ? V (p)) ? ?p /? P (x /? V (p))} Lemma 3.7.11 ([6]) LetM = (M,R, V ) be a rational Kripke model and ? the set of propositional variables in the language. Then {W (P ) |P ? P (?)} is a rational partition of the state space M ofM, called the partition of M induced by ?. Proof. For every P ? P (?) we have that W (P ) = (?p?P V (p) )\(?p/?P V (p) ). Thus W (P ) is a boolean combination of regular sets and therefore regular itself. qed Proposition 3.7.12 ([6]) It is (semi-)decidable whether or not a given pointed gener- ated rational Kripke model (Mr, u) and given finite pointed Kripke model (Mf , v) are bisimilar. Proof. To prove this claim a semi-algorithm which halts ifMr is finite up to bisimula- tion is given. Minor alterations are made to the Paige-Tarjan algorithm. The resulting semi-algorithm can then be applied effectively to rational Kripke models. Algorithm: Let Mr = (??, R, V ) be the rational Kripke model under consideration, with (Mr, s) the pointed rational Kripke model. 3.7. BISIMULATION 63 1. Start off with the rational partitioning of the domain induced by ?, with the only change being that the vertex u is placed in its own block: Let P ? ? P (?) be the set of exactly all those propositional variables satisfied at u. P0 = {V ?? (P ) |P ? P (?) , P 6= P ?} ? {S, V ?? (P ?) \S} where S = {u}. Furthermore, let Psplit ? P0 and initialise it to Psplit = {S}. Let k0 = |Psplit|. 2. To obtain the partition Pi choose an arbitrary set Ai ? Psplit and perform the splitting procedure of the sets in Pi?1: Pi = { B ?R ?1 (Ai) , B\R?1 (Ai) |B ? Pi?1} and update Psplit?s content such that: Psplit = Psplit ? { B ?R?1 (Ai) |B ? Pi?1} and then Psplit = Psplit\ {?}. Lastly set ki = |Psplit|. The alteration made to the Paige-Tarjan algorithm is that only sets that contain words reachable form the word u, or u itself are used to perform the splitting - since we are only interested in sets that can be reached from u. Now, if there is a finite t such that for any of the kt sets in Psplit the splitting procedure does not produce a new partition, then a fixpoint is reached. Each partition Pi is a set of regular sets: P0 contains only regular sets. A combi- nation of boolean operators are applied to the sets in Pi?1 and the claim then follows since regular sets are closed under the boolean operations. These closure properties are then also the reason why each partition that follows is a set of regular sets. Let Pt now be the final partition reached and label its elements from D1 toDl. Define a finite rational Kripke model as follows: MF = (W1, R1, V1) with W1 = {1, 2, . . . , l} and iR1j holds for 1 ? i, j ? l if and only if Di ? R?1 (Dj) 6= ?. Then the relation B : ?? ? W1 defined by sBi for s ? ?? and 0 ? i ? l if and only if s ? Di, is a bisimulation from ?? to W1. Hence, (Mr, u) and (MF , w) are bisimilar, where u ? Dw. Since two pointed Kripke structures are bisimilar if and only if their bisimulation quotients are isomorphic [47], the pointed model (Mr, u) will be bisimilar to (Mf , v), if and only if (MF , w) is bisimilar to (Mf , v). Since these two pointed models are both finite, bisimilarity between them is decidable. Thus, if the answer is positive, this procedure will produce it. qed Definition 3.7.13 The pointed frames (models) (S1, u1) and (S2, u2) are n-bisimilar (or, n-bisimulation equivalent) if there is an n-bisimulation B between S1 and S2 such that B relates u1 and u2. 64 CHAPTER 3. RATIONAL KRIPKE STRUCTURES Intuitively, an n-bisimulation is a relation between two frames (models) that pre- serves atomic information and transition possibilities up n steps. The concept of n-bisimulation can be rephrased in terms of a bisimulation game, so that two pointed Kripke frames (models) are n-bisimilar if and only if Player II has a winning strategy in the n-round bisimulation game. For more details see e.g. [47]. Lemma 3.7.14 ([6]) It is decidable whether or not two given pointed rational Kripke models are n-bisimilar. Proof. Two methods to determine whether two given pointed Kripke models (M1, u1) and (M2, u2) are n-bisimilar are given. First method : Firstly determine the partitions P1 and P2 of M1 and M2 induced by ?. Note that there must be a one-to-one correspondence between the elements in P1 and P2. Enumerate the elements in P (?) and let B0i = {ui} for i = 1, 2. We will construct sequences of regular languages Bji for j = 1, 2, . . . , n (if possible) as follows: 1. Initialize Bj1 = B j 2 = ?. 2. Enumerate the sets in Bj?11 and B j?1 2 , e.g., B j?1 1 = {A1, A2, . . . , Am} and Bj?12 ={C1, C2, . . . , Cm}. The lists Bj?11 and Bj?12 must be of equal length and contain matching elements in matching positions. Now, for k = 1, 2, . . . ,m: (a) Compute the regular language R (Ak) and then the regular languages R (Ak)? W (Pl) for every Pl ? P (?). (b) Compute the regular language R (Ck) and then the regular languages R (Ck)? W (Pl) for every Pl ? P (?). (c) If R (Ak) ? W (Pl) = ? ?? R (Ck) ? W (Pl) = ?, iterate through the elements in P (?), adding the language R (Ak)?W (Pl) at the end of Bji for each iteration. Otherwise Bji cannot be obtained. Halt the procedure and return ?no?, i.e(M1, u1) and (M2, u2) are not n-bisimilar. If Bn1 and Bn2 are constructed successfully, return ?yes? i.e. (M1, u1) and (M2, u2) are n-bisimilar. Second method Alternatively, characteristic formulas (see [47]) can be used to determine whether two models are n-bisimilar. Considering (M1, u1) as the reference structure, we can characterize n-bisimilarity to (M1, u1) with a modal formula ?n[M1,u1], such that (M1, u1) and (M2, u2) are n-bisimilar if and only if M2, u2 |= ?n[M1,u1]. We define ?n[M1,u1] in- ductively as follows: 3.7. BISIMULATION 65 1. ?0[M1,u1] is the conjunction of all p ? ? that are true at u1 and all ?p that are false at u1 inM1. 2. ?n+1[M1,u1] := ? 0[M1,u1] ? ? u1Ru2 ?R??n[M1,u1] ? [R] ? u1Ru2 ? n[M1,u2]. Now, do local model checking of ?n[M1,u1] inM2 at u2. IfM2, u2 |= ?n[M1,u1] return ?yes?, else return ?no?. The second approach has the advantage that, once ?n+1[M1,u1] is determined, it can be used to determine whether any other given model is n-bisimilar to (M1, u1). qed Proposition 3.7.15 ([6]) It is (semi-)decidable whether or not a pointed rational Kripke model (M, u) and a pointed finite Kripke model (N , v) are not bisimilar. Proof. A semi-algorithm subsequently testing n-bisimulations of (Mr, u) and (Mf , v) for n = 1, 2, . . ., using either of the methods in lemma 3.7.14 is run. If the two models are not bisimilar, then they are not n-bisimilar for a large enough n, so this algorithm will terminate after finitely many steps. qed The two semi-decidability results now have the following interesting consequences: Corollary 3.7.16 ([6]) It is decidable whether or not a given pointed generated ratio- nal Kripke model (Mr, u) and given finite pointed Kripke model (Mf , v) are bisimilar. 66 CHAPTER 3. RATIONAL KRIPKE STRUCTURES Chapter 4 Subclasses of Rational Kripke Structures In this chapter three subclasses of rational Kripke structures are investigated. Morvan [71] gives two ways to isolate subclasses of rational graphs. The first way is a structural restriction on the graph itself, while the second involves a limitation on the transducer. This chapter deals with one subclass of the first type and two subclasses of the second. 4.1 Automatic Kripke structures Definition 4.1.1 ([66]) A transducer T = ?Q,?,?, qi, F, ?? is called letter-to-letter or synchronous if every (p, u, v, q) ? ? satisfies u, v ? ?. A relation recognised by a synchronous transducer is length-preserving since it only relates words u, v ? ?? if |u| = |v|. This is not a very general class of relations and in order to obtain a broader class, the synchronisation of the transducer can be relaxed ([37]). Definition 4.1.2 ([79]) Let ? /? ?, then ?? = ? ? {?}. The convolution of a pair (u, v) is the pair (u?i, v?j) from ?? ? ?? where i = max (0, |v| ? |u|) and j = max (0, |u| ? |v|). Then the convolution of a binary relation R over ?, de- noted by ?R, is the relation containing all the convolutions of the pairs in R, i.e. ?R = {(u?i, v?j) | (u, v) ? R} Definition 4.1.3 ([79]) A binary relation R ? ?? ? ?? over a finite alphabet ? is regular (automatic or finite automaton recognisable) if its convolution ?R is recognisable by a synchronous transducer. Definition 4.1.4 ([79]) An automatic Kripke frame is a rational Kripke frame F = (S,R) over a finite alphabet ? such that S ? ?? is a regular language and R ? 67 68 CHAPTER 4. SUBCLASSES OF RATIONAL KRIPKE STRUCTURES ?? ? ?? is regular. Example 4.1.5 The transducer T in figure 4.1 is a synchronous transducer over ?? = {0, 1,?}. Consider the Kripke frame F = (S,R) where S = (0 + 1)? 0 and R = R1 ?R2 ?R3 with: R1 = (0, 1) (, u) (, 0)+ R2 = (1, 1) (u, v) (0, w) (, 0)+ R3 = (1, 1) (u, u) (0, 1) (v, w) (0, 0)+ for u, v, w ? ??. Then T recognises ?R and the Kripke frame F , given in figure 4.2, is automatic. F is the frame where each even number n ? N is encoded in the standard way as a binary string without leading zeros and each encoded even number is related to all the encodings of even numbers strictly greater than itself. The automatic Kripke frame F does not have a bounded degree. Figure 4.1: The synchronous transducer T recognising ?R. q1q2q3q4 q5 q6 q7 1/1 1/1 0/1 0/10/0 0/0 0/1 ?/0 0/0 1/1 0/0; 0/1; 1/1; 1/0 0/0 0/0; 0/1; 1/1; 1/0 ?/0 ?/1 ?/0 Figure 4.2: An automatic Kripke frame. 0 10 100 110 1000 . . . ? 4.1. AUTOMATIC KRIPKE STRUCTURES 69 The class of automatic graphs have been studied extensively under different names. Automatic relations were already studied by Bu?chi in 1960 under the name sequential relations and in 1965 by Elgot and Mezei [37] where they were called synchronized rational relations. Hodgson studies the satisfiability problem for first-order logic over automatic graphs in [48] and in [26]. Cannon et al. study automatic structures in order to do computations on some finitely generated groups. In [44] Frougny and Sakarovitch do a comprehensive study of the subclass of rational relations they called synchronized rational relations. This is exactly the class of regular relations. Automatic structures are reintroduced by Khoussainov and Nerode in [54] where they also define automat- ically presentable structures. The notion of a graph being rationally presentable is analogous to this. Automatic structures have since been studied by various authors; see for instance Blumensath?s Diploma thesis [15] where he has studied various subclasses of automatic structures. In [16, 17] automatic and ?-automatic structures have been studied and in particular the complexity of model checking and query evaluation on automatic structures for fragments of first-order logic. In his PhD. thesis, [79], Rubin studies the expressiveness and limitations of the transducers recognising automatic structures and in and [55] by Khoussainov et al. some classes of automatic structures are characterised and the isomorphism problem for automatic graphs is studied. Then automatic linear orders and also automatic trees are studied in [56] by Khoussainov et al. 4.1.1 Examples and non-examples of automatic frames Many of the classes of infinite structures which have been studied for verification pur- poses are included in the class of automatic Kripke frames. Petri nets Let ??k denote the words in ?? of length less than or equal to some k ? N and let LDk = ( ??k ? {}) ?({} ? ??k). The following result can be used to determine whether a graph or a class of graphs is automatic. Proposition 4.1.6 ([44]) Every rational relation with bounded length difference is a regular relation. Proof (Sketch).[44] This follows from the fact that a rational relation with the differ- ence between the lengths of the words it relates bounded by some k, is a finite union of products of subsets of LDk and rational subsets of (A?B)?. qed Example 4.1.7 In [69] Morvan states that the configuration graphs of Petri nets are rational. Moreover, Carayol and Rubin observed separately that an automatic presen- tation of the configuration graph of a Petri net is obtained when a unary encoding of 70 CHAPTER 4. SUBCLASSES OF RATIONAL KRIPKE STRUCTURES the markings of the Petri net is used. Let 0k110k21 ? ? ? 10kn ? ?? represent a mark- ing M = (k1, . . . , kn) of a Petri net N = (P, T, F,M0) where P = {p1, p2, . . . , pn}, T = {t1, t2, . . . , tm} and ? = {0, 1}. Furthermore, let Rti be the relation induced by firing the transition ti. The value of dij = F (ti, pj) ? F (pj, ti) for every pair i, j ? {1, 2, . . . , n} is constant (Proposition 3.1.19). Hence the difference in length be- tween two words (i.e. states) related to each other by Rti is at most ?n j=1 |dj| for each i ? {1, 2, . . . , n}. From proposition 4.1.6 this relation is regular. This is true for every relation Rt with t ? T and therefore the configuration graph of N is automatic. For a specific example, let N = (P, T, F,M0) be the Petri net with P {p1, p2}, T = {t} and M0 = (4, 5). Furthermore, the flow function is defined by F (p1, t) = 2; F (t, p2) = 3 and F (p2, t) = F (t, p1) = 0. Then dt1 = 0 ? 2 and dt2 = 3 ? 0 and the difference in length between two words representing the markings and related by the relation induced by the transition t is bounded | ? 2| + |3| = 5. Since t is the only transition this is also the bound for the length difference between any two related words. In particular the word 0000100000 representing the initial marking M0 is only related to the word 00100000000. In fact, for N related words will have a length difference of exactly 1. ? A consequence of the inclusion of the configuration graphs of Petri nets in the class of automatic graphs, is that Janc?ar?s result in [49] on the undecidability of bisimilarity for labeled Petri nets also carries over to the class of automatic Kripke frames. Corollary 4.1.8 It is undecidable whether two given pointed automatic Kripke models are bisimilar or not. Moreover, it is also undecidable whether two given automatic Kripke frames are globally bisimilar. Khoussainov et al. ([54]) prove that prefix-recognisable frames are included in the class of automatic frames. Therefore the undecidability of bisimilarity for automatic frames also follows from the undecidability of bisimilarity for prefix-recognisable frames [50]. Congruential graphs Blumensath and Gra?del give an alternative characterisation of automatic frames in [17]. This characterisation makes use of an important tool in mathematical logic, namely interpretation. A copy of a structure is defined within another structure, thus allowing the transfer of certain results among the theories. One can now use this characterisation to prove or disprove that some class of structures belongs to the class of automatic Kripke frames. Let L be the set of first-order formulas of the natural numbers where + and = are the only non-logical symbols used. 4.1. AUTOMATIC KRIPKE STRUCTURES 71 Definition 4.1.9 ([76]) Presburger arithmetic is the first-order theory of the struc- ture ?N,+,=?, i.e. the set of all sentences in L which are true in ?N,+,=?. In 1929 Presburger [76] showed that Presburger Arithmetic is decidable, consistent and complete. Fisher and Rabin [43] later proved that the decision algorithm provided by Presburger has a worst case runtime of at least 22cn for some constant c > 0 and where n is the length of the formula. This is one of the few examples of algorithms that provably requires more than polynomial runtime. For convenience a number of non-logical symbols are added to the language. In fact, they serve as abbreviations for formulas in L. These non-logical symbols are the constant symbols 0 and 1, the binary relation symbol < and the unary function symbol s. The formula ?y (0+ y = y) now defines 0. The ordering < is defined by ?x?y (?z (?z = 0 ? x+ z = y)? x < y) . Then 1 is defined by ((0 < 1) ? ??x (0 < x ? x < 1)) and s is defined by ?x?y (s (x) = y ? x < y ? ??z (x < z ? z < y)) . Definition 4.1.10 ([17, 15]) A subset X ? Nn is Presburger definable if there is a Presburger formula (first-order formula in the language of the Presburger arithmetic) ? (x?) with free variables x? = (x1, . . . , xn) such that X = {s ? Nn|s |= ? (x?)}. Further- more, a Kripke frame is first-order definable in ?N,+,=? if its domain and binary relation(s) are Presburger definable. Definition 4.1.11 ([17, 15]) A Kripke frame is first-order interpretable in ?N,+,=? if it is isomorphic to a Kripke frame that is first-order definable in ?N,+,=?. Proposition 4.1.12 ([17]) A Kripke frame is automatic if and only if it is first-order interpretable in the expansion ?N,+, |p? of the Presburger arithmetic, where |p : N? N is the relation such that x|py ?? x is a power of p that divides y. Now consider the following class of graphs studied by Urvoy. Definition 4.1.13 ([88]) A congruential system C is a finite set of rules of the form (p, r) a? (q, s) where a ? ? (for ? a finite alphabet of labels), p, q, r, s ? N. The graph of a congruential system C, called a congruential graph, is given by G (C) = (N, RG(C)) where the relation RG(C) is defined by RG(C) = {(pn+ r, a, qn+ s) | (p, r) a? (q, s) , n ? N} 72 CHAPTER 4. SUBCLASSES OF RATIONAL KRIPKE STRUCTURES Congruential functions are presented by Conway in [34] and also by Burckel in [25]. Congruential systems are a non-deterministic generalization of these functions. Example 4.1.14 Let C be the congruential system defined by the rules: for n > 0 2n a? n 2n+ 1 a? 3(2n+ 1) + 1 = 6n+ 4 Then the well-known Collatz?s graph [33] given in figure 4.3, is the graph of C where 0k is short for the word 00 ? ? ? 0 ? ?? ? k times ? ?? with ? = {0}, and it is the unary representation of the number k ? N. Figure 4.3: The Collatz?s graph. 01 02 04 08 016 032 064 021 042 05 010 03 06 . . . . . . . . . . . . ? Proposition 4.1.15 ([88]) Under the unary representation of natural numbers, every congruential graph is a rational Kripke frame. Proof.[[88]] The relation of the graph (in unary representation) of an elementary con- gruential system C with the rule nq+ r a? np+ s is recognised by the finite transducer in figure 4.4. Figure 4.4: A finite transducer that recognises the relation of an elementary congruen- tial graph. q1 q2 0r/0s 0q/0p Any congruential system is the finite union of elementary congruential systems and since rational relations are closed under finite union, any congruential graph is a rational Kripke frame. qed 4.1. AUTOMATIC KRIPKE STRUCTURES 73 This result can now be refined: Proposition 4.1.16 Congruential graphs are automatic Kripke frames. Proof. Consider an elementary congruential system C with the rule nq + r a? np+ s. This rule involves only addition and multiplication with a constant which are both Presburger definable: C (x, y) ?? ?n ??x = n+ n+ ? ? ?+ n ? ?? ? q times +r? ? y = n+ n+ ? ? ?+ n ? ?? ? p times +s? ?? For m ? N let m? be a constant symbol for it in the fist-order language used. Since ?1 is Presburger definable using the ordering, so are r? and s?. For example r? = ?1 + ?1 + ? ? ?+ ?1 ? ?? ? r times . Only finitely many such constants will be needed since there are only finitely many rules in a system. Then by proposition 4.1.12 the graph of this system is automatic. qed Non-automatic rational Kripke frames Example 4.1.17 Let R = {(u, v) |u ? {a, bb}? , v ? {ba?b}?}. Then the transducer in figure 4.5 recognises R and R can also be represented by the regular expression{(a, )? , {(b, b) , (, a)? , (b, b)}?}?. Therefore, the frame F = (S,R) is a rational Kripke frame. Figure 4.5: A transducer recognising R = {(u, v) |u ? {a, bb}? , v ? {ba?b}?}. q1 q2 a/ /a b/b b/b If there exists a letter-to-letter transducer that recognises the convolution of R, then it must recognise a pair of words of the type ( ak (bb)l?r, (bamb)l ) for k, l,m ? N where (bamb)l = bam1bbam2b ? bamtb ? ?? ? l times such that m1 +m2 + ? ? ? +mt ? k = r. To recognise the pair of words k edges with input label a must be read and then 2l edges with b as input label. The difficultly now comes in with counting the number of times a edge with a for the output label is read. This must be done in order to know how many times edges 74 CHAPTER 4. SUBCLASSES OF RATIONAL KRIPKE STRUCTURES labeled by /b must be followed to form the desired pair of words. However, automata do not have the ability to keep track of the number of times a certain type of input has been read. Push-down automata are needed for that. Hence, no such transducer exists and F is not an automatic Kripke frame. ? Example 4.1.18 ([66]) Let R = {(An, u) |n ? 0, u ? B? (AB?)n}. Then R is a ra- tional relation recognised by the transducer in figure 4.6 and the rational expression {(a, a) , (, b)}? represents R. Then a Kripke frame F = (S,R) where S = {A,B}? is rational. However, by using a similar argument to the one used in Example 4.1.17, it follows that there does not exist a letter-to-letter transducer accepting the convolution of R and F is not automatic. Figure 4.6: A transducer recognising R = {(An, u) |n ? 0, u ? B? (AB?)n}. q1/b a/a ? Automatic Kripke frames of finite out-degree can be separated from the rational Kripke frames of finite out-degree by making use of the the growth rate of the out- degree of vertices. Proposition 4.1.19 ([78]) For any automatic frame, F , of finite out-degree and any state s, there exists a c ? N, such that the out-degree of vertices at distance n of x is at most cn. Two non-automatic rational Kripke frames are given. In the first example the growth rate of the out-degree of vertices exceeds the bound for automatic Kripke frames, but it not the growth rate of the out-degree of vertices in rational Kripke frames given in Proposition 3.1.16. Example 4.1.20 Let ? = {?, A,B, 0, 1} and consider the rational Kripke frame F = (S,R) in figure 4.7 where the universe S is given by the regular expression {{A,B} {0, 1}?}? {A, b}? ? {?} and the relation R is recognised by the transducer in figure 4.8. At distance n from the state ??? a vertex has out-degree of 2n2 . Firstly observe that a vertex at distance n+1 from ???, for n ? 1, is a word of length n2 and each position in the word can assume one of two letters. Moreover, the state at distance n is related to exactly 2? 2? ? ? ? ? 2 ? ?? ? n2 words and therefore the out-degree is 2n2 . 4.1. AUTOMATIC KRIPKE STRUCTURES 75 Now, for any c ? N there is an M ? N such that 2M ? c and therefore ( 2M )l ? cl for n ? N. But then for all n > M it holds that n2 > Mn and therefore also that 2n2 > 2Mn ? cn. Thus there does not exist a constant c such that the out-degree of vertices at distance n from any state s is at most cn. This proves that F is not an automatic frame. Figure 4.7: A finite degree rational graph with the vertices at a distance n from any chosen vertex r having out-degree 2n2 . ?  A B A000 A001 ? ? ? A111 B000 B001 ? ? ? B111 A0000000A A0000000B ? ? ? B1111111A B1111111B A00000000000A000 ? ? ? B11111111111B111 ? Example 4.1.21 ([66]) Revisit the rational Kripke frame discussed in Example 3.1.17, given again in figure 4.9. This frame is not automatic since for a state s in this frame, the out-degree of states at distance n from x is 22n+1 - it exceeds the upper bound in Proposition 4.1.19. ? 76 CHAPTER 4. SUBCLASSES OF RATIONAL KRIPKE STRUCTURES Figure 4.8: A transducer recognising the relation R. q1 q2 q3 q4 q5 q6 ?/ / /x x1/x2u y1/y2 y3/y4 /yx, x1, x2 ? {A,B} u ? {0, 1}3 y, y1, y2, y3, y4 ? {0, 1} Figure 4.9: A non-automatic rational Kripke frame with finite out-degree. 0 1 00 01 10 11 0000 . . . 1000 . . . 1111 0000000 . . . 10001000 . . . 11111111 000 . . . 100 . . . 111 000000 . . . 100000 . . . 111111 . . . 4.1.2 Model checking on Automatic structures Verification of properties for infinite state systems can be reduced to the satisfiability problem (see Chapter 3): the task of determining whether or not a formula with free variables is satisfiable in a given structure. A positive result concerning the satisfiability problem for first-order logic on auto- matic Kripke frames has been obtained: Theorem 4.1.22 ([48, 54]) The satisfiability problem for first-order logic over auto- matic Kripke frames is decidable. Moreover, every automatic Kripke frame has a decidable first-order theory. This means that, fixing a frame, there is an algorithm which can determine whether a given first-order sentence is true or not. 4.2. RATIONAL KRIPKE TREES 77 Another problem that has been studied is first-order query evaluation: if an automatic Kripke frame is fixed, then, given as input a first-order formula, ? (x?) with free variables x? = (x1, x2, . . . , xn), determine the tuples of elements a? in the frame that satisfy ?. Formally the relation {a? ? Sn|F |= ? (a?)} is computed. First-order query evaluation for automatic frames is decidable since every such relation is an effective computable regular relation [15]. A direct consequence of these results is that model checking formula from the lan- guages considered so far, is also decidable. The hybrid language Ht (U, ?) can be ex- tended even further such that it has the same expressive power as first-order logic ([11, 13, 14]). Add the quantifier ?, quantifying over the state variable, to obtain the hybrid language Ht (U, ?, ?). Semantically, letM = (S,R, V ) and s ? S, then: M, s |= ?x? ?? there is a nominal i ? ? such thatM, s |= ? [x? i] Formulas in Ht (U, ?, ?) can be translated to first-order formulas - see [11] for the extension of the standard translation [89]. Hence, local model checking of formulas in Ht (U, ?, ?) is decidable. Furthermore, using this extension of the standard translation, every formula ? ? Ht (U, ?, ?) translates into a first-order formula ? containing exactly one free variable. The evaluation of ? then produces a regular set. Global model checking of formulas in Ht (U, ?, ?) is therefore also decidable. Moreover, for ? ? Ht (U, ?, ?) the set [|?|] is regular. Even though automatic Kripke frames enjoy positive result with respect to first- order logic, undecidability is obtained when the first-order logic is extended with reach- ability or transitive closure operators. Theorem 4.1.23 ([15]) The reachability problem over automatic graphs is undecid- able. Therefore, even though automatic Kripke frames have decidable first-order theories, extending first-order logic with reachability gives undecidability. When decidable reach- ability is of interest there is no advantage to studying automatic frames over rational frames since the former does not enjoy more favourable results. 4.2 Rational Kripke trees Definition 4.2.1 ([27]) A rational Kripke tree is a rational Kripke frame that satisfies the following three properties: 1. The frame is connected. 2. Every state in the frame has at most one predecessor. 78 CHAPTER 4. SUBCLASSES OF RATIONAL KRIPKE STRUCTURES 3. There is a unique state in the domain of the frame which is not in the range, i.e. there is a unique state in the frame which has no predecessors. Therefore, a rational Kripke tree model is a rational Kripke model with a ra- tional Kripke tree as the underlying frame. Rational Kripke trees have been studied by Carayol and Morvan in [27]. Proposition 4.2.2 ([27]) It is undecidable whether a rational Kripke frame is a tree. The last two of the three properties listed in the definition can be verified easily. The second property can be checked using Shutzenberger?s theorem which appears in [7]. In order to verify whether a rational graph G = (S,R) has the third property, i.e. verifying the existence of the root, one needs to check that the set D\W is a singleton, where D denotes the domain of R and W its range. However, to prove that it is undecidable whether or not a given rational graph is a rational tree, Morvan an Carayol reduces the problem to a variation of the uniform halting problem for Turing machines. Example 4.2.3 ([27]) An example of a rational Kripke tree that is not automatic is given below. The rational Kripke frame obtained from the finite transducer in figure 4.10 is the graph given in figure 4.11. Figure 4.10: A finite transducer that produces a rational Kripke frame with finite, but unbounded degree. q1 q2 q3 q4/A A/A0 A/A1 /A 0/0 1/1 A/A0 A/A1 This graph is a rational forest presented in [27] - it contains infinitely many con- nected components. As seen earlier in Chapter 3 on page 54, the generated subframe of a rational Kripke frame is not necessarily rational itself and therefore one can?t simply claim that one of the connected components is a rational tree. From [27] it holds that given a regular language L, the graph connecting the words in L into a half line in length-lexicographic order is automatic. Observe that the set of all the roots of the components in figure 4.11 form a regular language, namely LT = A+ {0, 1}? ? {}. In 4.2. RATIONAL KRIPKE TREES 79 Figure 4.11: The forest such that every vertex at a depth n has 2n successors.  A A0A A1A A00A0A A00A1A A10A0A A10A1A A0 A00A A10A A1 A01A A11A . . . figure 4.12, I present a transducer that produces a rational graph with the words in LT as vertices. Figure 4.12: A transducer which produces a graph connecting the roots. q1 q2 q3 A/A /0 A/0 q4 q5 / A/A A11/AA0 1/0 q6 q7 q8q9 q10 A/A1/A A/A / 0/0 1/1 0/1 01/10 1/0 Figure 4.13 is the frame obtained from this transducer. The frames in figures 4.11 and 4.13 are both rational Kripke frames, and therefore the union of these two frames will again be rational. Moreover, it will be connected and therefore a rational Kripke tree. This tree is not automatic due to the limit of the growth rate of automatic graphs of finite degree (Proposition 4.1.19). ? Definition 4.2.4 ([27]) A vertex (state) in a tree that is not the predecessor of any other state is called a leaf. In [71] Morvan gives the following result. 80 CHAPTER 4. SUBCLASSES OF RATIONAL KRIPKE STRUCTURES Figure 4.13: The rational graph relating all the roots of the forest. A A0 A1 AA A00 A01 A10 A11 AA0 AA1 AAA A000 A001 A010 A011 A100 A101 A110 A111 AA00 AA01 AA10 AA11 AAA0 AAA1 AAAA . . . Proposition 4.2.5 ([71]) The set of leaves of a rational graph is a regular set. Proof. This result follows directly form the closure properties of regular languages. Let T = (S,R) be a rational tree. The domain, D, and the range, W of R are both regular. The set W will contain all the states of the tree except for the root. Thus the set W\D will be the set of all leaves. This set will be a regular language since regular languages are closed under complementation. qed 4.2.1 Model checking on rational Kripke trees Proposition 4.2.6 ([71]) Reachability is decidable for any given pair of vertices of any given rational Kripke tree. Proof. The decidability of the reachability follows directly from the structure of a tree: any state v is only finitely many steps away from the root. Hence the set of vertices, say W , from which v is reachable is finite. Determining whether v is reachable from u then reduces to checking whether u ? W . This actually checks backward reachability. qed A language expressing reachability between two states is necessary in order to make proper use of this result. Let Ht (U,3?) be the basic tense language which, in addition to being extended with nominals from the finite set ? and the [U ]-operator, is also extended with the reachability operator 3?. Definition 4.2.7 A formula in a hybrid language Ht is pure if it contains no propo- sitional variables. Hence the only atomic formulas from which pure formulas are built up are the nominals. Example 4.2.8 The pure formulas from Ht (U) are still quite expressive. 3i? 2i 4.3. MONOTONOUS RATIONAL KRIPKE STRUCTURES 81 This formula states that if the denotation of the nominal i ? ? is a successor of the current state, then it is the only successor of the current state. Pure formulas from the language Ht (U,3?) can now express the reachability be- tween two states in a model. 3?i(4.1) [U ] (j ? 23?i)(4.2) The first formula here says the state which is the denotation of the nominal i is reachable form the current state, while the second formula expresses: ?The denotation of i is reachable from every successor of the denotation of j.? ? Corollary 4.2.9 Local model checking of pure formulas from the language Ht (U,3?) is decidable for rational Kripke trees models, i.e. given a rational Kripke tree model M = (S,R, V ), a state s ? S and a formula ? ? Ht (U,3?) then it is decidable whether M, s |= ? or not. This is a direct result of the decidability of reachability between two states. In their study on rational graphs, Carayol and Morvan investigate the first-order theories of rational trees. Proposition 4.2.10 ([27]) Every rational Kripke tree has a decidable first-order theory. In addition Carayol and Morvan show that first-order logic with rational accessibility is undecidable for rational trees and that there exists a rational directed acyclic graph with an undecidable first-order theory. 4.3 Monotonous rational Kripke structures The subclass of monotonous rational Kripke structures is defined by the transducers recognising their relations. Definition 4.3.1 ([71]) Let M = (S,R) be a rational Kripke frame such that the relation R is recognised by the transducer T = ?Q,?,?, qi, F, ??. If every transition (p, u, v, q) ? ? satisfies |u| ? |v| or every transition (p, u, v, q) ? ? satisfies |u| ? |v|, then the rational Kripke frame is monotonous. Example 4.3.2 Consider the transducer T presented in figure 4.14. This is a simple example where the rational Kripke frame (see figure 4.15) generated by the transducer T is a monotonous rational Kripke frame. ? 82 CHAPTER 4. SUBCLASSES OF RATIONAL KRIPKE STRUCTURES Figure 4.14: A transducer T producing a monotonous rational Kripke frame. q1 q2 q3 1/1 1/1 0/1 1/0 /0 0/1 1/0 0/1 Figure 4.15: A monotonous rational Kripke frame. 11 101 1001 10001 111 1011 1101 110 1010 011 0101 01001 010001 . . . . . . . . . . . . Another example of a monotonous frame is the frame presented in figure 3.7 in chapter 3 - which then also serves as an example of a non-automatic monotonous frame. 4.3.1 Model checking on monotonous rational Kripke struc- tures. Monotonous rational Kripke frames have the following positive result with respect to reachability. Proposition 4.3.3 ([71]) Given a monotonous rational Kripke structure, reachabil- ity between any two given states is decidable. Proof. Fix the monotonous rational Kripke modelM = (S,R, V ) and then receive the states u and v as input. Now ask the question: ?Is the state v reachable from the state 4.3. MONOTONOUS RATIONAL KRIPKE STRUCTURES 83 u?? Suppose the model is upward monotonous, i.e. each transition (p, u?, v?, q) in the transducer recognising R satisfies |u?| ? |v?|, then the subset L = {w : |u| ? |w| ? |v|} of S is finite. This means there are only finitely many words w such that |w| = |u| and therefore only finitely many states of the same length, |u|, reachable from the state u before a state with length greater than |u| must be accessed. In the same way there are then only finitely many states of length |u| + 1 reachable from u before a state of even greater length must be accessed, etc. Thus there are finitely many possible paths from u to v. Hence the problem reduces to whether or not at least one of these finite paths belongs to the frame, which is equivalent to checking membership to a regular set a finite number of times for each path. qed This result now makes it possible do model checking of some hybrid logic formulas on monotonous rational Kripke frames. Corollary 4.3.4 If ? is a pure formula in the hybrid language Ht (U,3?), then local model checking of ? on a monotonous rational Kripke frame is decidable. In [71] Morvan conjectures that the first-order theory of monotonous rational graphs is decidable. If this is indeed the case, then model checking of formulas from the more expressive hybrid languages on monotonous rational Kripke frames will also be decidable. 84 CHAPTER 4. SUBCLASSES OF RATIONAL KRIPKE STRUCTURES Chapter 5 An extension of rational Kripke structures Only finite words over a finite alphabet have been considered up to now. One can also consider languages consisting of infinite strings (words). Automata on infinite words were introduced by Bu?chi in [23, 24]. Since then automata on infinite words and the languages they recognise have been studied by various authors, see for instance [64, 4, 62, 18, 45]. 5.1 ?-rational languages Recall that ? is the first infinite ordinal and let ? be a finite alphabet. Then a word of infinite length, or ?-word, ? over ? is a sequence of letters in ?, ? = ? (0)? (1) . . . ? (n) . . .. The set of all infinite words over ? will be denoted by ??. ?-languages are the subsets of ??. Recall the definition of the product of two subsets X,Y ? ??: XY = {uv|u ? X, v ? Y } This product can now be extended to include sets containing infinite words, by setting X ? ?? and Y ? ??. Notice that the length of such a concatenated sequence must be the first ordinal ?. Furthermore, for X ? ??, let X? denote the set of infinite words obtained by concatenating an infinite sequence of nonempty words of X. Rational subsets of ?? can now be defined. Definition 5.1.1 ([45]) The class of ?-rational subsets of ??, is the smallest set RAT? (??) of subsets of ?? such that: 1. if X ? RAT? (??), then X? ? RAT? (??). 2. if X ? ?? and Y ? ??, then their product XY belongs to RAT? (??). 85 86 CHAPTER 5. AN EXTENSION OF RATIONAL KRIPKE STRUCTURES 3. RAT? (??) is closed under finite union. It then follows that the ?-rational subsets of ?? are precisely those subsets which are finite unions of sets of the form XY ?, where X,Y are rational subsets of ??. Definition 5.1.2 ([24]) A Bu?chi automaton A = ?Q,?, qi, F, ?? is a finite au- tomaton, as defined in definition 2.3.2, but with the following acceptance condition: An infinite word ? ? ?? is recognised by A if there is an infinite path (qi, ?1, q1) (q1, ?2, q2) . . . (qn, ?n, qn+1) . . . such that ? = ?1?2 ? ? ??n ? ? ? , a finite state qf ? F and infinitely many i ? N such that qi = qf . Thus, an infinite word is recognised if a final (accepting) state is visited infinitely many times. Note that Bu?chi automata need not be deterministic. In fact, the class of ?-languages recognised by deterministic Bu?chi automata is strictly included in the class of ?-languages recognised by non-deterministic Bu?chi automata [64] (see also [75] for details). The language of infinite words recognised by a Bu?chi automaton A will be denoted by L? (A). In [72] Muller suggests a different acceptance condition for deterministic automaton on infinite words. For a path p, define Inf (p) to be the set of states visited infinitely many times by p. Definition 5.1.3 ([72]) A finite automaton, A = ?Q,?, qi, F, ?? with F ? P (Q), is a Muller automaton if it has the acceptance condition: An infinite word ? ? ?? is recognised by A if there is a path p := (qi, ?1, q1) (q1, ?2, q2) . . . (qn, ?n, qn+1) . . . such that ? = ?1?2 ? ? ??n ? ? ? and Inf (p) ? F . Note that this is a more constrained acceptance condition than Bu?chi?s: Bu?chi requires that Inf (p) ? F 6= ? while Muller requires Inf (p) ? F . Instead of referring to a Bu?chi or Muller automaton, one can simple say an automa- ton with Bu?chi or Muller acceptance condition. ?-rational languages can now be characterised in terms of finite machines (an ana- logue of Kleene?s theorem for infinite words). Theorem 5.1.4 ([64]) A subset X of ?? is ?-rational, if an only if 1. X = L? (A1) where A1 is a non-deterministic Bu?chi automaton, and 2. X = L? (A2) where A2 is a deterministic Muller automaton. The reader is also referred to [75] for a proof of this theorem. 5.1. ?-RATIONAL LANGUAGES 87 Example 5.1.5 Let ? = {0, 1}, then the set of infinite words X? with at most finitely many occurrences of a ?0? directly followed by an occurrence of a ?1?, is an ?-rational subset of ??: X (1?0?01)? (0? + 1?) Figure 5.1 gives a Bu?chi automaton A = ?QA,?, q1, {q3, q4} , ?A? as well as a cor- responding Muller automaton B = ?QB,?, q1, {{p2} , {p3}} , ?B? both recognising the language X?. Note that the Muller acceptance condition is necessary for the determin- istic automaton B and Inf (p) ? F 6= ? is not enough. If B had only Bu?chi acceptance conditions then (101)? ? L? (A), but (101)? /? X?. Figure 5.1: A non-deterministic Bu?chi automaton and a Muller automaton both recog- nising ? = (1?0?01)? (0? + 1?). A q1 q2 q3 q4 0 1 1 0 0 1 0 1 B p1 p2 p3 1 0 0 1 0 1 ? Theorem 5.1.6 The class RAT? (??) of ?-rational subsets is an effective Boolean al- gebra. A proof of this theorem can also be found in [75]. It is still possible to reason about finitary languages in this framework. Lemma 5.1.7 Let X ? REG (??) and suppose ? /? ?. The regular language X can be embedded in a ?-rational subset X? of (? ? {?})?. Proof. For every u ? X, let u? = u?? be the associated ?-word over ?? = ? ? {?}. Let X? be the ?-language of all these words. Then there is an embedding f : X ? X?. Moreover, since X ? REG (??) there is a finite automaton A = ?Q,?, q0, F, ?? recognising X. Let A? = ?Q ? {qf} ,??, q0,{qf}??? be the Bu?chi automaton such that qf /? Q and the transition relation ?? is obtained in the following way: 1. ? ? ?? 2. for every q ? F let ( q,?, qf ) ? ?? 88 CHAPTER 5. AN EXTENSION OF RATIONAL KRIPKE STRUCTURES 3. ( qf ,?, qf ) ? ??. It now needs to be proven that L? (A) = X?: Let ? ? L? (A). Then there is an infinite path (q0, ?1, q1) (q1, ?2, q2) . . . (qn, ?n, qn+1) . . . such that qf occures infinitely often. Futhermore, there is an i ? N such that ( qi,?, qf ) and qj = qf for all j > i. The path therefore has the form:( q0, ?1, q1 ) (q1, ?2, q2) . . .(qi,?, qf)(qf ,?, qf) . . . From the construction of A? the state qi is a final state in A. Thus, there is a word u ? L (A) such that ? = u?? and therefore L? (A) ? X?. Now suppose ? ? X?, then ? = u?? for some u = u1u2 ? ? ? uk ? X. This means that there is a finite path (q0, u1, q1) (q1, u2, q2) . . . (qk, uk, qk+1) in A with qk+1 ? F . By construction the transition ( qk+1?, qf ) ? ??. Moreover, the infinite path (q0, u1, q1) (q1, u2, q2) . . . (qk, uk, qk+1)(qk+1?, qf)(qf ,?, qf) . . . is in A?. Hence, ? ? L? (A) and X? ? L? (A). qed Example 5.1.8 This example illustrates the embedding of a regular language in an ?-rational language. Let X ? REG (??) be the set of all finite words over ? = {0, 1} in which every occurrence of a ?0? is directly followed by an occurrence of a ?1?. Then X = (1 + 01)? and X is recognised by the finite automaton A in figure 5.2. Now let ?? = {0, 1,?}, then X is embedded into the ?-rational language X? = (1 + 01)??? which is recognised by the Bu?chi automaton A? in figure 5.2. Figure 5.2: The finite automaton A and the Bu?chi automaton A?. A : A q1 q2 0 1 1 B : A? p1 p2 p3 0 1 1 ? ? ? ?-rational languages can therefore be seen as a generalisation of finitary regular languages. 5.2. ?-RATIONAL RELATIONS 89 5.2 ?-rational relations Rational relations on infinite words, called ?-rational relations can now be defined. They have been studied by various authors: Barzdin and Trakhtenbrot [4], Lindner and Staigner [62], Nivat and Gire [45] and later also by Frougny and Sakarovitch [44]. Definition 5.2.1 ([42]) An ?-rational relation over a finite alphabet ?, is a subset of ?? ? ?? which are the finite union of relations of the form R1R?2 where R1 and R2 are rational relations over ?? ? ?? . Analogous to the case of ?-languages, the finite machines recognising rational re- lations on finite words can be modified to obtain machines recognising relations on infinite words. Definition 5.2.2 ([24, 5]) A finite transducer T = ?Q,?,?, q0, F, ?? is a Bu?chi transducer if it has the following acceptance condition: A pair (?, ?) ? ?? ? ?? is recognised by T , if for ? = ?1?2 . . . ?n . . . and ? = ?1?2 . . . ?n . . . there is an infinite path (qi, ?1, ?1, p1) (p1, ?2, ?2, p2) . . . (qn, ?n+1, ?n+1, pn+1) . . . and a final state qf ? F such that qf = pn for infinitely many non-negative integers n. Since ? and ? are ?-words, only finitely many of the ?i?s and ?i?s may be the empty word, i.e. there exist k, l ? N such that ?j 6=  for every j > k and ?j 6=  for every j > l. Definition 5.2.3 ([44]) A transducer T = ?Q,?,?, q0, F, ?? is deterministic if it satisfies the following: 1. There is a partitioning Q = Q1 ?Q2 such that (a) for every q ? Q1, if (q, u, v, p) ? ? then u ? ? and v = . (b) for every q ? Q2, if (q, u, v, p) ? ? then u =  and v ? ?. 2. q0 is unique, i.e the only initial state. 3. For every input (respectively, output) symbol at most a single transition to a new state is possible. The transducer T is non-deterministic whether it satisfies these conditions or not. Theorem 5.2.4 ([41, 5]) A relation R over ?? ? ?? is rational if and only if it is recognised by a non-deterministic Bu?chi transducer. 90 CHAPTER 5. AN EXTENSION OF RATIONAL KRIPKE STRUCTURES In fact, in the literature ?-rational relations are usually defined as the class of languages accepted by Bu?chi transducers and not in terms of ?-rational expressions. As with automata, the Muller acceptance condition can be used instead of the Bu?chi condition. Definition 5.2.5 ([72, 5]) A finite transducer T = ?Q,?,?, q0, F, ?? is a Muller transducer if F ? P (Q) and it has the following acceptance conditions: A pair (?, ?) ? ?? ? ?? is recognised by T , if for ? = ?1?2 . . . ?n . . . and ? = ?1?2 . . . ?n . . . there is an infinite path p := (qi, ?1, ?1, p1) (p1, ?2, ?2, p2) . . . (qn, ?n+1, ?n+1, pn+1) . . . such that Inf (p) ? F . Lemma 5.2.6 ([5]) An ?-relation is accepted by a nondeterministic Bu?chi transducer if and only if it is accepted by a non-deterministic Muller transducer. Proof (Sketch).([5]) If a Bu?chi transducer TB = ?Q,?,?, q0, FB, ?? then TM = ?Q,?,?, q0, FM , ?? where FM = {P ? Q|P ? FB 6= ?}, is a Muller transducer which recognises the relation as TB. In [85] Thomas gives a construction of a Bu?chi automaton from a given Muller automaton such that the two automata recognise the same ?-rational language. This construction can now be modified slightly to produce a Bu?chi transducer recognising the same relation as a given Muller transducer. qed This lemma states that non-deterministic Bu?chi and Muller transducers have the same accepting power and that ?-rational relations are exactly those accepted by a non-deterministic Muller transducers. Example 5.2.7 Let R be the ?-rational relation such that two ?-words are related by R if and only if there are finitely many corresponding symbols in which they differ, i.e. R = ((0, 0) + (0, 1) + (1, 0) + (1, 1))? ((0, 0) + (1, 1))? with F = {q2}. If the transducer T given in figure 5.3 is equipped with Bu?chi acceptance conditions with F = {q2} being the set of final states, then T recognises R. By the construction given in [5] mentioned in the proof of Lemma 5.2.6, R is also accepted by T under Muller acceptance conditions if F = {{q1, q2} , {q2}}. Since q1 has no incoming edges, no pair of ?-words are accepted by T because of an infinite path p for which Inf (p) = {q1, q2}. Hence, only if Inf (p) = {q2} does the path form an accepting run. ? Rational relations over finite words can also be embedded into ?-rational relations. 5.2. ?-RATIONAL RELATIONS 91 Figure 5.3: A transducer T which can be equipped with either Bu?chi or Muller accep- tance conditions in order for it to recognise the ?-rational relation R. q1 q2 1/1 0/0 1/0 1/1 0/0 0/1 1/1 0/0 Lemma 5.2.8 A rational relation R ? ?? ? ?? can be embedded into an ?-rational relation R? ? ??? ? ??? where ?? = ? ? {?}. The proof of this lemma is analogous to the proof of lemma 5.1.7 and the idea is illustrated in the example below. Example 5.2.9 The relation R = ((0, 1) (1, 1)? (0, 1))? is recognised by the transducer in figure 5.4 and can be embedded into the relation R? = ((0, 1) (1, 1)? (0, 1))? (?,?)? which is recognised by the transducer in figure 5.5 Figure 5.4: A transducer T recognising R = ((0, 1) (1, 1)? (0, 1))?. q1 q2 0/1 0/1 1/1 Figure 5.5: A transducer T? recognising R?. q1 q2 q3 0/1 0/1 1/1 ?/? ?/? ? 92 CHAPTER 5. AN EXTENSION OF RATIONAL KRIPKE STRUCTURES 5.3 ?-rational Kripke structures Finally, rational Kripke frames (models) can be extended to ?-rational Kripke frames (models). Definition 5.3.1 An ?-rational Kripke frame is a Kripke frame ?S,R? where S is an ?-rational subset of ??, for a finite alphabet ? and R ? ????? is an ?-rational relation over ?. Definition 5.3.2 An ?-rational Kripke model is a Kripke model ?F , V ?, based on an ?-rational Kripke frame, equipped with an ?-rational valuation, i.e. V assigns an ?-rational subset of ?? to every propositional variable p ? ?. Note that the class of rational Kripke frames can be embedded into the class of ?-rational Kripke frames. Likewise for ?-rational Kripke models. This is done by embedding the universe and the relation of the structure into an ?-rational language and an ?-rational relation over the same extended alphabet. In the case of models, the regular languages assigned to the propositional variables by the valuation are also embedded into ?-rational languages over this extended alphabet. Proposition 5.3.3 The classes of ?-rational Kripke structures are finitely presentable. Proof. The set of states and the valuation can be presented by finitely many Bu?chi or Muller automata while a Bu?chi or a Muller transducer can be used to represent the relation. qed Example 5.3.4 LetM = ?S?, R?, V?? be an ?-rational Kripke model, and let the set of propositional variables be ? = {p, q}. Furthermore, let the set S? = ?? = {0, 1}? and let R? be the ?-rational relation, such that R? relates a word ? to a word ? if ? and ? share a finite prefix. Finally let V? (p) be the ?-rational language with no more than one occurrence of ?0? and V? (q) contain the ?-words in which every letter in ? occur at least once. The model M can then be finitely presented by the various machines with Bu?chi acceptance conditions in figure 5.6. ? Any rational Kripke structure has countably many states since the states are labeled by a regular language. This is however not the case for ?-rational Kripke structures. Their state spaces are labeled by ?-rational languages and can therefore be uncountable. Thus, in order to show that ?-rational Kripke frames are indeed a generalisation of rational Kripke frames I will now give an example of an ?-rational Kripke frame which is not rationally presentable. 5.3. ?-RATIONAL KRIPKE STRUCTURES 93 Figure 5.6: Bu?chi automata and transducers representing the ?-rational Kripke model M. A1 recognising S?: p1 0 1 A2 recognising V? (p): q1 q2 0 1 1  A3 recognising V ? (q): r1 r2 r3 r4 0 1 1 0 0, 1 0, 1 0, 1 0, 1 T recognising R?: s1 s2 0/1 1/0 0/0 1/1 0/0 0/1 1/0 1/1 Definition 5.3.5 The characteristic string of a subset X of N is an ?-word ? over the alphabet ? = {0, 1} such that ? (i) = 1 if i ? X for every i ? N where ? (i) is the ith character in ?. The characteristic string associated with a set X is denoted by CX. Example 5.3.6 Let F = ?P (N) ,?? be a Kripke frame with the set of subsets of the natural numbers as its universe and set inclusion as its relation. Clearly the universe is an ?-rational set of ?? - each subset is simply presented by its characteristic string. In fact ?? represents the universe. Now let X,Y ? P (N) then X ? Y if and only if CX only has a ?1? in position i if CY has a ?1? in position i. But this is exactly the relation recognised by the Bu?chi transducer in figure 5.7. Hence, F is an ?-rational Kripke frame. ? Since P (N) is uncountably infinite, it cannot be labeled by a regular language and cannot be the universe of a rational Kripke frame. 94 CHAPTER 5. AN EXTENSION OF RATIONAL KRIPKE STRUCTURES Figure 5.7: The Bu?chi transducer recognising the relation {(CX , CY ) |X ? Y }. q1 1/1 0/0 0/1 5.4 Model checking on ?-rational Kripke models In this section I investigate model checking Kt on ?-rational Kripke models. Question 5.4.1 Is model checking of Kt-formulas decidable on ?-rational Kripke mod- els? I will provide a solution similar to the case of finite words, i.e a synchronised product of transducers and automata over infinite words. It must be decided which acceptance conditions to use and how to define the acceptance conditions of the synchronised product. One may easily be tempted to alter the definition of the synchronised product of a finite automaton and a finite transducer by just adding Bu?chi acceptance conditions. From the example below it is clear that this is not sufficient and that more care must be taken with the acceptance conditions. Example 5.4.2 Let T and A, given in figure 5.8 be a Bu?chi transducer and a Bu?chi automaton recognising R? and X? respectively. Let B, see figure 5.9, be the Bu?chi automaton obtained from the synchronisation of their transition relations as well as the cross product of their sets of final states. Then B does not accept any ?-word and consequently does not recognise ?R??X?. Figure 5.8: The Bu?chi automaton A and the Bu?chi transducer T . p1 p2 1/0 0/1 q1 q2 0 1 ? Definition 5.4.3 Let T? = ?QT? ,?, q0T? , FT? , ?T?? be a Muller transducer, and let A? =?QA? ,?, q0A? , FA? , ?A?? be a Muller automaton. 5.4. MODEL CHECKING ON ?-RATIONAL KRIPKE MODELS 95 Figure 5.9: A Bu?chi automaton B. p1q1 p2q1 p1q2 p2q2 1 0 The synchronised product of T? with A? is the Muller automaton: T? iA? = ?QT? ?QA? ,?,(q0T? , q0A?) , FT?iA? , ?T?iA?? where ?T?iA? : (QT? ?QA?) ? (? ? {}) ? P(QT? ? QA?) is defined in the same way ?TiA was definined for a finite transducer T and a finite automaton A. See Definition 3.3.5 for the details. Futhermore, FT?iA? is defined as follows: Let STi ? FT? and SAj ? FA? . Then Sij = STi ? SAj . Now set Sij = P (Sij) and Sij = { Y ? S| (?q ? FT?? (r1, r2) ? Y (r1 6= q)) ? (?q ? FA?? (r1, r2) ? Y (r2 6= q)) } Finally set Fij = Sij\Sij. Then FT?iA? =?STi ?FT? , SAj ?FA? Fij Again, the synchronization of accepting runs of T? and A? is an accepting run of RTiA. Lemma 5.4.4 Let T? = ?QT? ,?, q0T? , FT? , ?T?? be a Muller transducer recognizing the ?-rational relation R(T?) and let A? = ?QA? ,?, q0A? , FA? , ?A?? be a Muller automaton recognizing the ?-rational language L(A?). Then the ?-rational language recognized by the synchronised product of T? and A? is L(T? iA?) = {u | ?w ? L(A?)(uR(T?)w)}. Lemma 5.4.5 Let ? be a finite non-empty alphabet, X? ? ?? an ?-rational subset, and let R? ? ?? ? ?? be an ?-rational relation. Then the sets ?R??X? = {u ? ??|?v ? X? (uR?v)} 96 CHAPTER 5. AN EXTENSION OF RATIONAL KRIPKE STRUCTURES and ? R?1? ? X? = {u ? ??|?v ? X? (vR?u)} are ?-rational subsets of ??. Proof. ?R??X? is the -reduction of the ?-rational language recognised by the syn- chronised product of a Muller transducer T? recognising R? and a Muller automaton A? recognising X?. qed Example 5.4.6 Suppose T? and A? are the transducer and automaton in Example 5.4.2 respectively, but both with the Muller acceptance condition for FT? = {p1, p2} and FA? = {q1, q2}. Let R? be the ?-rational relation recognised by T? and X? the ?-rational relation recognised by A?. Then {(p1, q1) , (p2, q2)} ? FT?iA? , and the syn- chronised product of T? and A? recognise ?R??X?. ? Global model checking of a formula in an ?-rational Kripke model, is defined as before: it produces the set of states, which satisfies the formula, symbolically. In the case of local model checking a formula, one needs to be more careful since the states are encoded as ?-sequences. There are uncountably many ?-sequences, while only countably many presentation. Therefore, local model checking a formula on an ?-rational Kripke model will be restricted to those states which can be represented by a Bu?chi-automaton, i.e. local model checking can be done at a state s if the set {s} forms an ?-rational language. Theorem 5.4.7 Local and global model checking of formulas in Kt on ?-rational Kripke models are decidable. Moreover, for every basic modal formula ? and every ?-rational Kripke modelM, the set [|?|]M is an effectively computable ?-rational language. Theorem 5.4.8 Local and global model checking of formulas from the hybrid language Ht (U) is decidable on ?-rational Kripke models and as before the set [|?|]M is an ?- rational language for every formula ? ? Ht (U) and every ?-rational modelM. The proofs of these two results are analogous to proofs for rational Kripke models. The claims follow from the closure properties of ?-rational languages as well as Lemma 5.4.5. It turns out that no expressiveness in terms of decidable model checking is sacri- ficed with the extension of rational Kripke structures to ?-rational Kripke structures - therefore justifying the study of ?-rational Kripke structures. Chapter 6 Conclusion 6.1 Summary In this dissertation I have studied Rational Kripke models - a study motivated by increasing interest in model checking in infinite structures. In particular, it has been shown that global and local model checking of formulas of the basic tense logic Kt (and the hybrid extension Ht (U) thereof) on rational Kripke models are decidable. Moreover, a constructive proof is presented where an automaton recognising the regular language ?R?X is given explicitly. The class of regularity preserving relations has been studied and two new types of two-sorted algebras have be defined: regularity preserving- and rational-Boolean algebras. The classes of regularity preserving and rational relations then respectively form algebras of the two types. Model theoretic results for rational Kripke models have been presented and in par- ticular bisimulation equivalence between rational Kripke models has been studied. It is shown that bisimilarity between a given pointed rational Kripke modal and a given finite pointed Kripke model is decidable. I have also studied three subclasses of rational Kripke structures and summarised some of the existing results on these structures. The hybrid language Ht (U,3?) turns out to be useful in expressing reachability between two given states, and as a result model checking pure formulas of Ht (U,3?) is decidable on rational Kripke tree models and monotonous rational Kripke models. Finally, rational Kripke models have been extended to ?-rational Kripke models. This extension is justified by the decidability of model checking formulas of Kt in ?-rational Kripke models. 97 98 CHAPTER 6. CONCLUSION 6.2 Applications I will now briefly discuss two potential applications of the model checking modal logic to the formal verification of infinite state systems. 6.2.1 Regular model checking A potential application is regular model checking [73]. This is a framework for algorith- mic verification of generally infinite state systems which essentially involves computing reachability sets in regular Kripke models. In [20] Bouajjani et al. present two comple- mentary techniques for solving two major problems in verification, namely computing the set of states reachable from a set of initial states, and computing the transitive closure of the transition relation. The first technique is direct automata-theoretic construction. Here the column transducer recognising the transitive closure of a length-preserving regular relation R is constructed. The column transducer is however not finite in general. In [52] Jonsson and Nilsson gave some sufficient conditions under which the transitive closure of a length-preserving regular relation is itself regular. For these relations the column transducer will be finite. These are only sufficient conditions for the transitive closure to be regular and there are many other relations for which the column transducer is also finite. Since the transitive closure of a relation can be used to compute the set of reachable states, this serves as a solution to both problems mentioned. The second technique discussed in [20] involves widening on regular sets - these are techniques to compute the effect of iterating a length-preserving regular relation. The idea is to guess automatically what the image will be when iterating a relation and starting with a given regular set, and then to decide whether the guess is correct. The guessing is done by comparing the given starting regular set X with the regular set R (X). A fixpoint test is used to ensure that an upper approximation of the set of reachable states is guessed. These techniques can now be generalised for rational relations instead of length- preserving regular relations. In the first case the only difference would be that since the relation R will now be rational, the transducer accepting it will be rational and therefore will accept -transitions. This does not affect the construction of the column transducer. Similarly, the widening on regular sets can be applied to rational relations. 6.2.2 Bounded model checking In [57] Schneider et al. describe a forerunner of bounded model checking. Bounded model checking has been introduced in [9] by Biere et al, and has since been studied extensively, see for instance [8], as an alternative to symbolic model checking techniques where binary decision diagrams (data structures used to represent Boolean functions) 6.2. APPLICATIONS 99 are used [1, 60, 68]. Most propositional binary decision diagrams suffer from an unavoid- able exponential blow-up [65]. Consequently model checkers based on binary decision diagrams may fail on relatively small models. Bounded model checking was introduced in an attempt to deal with cases like these. The basic idea behind bounded model checking is to reduce the model checking task to the satisfiability problem of some base logic. The base logic is usually proposi- tional logic and the model checking task is usually reduced to the Boolean satisfiability problem (SAT). In technical terms, the specification to be model checked (expressed in temporal logic) is unwound a finite number of times to obtain a formula in the base logic. Therefore bounded model checking is mainly used for the verification or falsification of liveness and safety properties respectively. Safety properties are specifications that hold invariantly along a given path whereas liveness properties are specifications which must hold at least once along a given path. Bounded model checking is used to produce counterexamples for safety properties or witnesses for liveness properties. Properties like liveness and safety can be expressed in linear- and branching-time temporal logics. Example 6.2.1 The linear-time temporal formula ? = Fp in LTLpast specifies a live- ness property: eventually there must be a state that satisfies the atomic proposition p. The branching-time formula A? in CTL? specifies that the liveness property must hold along every path (starting at the current state). The formula ? = G (p ? q) in LTLpast specifies a safety property: at least one of p and q must always be satisfied. Then E? ? CTL? states that there must be a path starting at the current state such that at least one of p and q is satisfied at every state in the path. ? Model checking of these properties on models with infinite state-spaces is therefore undecidable. It then follows that bounded model checking is an incomplete infinite-state verification method. Moreover, even though some problems can be solved by bounded model checking but cannot be solved by BDD-base model checking techniques, the converse is also true. Some problems can be solved better by BDD-based techniques. Bounded model checking is therefore an automatic verification method that supplements other existing methods but does not replace any of them [8]. Furthermore, since bounded model checking relies on an exponential procedure it does not solve the complexity problem of model checking. Some interesting problems can however be solved faster by bounded model checking. In [35] the infinite state models (transition systems) on which model checking is done must be expressible in terms of a set of Boolean constraints. In [82, 81] integer Kripke models, where the relation and assignment must be expressible expressible in 100 CHAPTER 6. CONCLUSION Presburger arithmetic, are used. Consequently, the bounded model checking techniques were studied with rather restricted classes of infinite structures in mind. Alternatively, the class of rational Kripke models is a very general class of (possi- bly) infinite structures on which model checking the basic tense logic Kt is decidable. Rational Kripke models are thus suitable candidates for bounded model checking of temporal logic formulas with Kt as the base logic. 6.3 Open problems As I have said before, rational graphs have not been studied very widely in the literature. Consequently, there are still many unanswered questions concerning rational Kripke structures. Firstly, an open problem is given in the form of a conjecture in Chapter 3: ?The expression complexity of global model checking of a Kt-formula is non-elementary in terms of the alternating box rank of the formula.? Natural questions that arise from this study: ?What is the strongest modal language for which model checking is decidable on rational Kripke models?? ?Are there other modal operators which preserve regularity but are not definable in the hybrid extension ofKt that can be added to the language?? Identification of such modalities will motivate model checking on rational Kripke models even further. On the other hand, an important task would be to identify natural subclasses of rational Kripke models where model checking of Kt extended with reachability is de- cidable. Concerning the model constructions on rational Kripke frames, the following two questions still need to be answered: 1. Is the unfolding of a rational Kripke frame a rational Kripke tree? (This question was only answered for finite Kripke frames.) 2. Given a pointed rational Kripke modelM, isM finite up to bisimulation? This problem is semi-decidable from the Paige-Tarjan algorithm. I conjecture that this problem is at most semi-decidable. However, this must still be proved. Rational Kripke trees have decidable first-order theories. As a result model checking tasks of formulas fromHt (U, ?, ?) is decidable for rational Kripke tree models. However, the follow question still needs to be answered: ?If M is a rational Kripke tree model, is the set [|?|] for ? ? Ht (U, ?, ?) a regular language?? Rational Kripke models have been generalised to ?-rational Kripke models in this dissertation. They can now also be generalised to tree rational and ?-tree rational Kripke models. 6.3. OPEN PROBLEMS 101 Finally, is it the case that when a modal formula ? is satisfiable in a rational Kripke frame (i.e. there exists a valuation and state where it is true) then there exists a rational valuation satisfying ?? 102 CHAPTER 6. CONCLUSION Bibliography [1] S.B. Akers. Binary decision diagrams. IEEE Transactions on Computers, C- 27(6):509?516, June 1978. [2] J.A. Anderson. Discrete Mathematics with Combinatorics. Prentice Hall, 2001. [3] J.-M. Autebert and L. Boasson. Transductions rationelles. Ed. Masson, 1988. [4] Y.M. Barzdin and B.A. Trakhtenbrot. Finite Automata, Behavior and Synthe- sis. North-Holland publishing company, Amsterdam, 1973. Translated form the Russian by D. Louvish, English translation edited by E. Shamir and L. H. Landwe- ber, Fundamental Studies in Computer Science, Vol. 1. [5] M.P. Be?al and O. Carton. Determinization of transducers over infinite words: the general case. Theory Comput. Syst., 37(4):483?502, June 2004. [6] W. Bekker and V. Goranko. Symbolic model checking of tense logics on rational kripke models. In The Proceedings of the 5th Workshop ?Methods for modalities? (M4M5). Electronic notes of Theoretical Computer Science, 2007. To appear. [7] J. Berstel. Transductions and Context-Free Languages. Teubner Studienbu?cher, Stuttgart, 1979. [8] A. Biere, E.M. Clarke, A. Cimatti, O. Strichman, and Y. Zhu. Bounded model checking, volume 58, chapter 3, pages 118?149. Academic Press, 2003. [9] A. Biere, E.M. Clarke, A. Cimatti, and Y. Zhu. Symbolic model checking without BDDs. In TACAS ?99: Proceedings of the 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems, pages 193?207, London, UK, 1999. Springer-Verlag. [10] P. Blackburn. Tense, temporal reference, and tense logic. Journal of Semantics, 11:83?101, 1994. [11] P. Blackburn. Representation, reasoning, and relational structures: a hybrid logic manifesto. Logic Journal of the IGPL, 8(3):339?625, 2000. 103 104 BIBLIOGRAPHY [12] P. Blackburn, M. de Rijke, and Y. Venema. Modal logic. Cambridge University Press, New York, NY, USA, 2001. [13] P. Blackburn and J. Seligman. Hybrid languages. Journal of logic, language and information, 4(3):251?272, 1995. [14] P. Blackburn and J. Seligman. What are hybrid languages? In M. de Rijke, M. Kracht, H. Wansing, and M. Zakharyaschev, editors, Advances in modal logic, volume 1, pages 41?62. CSLI Publications, Stanford University, 1998. [15] A. Blumensath. Automatic structures. Diploma thesis, RWTH-Aachen, 1999. [16] A. Blumensath and E. Gra?del. Automatic structures. In LICS ?00: Proceedings of the 15th Annual IEEE Symposium on Logic in Computer Science, pages 51?62, Washington, DC, USA, 2000. IEEE Computer Society. [17] A. Blumensath and E. Gra?del. Finite presentations of infinite structures: Au- tomata and interpretations. Theory of Computing Systems, 37:641 674, 2004. [18] L. Boasson and M. Nivat. Adherences of languages. Journal of Compt. System Sci, 20(3):285?309, 1980. [19] A. Bouajjani, J. Esparza, and O. Maler. Reachability analysis of pushdown au- tomata: Application to model-checking. In A. Mazurkiewicz and J. Winkowski, editors, Proc. of CONCUR ?97, volume 1243 of LNCS, pages 135?150. Springer, 1997. [20] A. Bouajjani, B. Jonsson, M. Nilsson, and T. Touili. Regular model checking. In CAV ?00: Proceedings of hte 12th International Conference on Computer aided verfication, pages 403?418, London, UK, 2000. Springer-Verlag. [21] C. Brink. Boolean modules. Journal of Algebra, 72(2):29?313, 1981. [22] C. Brink, K. Britz, and R.A. Schmidt. Peirce algebras. Research Report MPI-I- 92-229, Max-Planck-Institut fu?r Informatik, Im Stadtwald, D-66123 Saarbru?cken, Germany, July 1992. [23] J.R. Bu?chi. Weak second-order arithmetic and finite automata. Z. Math. logik Grundl. Math., 6:66?92, 1960. [24] J.R. Bu?chi. On a decision method in restricted second-order arithmetic. In E. Nagel et al., editor, Logic, Methodology and Philosophy of Science, pages 1?11. Stanford University Press, Stanford, 1962. [25] S. Burckel. Functional equations associated with congruential functions. Theoret- ical Computer Science, 123(2):397?406, 1994. BIBLIOGRAPHY 105 [26] G.W. Cannon, D.S.A. Epstein, D.F. Holt, S.V. Levy, M.S. Paterson, and W.P. Thurston. Word Processing in Groups. A.K. Peters, Ltd., Natick, MA, USA, 1992. [27] A. Carayol and C. Morvan. On rational trees. In Zolta?n ?Esik, editor, CSL, volume 4207 of Lecture Notes in Computer Science, pages 225?239. Springer, 2006. [28] D. Caucal. On infinite transition graphs having a decidable monadic theory. In ICALP ?96: Proceedings of the 23rd International Colloquium on Automata, Lan- guages and Programming, pages 194?205, London, UK, 1996. Springer-Verlag. [29] D. Caucal and T. Knapik. A Chomsky-like hierarchy of infinite graphs. In MFCS ?02: Proceedings of the 27th International Symposium on Mathematical Founda- tions of Computer Science, pages 177?187, London, UK, 2002. Springer-Verlag. [30] E.M. Clarke and E.A. Emerson. Design and synthesis of synchronization skeletons for branching time temporal logic. In Proceedings of the Workshop of logic of programs, volume 131 of LNCS, pages 52?71, Yorktown Heights, New York, USA, 1981. Springerverlag. [31] E.M. Clarke and E.A. Emerson. Using branching time logic to synthesize synchro- nization skeletons. Science of computer programming, 2:241?266, 1982. [32] E.M. Clarke and B.H. Schlingloff. Model checking. In A. Robinson and A. Voronkov, editors, Handbook of automated reasoning, chapter 24, pages 1635? 1790. Elsevier Science Publishers, 2002. [33] L. Collatz. On the origin of the (3n+1)-problem. volume 3 of 12, pages 9?11. Journal of Qufu Normal University, 1986. (Chinese, transcribed by Zhi-Ping Ren)[German translation: ?Uber den Ursprung des (3n+1)-Problems, by Zhang- Zheng Yu 1991, Hamburg]. [34] J.H. Conway. Unpredictable iterations. In Proceedings of the Number Theory conference, pages 49?52, University of Colorado, Boulder, 1972. [35] L.M. de Moura, H. Rue?, and M. Sorea. Lazy theorem proving for bounded model checking over infinite domains. In CADE-18: Prodeedings of the 18th Interna- tional Conference on Automated Deduction, volume 2392 of LNCS, pages 438?455, London, UK, July 2002. Springer-Verlag. [36] S. Eilenberg. Automata, Languages and Machines, volume A. Academic Press, New York, 1974. [37] C. Elgot and J. Mezei. On relations defined by finite automata. IBM Journal of Research and Development, 9:47?68, 1965. 106 BIBLIOGRAPHY [38] J. Esparza. An automata-theoretic approach to software verification. In Develop- ments in Language Theory, volume 2710 of LNCS, page 164, 2003. [39] J. Esparza and P. Janc?ar. Deciding finiteness of Petri nets up to bisimulation. In ICALP ?96: Proceedings of the 23rd International Colloquium on Automata, Languages and Programming, pages 478?489, London, UK, 1996. Springer-Verlag. [40] J. Esparza, A. Kucera, and S. Schwoon. Model-checking LTL with regular val- uations for pushdown systems. In Proc. of TACS ?2001, volume 2215 of Lecture Notes in Computer Science, pages 306?339, 2001. [41] O. Finkel. On infinitary rational relations and Borel sets. In DMTCS, pages 155?167, 2003. [42] O. Finkel. Undecidability of topological and arithmetical properties of infinitary rational relations. Informatique The?orique et Applications, 37(2):115?126, 2003. [43] M.J. Fisher and M.O. Rabin. Super-exponential complexity of Presburger arith- metic. In Proceedings of the SIAM-AMS Symposium in Applied Mathematics, volume 7, pages 27?41, 1974. [44] C. Frougny and J. Sakarovitch. Synchronized rational relations of finite and infinite words. Theoretical Computer Science, 108(1):45?82, 1993. [45] F. Gire and M. Nivat. Relations rationnelles infinitaires. Calcolo, 21(2):91?125, June 1984. [46] V. Goranko. Infinite state model checking in modal logic. In Prakash Panangaden, editor, Proceedings of the Twentieth Annual IEEE Symp. on Logic in Computer Science, LICS 2005. IEEE Computer Society Press, June 2005. Short Presentation. [47] V. Goranko and M. Otto. Model theory of modal logic. In P. Blackburn, F. Wolter, and J. van Benthem, editors, Handbook of Modal Logic, pages 255?325. Elsevier, 2006. [48] B.R. Hodgson. On direct products of automaton decidable theories. Theoretical Computer Science, 19:331?335, 1982. [49] P. Janc?ar. Undecidability of bisimilarity for Petri nets and some related problems. Theoretical Computer Science, 148(2):281?301, 1995. [50] P. Janc?ar and J. Srba. Undecidability results for bisimilarity on prefix rewrite sys- tems. In Proceedings of 9th International Conference on Foundations of Software Science and Computation Structures (FOSSACS?06), volume 3921 of LNCS, pages 277?291. Springer-Verlag, 2006. BIBLIOGRAPHY 107 [51] J.H. Johnson. Rational equivalence relations. Theoretical Computer Science, 47(3):39?60, 1986. [52] B. Jonsson and M. Nilsson. Transitive closures of regular relations for verifying infinite-state systems. In TACAS ?00: Proceedings of the 6th international con- ference on tools and algorithms for construction and analysis of systems, pages 220?234, London, UK, 2000. Springer-Verlag. [53] Y. Kesten, O. Maler, M. Marcus, A. Pnueli, and E. Shahar. Symbolic model checking with rich assertional languages. Theoretical Computer Science, 256(1- 2):93?112, 2001. [54] B. Khoussainov and A. Nerode. Automatic presentations of structures. In LCC ?94: Selected Papers from the International Workshop on Logical and Computational Complexity, pages 367?392, London, UK, 1995. Springer-Verlag. [55] B. Khoussainov, A. Nies, S. Rubin, and F. Stephan. Automatic structures: Rich- ness and limitations. In LICS ?04: Proceedings of the 19th Annual IEEE Sym- posium on Logic in Computer Science (LICS?04), pages 44?53, Washington, DC, USA, 2004. IEEE Computer Society. [56] B. Khoussainov, S. Rubin, and F. Stephan. Automatic linear orders and trees. ACM Trans. Comput. Logic, 6(4):675?700, 2005. [57] T. Kropf, R. Kumar, and K. Schneider. Alternative proof precedures for finite-state machines in higher-order logic. In HUG ?03: Proceedings of the 6th international Workshop on higher-order logic theorem proving and its applications, pages 213? 226, London, UK, 1994. Springer-Verlag. [58] G.M. Kuper and M.Y. Vardi. On the complexity of queries in the logical data model. In Lecture notes in computer science on ICDT ?88, pages 267?280, New York, NY, USA, 1988. Springer-Verlag New York, Inc. [59] O. Kupferman, M. Y. Vardi, and P. Wolper. An automata-theoretic approach to branching-time model checking. Journal of the ACM, 47(2):312?360, March 2000. [60] C.Y. Lee. Representation of swithching circuits by binary decision programs. Bell Systems Techinical Journal, 38:985?999, 1959. [61] A.H. Lewis. An introduction to Petri nets. George Mason University, 1999. http://ict.tippinst.ie/%7Ejhannafin/RandD/petri-intro.pdf. [62] R. Lindner and L. Staiger. Algebraische codierungsteorie -theorie der sequentiellen codierunge. Akademie-Verlag, 1977. 108 BIBLIOGRAPHY [63] N. Markey. Temporal logics. Course notes, Master Parisien de Recherche en Informatique, Paris, France, 2006. [64] R. McNaughton. Testing and generation infinite sequences by a finite automaton. Information and Control, 9:521?530, 1966. [65] C. Meinel and T. Theobald. Algorithms and Data Structures in VLSI Design: OBDD - Foundations and Applications. Springer-Verlag, Berlin, 1998. [66] A. Meyer. Finitely presented infinite graphs. The`se de doctorat, University of Rennes, October 2005. [67] A. Moen. Introduction to Petri nets, 2003. Lecture notes, http://www.ifi.uio.no/dbsem/foils2003vaar/. [68] B.M.E Moret. Decision trees and diagrams. ACM Computing Surveys, 14(4):593? 623, 1982. [69] C. Morvan. On rational graphs. Rapport de recherche 3944, INRIA, Mai 2000. [70] C. Morvan. Les graphes rationnels. The`se de doctorat, Universit de Rennes 1, 2001. [71] C. Morvan. Classes of rational graphs. http://www.irisa.fr/JM06/Papers/morvan.pdf, 2006. [72] D.E. Muller. Infinite sequences and finite machines. In Proc. 4th IEEE Symp. on Switching Circuit Theory and Logical Disign, pages 3?16, 1963. [73] M. Nilsson. Regular model checking. Phd. thesis, Uppsala University, Uppsala, Sweden, March 2005. [74] M. Nivat. Transductions des langages die Chomsky. Ann. Inst. Fourier (Grenoble), 18:339?456, 1968. In French. [75] D. Perrin and J.E. Pin. Infinite words, volume 141 of Pure and Applied Mathe- matics. Elsevier, 2004. ISBN 0-12-532111-2. [76] M. Presburger. ?Uber die vollstaendigkeit eines gewissen systems der arithmetik ganzer zahlen in welchem die addition als einzige operation hervortritt. Comptes Rendus du I congre?s de Mathematiciens des Pays Slaves, pages 92?101, 1929. [77] M.O. Rabin. Decidability of second-order theories and automata on infinite trees. Trans. Amer. Math. soc., 141:135, 1969. BIBLIOGRAPHY 109 [78] C. Rispal. The synchronized graphs trace the context-sensitive languages. In Pro- ceedings of the 4th International Workshop on Verification of Infinite-State Sys- tems (Infinity 2002), volume 68. Electronic notes of Theoretical Computer Science, 2002. [79] S. Rubin. Automatic Structures. PhD thesis, The University of Auckland, 2004. [80] N. Sa?ntean. Memento transducers. Reading Course Presentation,CS 900 Readings in Computer Science, 2002. [81] K. Schneider and T. Schuele. Bounded model checking of infinite state systems: exploiting the automata hierarchy. In Proceedings of the second ACM and IEEE International Conference on Formal Methods and Models for Co-Design, (MEM- OCODE), pages 17?26, San Diego, CA, USA, June 2004. IEEE Computer Society. [82] K. Schneider and T. Schuele. Bounded model checking of infinite state systems. Form. Methods Syst. Des., 30(1):51?81, 2007. [83] C. Stirling. The joys of bisimulation. In MFCS ?98: Proceedings of the 23rd In- ternational Symposium on Mathematical Foundations of Computer Science, pages 142?151, London, UK, 1998. Springer-Verlag. [84] T.A. Sudkamp, editor. Languages and machines : an introduction to the theory of computer science. Addison-Wesley Longman Publishing Co., Inc., Boston, MA, USA, 1988. [85] W. Thomas. Languages, automata and logic. In Handbook of formal languages, vol. 3: beyond words, pages 389?455. Springer-Verlag New York, Inc., New York, NY, USA, 1997. [86] W. Thomas. A short introduction to infinite automata. In DLT ?01: Revised Papers from the 5th International Conference on Developments in Language Theory, pages 130?144, London, UK, 2002. Springer-Verlag. [87] W. Thomas. Constructing infinite graphs with a decidable MSO-theory. In B. Rovan and P. Vojta`s, editors, MFCS, volume 2747 of Lecture Notes in Computer Science, pages 113?124. Springer, 2003. [88] Tanguy Urvoy. Regularity of congruential graphs. In MFCS ?00: Proceedings of the 25th International Symposium on Mathematical Foundations of Computer Science, pages 680?689, London, UK, 2000. Springer-Verlag. [89] J. van Benthem. Modal logic and classical logic. Bibliopolis, 1983. 110 BIBLIOGRAPHY [90] M.Y. Vardi. An automata-theoretic approach to linear temporal logic. In F. Moller and G. Birtwistle, editors, Logics for Concurrency: Structure versus Automata, volume 1043 of Lecture Notes in Computer Science, pages 238?266. Springer- Verlag, Berlin, 1996. [91] Y. Venema. Temporal logic. In L. Globe, editor, The Blackwell Guide to Philo- sophical Logic, pages 203?223. Blackwell Publishers, 2001. [92] I. Walukiewicz. Model checking CTL properties of pushdown systems. In FSTTCS, pages 127?138, 2000.