Protoautomata as Models of Systems with Data Accumulation Irina Mikhailova1 and Boris Novikov2 and Grygoriy Zholtkevych2 1 Luhansk Taras Shevchenko National University, Institute of Information Technology, 2, Oboronna Str., 91011, Luhansk, Ukraine mia irina@rambler.ru 2 V.N. Karazin Kharkiv National University, School of Mathematics and Mechanics, 4, Svobody Sqr., 61022, Kharkiv, Ukraine {bvnovikov46,g.zholtkevych}@gmail.com Abstract. In the paper formal models of software systems and their components based on the notion of an abstract machine are discussed. Necessity to model systems with data accumulation sets the problem of study of generalizations of the notion of an abstract automaton. In the paper two generalizations, namely, preautomata and protoautomata, are considered. It is shown that passing from automata via preautomata to protoautomata can be naturally realized using the language and methods of category theory. Keywords. system modelling, abstract automaton, category of automata, preautomata, category of preautomata, globalization, protoautomaton, category of protoautomaton, reflector, free protoautomaton Key terms. MathematicalModel, SpecificationProcess, VerificationPro- cess 1 Introduction Theory of abstract state machines or abstract automata is widely applied in different areas of Computer Science. While the early applications of automata theory were connected with theory of compilators design (see, for example, [1]), the more recent its applications are focused on the problems of specification and verification of behaviour of software components [3, 11]. Such changing of the object of the theory was marked by R. Milner in [11]: “In the classical theory, rather little attention is paid to the way in which two automata may interact, in the sense that an action by one entails a complementary action by another. This kind of interaction requires us to look at automata in new light; in particular, this interdependency of automata via their actions seems to demand a new approach to behavioural equivalence”. Protoautomata as Models of Systems with Data Accumulation 583 But the practice of modelling system behaviour based on the automata ap- proach has shown that the approach is inadequate if data accumulation for the correct response is necessary. Using the concept of partial action of a semigroup on a set [7, 10], we have defined the notion of preautomaton and studied its properties [4, 12]. The further study has shown that preautomata can be used for modelling some aspects of behaviour of systems with a delayed response [13, 14]. In this paper, we consider a more general class of automaton-liked systems — the class of protoautomata. All necessary information from the theory of semi- groups, automata theory, and category theory can be found in the monographs [5, 6, 8, 9]. We use the notation ϕ : A 99K B for the partial mapping of A to B (unlike the complete mapping A → B). If ϕ(a) is not defined for a ∈ A, we write ϕ(a) = ∅. The free monoid on the alphabet Σ is denoted by Σ ∗ , and its unit by ε. All actions and preactions used in the paper are right, as it is common in the automata theory. 2 Preliminaries We will use the definition of the automaton in the following form (the condition of the finiteness is ignored): Definition 1. Given a set X and a free monoid Σ ∗ over the alphabet Σ, an automaton is a mapping X × Σ ∗ → X : (x, a) 7→ xa such that for all x ∈ X and u, v ∈ Σ ∗ xε = x, (1) x(uv) = (xu)v. (2) More general concept is the following Definition 2 (see [4]). A preautomaton is such a partial mapping of X × Σ ∗ 99K X : (x, a) 7→ xa, that a) the condition (1) is fulfilled; b) if xu 6= ∅ and (xu)v 6= ∅, then x(uv) 6= ∅ and equality (2) is fulfilled; c) if xu 6= ∅ and x(uv) 6= ∅, then (xu)v 6= ∅ and equality (2) is fulfilled. The preautomata over the monoid Σ ∗ form a category PAut(Σ); its mor- phisms are such maps ϕ : X → Y that (∀ a ∈ Σ ∗ )(∀ x ∈ X)( xa 6= ∅ =⇒ ∅ 6= ϕ(x)a = ϕ(xa)). (3) The category Aut(Σ) of the automata over Σ is a full subcategory of PAut(Σ). Preautomata appear in the following situation. Let Y be an automaton and X an arbitrary nonempty subset of Y . Then a restriction of an action on X is a preautomaton. Conversely, let X × M 99K X be a preautomaton. The construction which is inverse to restriction is called globalization. More precisely: 584 I. Mikhailova, B. Novikov and G. Zholtkevych Definition 3. A globalization of the preautomaton X is an automaton Z with an injection ι : X → Z such that for all a ∈ Σ ∗ , x ∈ X xa 6= ∅ =⇒ ∅ 6= ι(x)a = ι(xa), ι(x)a ∈ ι(X) =⇒ xa 6= ∅ & ι(xa) = ι(x)a. Obviously, ι is a morphism of PAut(M ). We also call it a globalization. Definition 4. A globalization ι : X → Z is called universal if for any global- ization ι0 : X → Z 0 there is an unique morphism κ : Z → Z 0 such that ι0 = κι. The following construction gives an universal globalization (obviously unique up to isomorphism) for any preautomaton X × Σ ∗ 99K X. Define a relation ` on the set X × Σ ∗ : (x, ab) ` (xa, b) ⇐⇒ xa 6= ∅. (4) Let ' be an equivalence relation generated by `, and X U = (X × Σ ∗ )/ '. An equivalence class of ' containing a pair (x, a) is denoted by [x, a]. For [x, a] ∈ X U and b ∈ Σ ∗ , we set [x, a]b = [x, ab]. Thus a complete action on X U is defined. Theorem 1. The automaton X U with a morphism ιU : X → X U : x 7→ [x, ε] is the universal globalization of the preautomaton X. Proof. See [4, Theorem 2] t u 3 Protoautomata The main object of this paper is a generalization of the notion of preautomaton: Definition 5. A protoautomaton is a partial mapping X × Σ ∗ 99K X : (x, a) 7→ xa such that a) the condition (1) is fulfilled; b) if xu 6= ∅ and (xu)v 6= ∅, then x(uv) 6= ∅ and equality (2) is fulfilled. We will also denote the protoautomaton from this definition simply by X, if it does not cause a confusion. Example 1. Let S be a free subsemigroup of Σ ∗ and α : X × S → X an au- tomaton. Define a partial mapping X × Σ ∗ 99K X as an extension of α, putting xu = ∅ for u ∈ Σ ∗ \ S; so we get a protoautomaton over Σ ∗ . Note that in general it is not a preautomaton. In addition, this example shows that the au- tomaton over an infinite alphabet can be represented as a protoautomaton over a two-letter alphabet. Example 2. Let X = {x, y} be a two-element set, L a subset of Σ ∗ . Define a protoautomaton X × Σ ∗ 99K X putting for a 6= ε  y, if a ∈ L, xa = ∅, if a ∈ / L, and ya = ∅. This example shows that protoautomata recognize all languages. Protoautomata as Models of Systems with Data Accumulation 585 We denote the category of protoautomata with morphisms defined by the condition (3) by PtAut(Σ); clearly, PAut(Σ) is its subcategory. It follows from the theory of partial action of semigroups [6, Theorem 5.7], that a protoautomaton which is not a preautomaton has no globalization. More precisely, for the protoautomaton X we can construct an automaton X U as in Sec. 2, but in this case the morphism ιU is not injective in general. In this situation, the concept of a reflector is useful. We recall its definition [9]: Definition 6. A subcategory D of a category C is called reflective if with each object C ∈ C an object RD (C) ∈ D is associated (called D-reflector of the object C) and a morphism ρD (C) : C → RD (C) (reflection morphism) such that for each D ∈ D the diagram ρD (C) C −→ RD (C) ↓ D can be extended uniquely to a commutative diagram by some morphism out HomD (RD (C), D). It is convenient to use another description of the equivalence ': Lemma 1. Define a relation ] on the set X × Σ ∗ : (x, a) ] (y, b) ⇐⇒ (∃ a0 , b0 , p ∈ Σ ∗ )(a = a0 p & b = b0 p & xa0 = yb0 6= ∅). Let ≈ be the equivalence relation generated by ]. Then ≈ coincides with '. Proof. If (x, a) ] (y, b) then (x, a) = (x, a0 p) ` (xa0 , p) = (yb0 , p) a (y, b0 p) = (y, b), whence ≈ ⊆ '. Conversely, if (x, a) ` (y, b), then a = cb, y = xc for some c ∈ Σ ∗ . Hence ` ⊆ ]. Consequently, ≈ ⊇ ' t u Remark 1. Obviously, ` is reflexive and transitive, while ] is reflexive and sym- metric. Lemma 2. Let X be a protoautomaton, Y be a preautomaton (both over Σ ∗ ), α : X → Y be a morphism, x, y ∈ X, a ∈ Σ ∗ . Then [x, ε] = [y, a] implies α(x) = α(y)a 6= ∅.. Proof. It follows from the condition that (x, ε) ] (z1 , b1 ) ] . . . ] (zn , bn ) ] (y, a) for some z1 , . . . , zn ∈ X, b1 , . . . , bn ∈ Σ ∗ . 586 I. Mikhailova, B. Novikov and G. Zholtkevych Apply induction on n. Since x = z1 b1 6= ∅ then α(x) = α(z1 )b1 . Suppose that α(x) = α(zn )bn 6= ∅. By definition of the relation ] bn = cp, a = dp, zn c = yd 6= ∅ for some c, d, p ∈ Σ ∗ . Then α(zn )c 6= ∅ and by the induction α(zn )(cp) 6= ∅. Since Y is a preautomaton then α(x) = α(zn )(cp) = α(zn c)p = α(yd)p = (α(y)d)p = α(y)a. Proof has completed t u Similarly (and even easier) one can prove Lemma 3. Let X be a protoautomaton, Y be an automaton (both over Σ ∗ ), α : X → Y be a morphism, x, y ∈ X, a, b ∈ Σ ∗ . Then [x, a] = [y, b] implies α(x)a = α(y)b. Proof is omitted t u We set [X, ε] = {[x, ε] ∈ X U | x ∈ X}. Obviously, [X, ε], being a subset of X U , is a preautomaton, and in addition, ιU (X) = [X, ε]. Theorem 2. Let X be a protoautomaton over Σ ∗ , then 1. [X, ε] is a reflector for X in the category PAut(Σ), 2. X U is a reflector for X in Aut(Σ), 3. X U is a reflector for [X, ε] in Aut(Σ). Proof. 1) Let Y be some preautomaton and α : X → Y be a morphism of protoautomata. The required morphism β : [X, ε] → Y is uniquely determined from the equality α = βιU . Indeed, for x ∈ X we have α(x) = βιU (x) = β([x, ε]). It follows from Lemma 2 that β is well-defined. 2) Similarly, using Lemma 3. 3) Follows from 1), 2), and the following well-known fact [9]: If A ⊂ B ⊂ C are categories, A is reflective in B, and B is reflective in C, then A is reflective in C. Moreover, the reflection morphism from C to A is the product of the corresponding reflection morphisms from C to B and from B to A t u Corollary 1. Aut(Σ) is a reflective subcategory of PAut(Σ). Moreover, the universal globalization of a preautomaton is its reflector. Example 3. Let X = {x, y, z, t}, p, u, v ∈ Σ ∗ \ {ε}. We set zu = zv = t, z(up) = x, z(vp) = y and sw = ∅ for all s ∈ X, w ∈ Σ ∗ \ {ε, p, u, v}. In such a manner X turns into a protoautomaton. Since (x, ε) ] (z, up) ] (z, vp) ] (y, ε) then [x, ε] = [y, ε] and the reflection morphism of X is non-injective. A large class of protoautomata is contained in the following example. Protoautomata as Models of Systems with Data Accumulation 587 Example 4. Consider a preautomaton X × Σ ∗ 99K X as a directed weighted multigraph with states as vertices and with edges of the form (x, u, y), where x, y ∈ X, u ∈ Σ ∗ , and y = xu. Let U be an arbitrary subset of edges of X. Build a transitive closure U t of the set U , extending it step by step by the rule: if the edges (x, u, y) and (y, v, z) are at some stage in the expansion, then on the next step we include the edge (x, uv, z). Then U t is a protoautomaton. Example 3 shows that there exists a protoautomaton such that it can not be embedded into some preautomaton (and thus into some automaton). 4 Free Protoautomata It is well known [2] that free automata play a significant role in the theory of automata (for example, in the problem of constructing a minimal realization). Therefore, it is advisable to consider the question about the existence of free objects in the category of protoautomata. Recall the necessary definitions: Definition 7. Let C and D be categories, F : C D be a functor, C be an object of C. An object D of D is called free on C with respect to the functor F , if there is a morphism α : C → F D such that for any object D0 ∈ D and any morphism β : C → F D0 there exists the unique morphism γ : D → D0 such that F (γ)α = β. (5) We consider a category Rel(Σ) whose objects are pairs (X, ρ), where X is a set (X ∈ Set), ρ ⊂ X × Σ ∗ is a binary relation such that X × {ε} ⊂ ρ. A morphism φ : (X, ρ) → (Y, σ) of Rel(Σ) is a map φ : X → Y such that (φx, u) ∈ σ for (x, u) ∈ ρ. Next, let F be a forgetful functor F : PtAut(Σ) Rel(Σ) mapping each protoautomaton X × Σ ∗ 99K X to the pair (X, ρ) with ρ = {(x, u) | xu 6= ∅}. Theorem 3. For each object (X, ρ) ∈ Rel(Σ) there is a protoautomaton that is free on it with respect to the forgetful functor F . Proof. For (X, ρ) ∈ Rel(Σ) construct a protoautomaton M = (ρ × Σ ∗ 99K ρ), defining the action by the rule  (x, uv), if (x, uv) ∈ ρ (x, u)v = ∅, if (x, uv) ∈ / ρ. Then F M = (ρ, ρ̂), where ρ̂ = {((x, u), v) | (x, u)v = (x, uv)} ⊂ ρ × Σ ∗ . Define the morphism α : (X, ρ) → (ρ, ρ̂) by the formula α(x) = (x, ε). Let us show that M is a free protoautomaton on (X, ρ). Let N = (Y × Σ ∗ 99K Y ) be some protoautomaton and F Y = (Y, σ). For the required morphism γ : M → N of (5) we have: γ(x, ε) = F (γ)(x, ε) = F (γ)α(x) = β(x). 588 I. Mikhailova, B. Novikov and G. Zholtkevych Then for any u ∈ Σ ∗ one can obtain γ(x, u) = γ(x, ε)u = β(x)u, i.e. γ is uniquely determined t u 5 Conclusion It seems that the class of protoautomata, which has been introduced in the paper, gives the most abstract models for systems with discrete behaviour. This class of abstract machines includes not only machines reacting on the received data immediately, as automata, but it also includes machines whose reactions depend on the accumulated information. The machines of this class having a greedy behaviour are united into a sub- class whose instances are called preautomata. Machines of the subclass are used for modelling behaviour systems for complex event processing as it was shown earlier [13, 14]. This class of machines, in contrast to the class of automata, is closed under structural decomposition, and hence, is more suitable for specify- ing complex systems. But the condition c) in the definition of a preautomaton (see Definition 2) seems unnatural. This condition also impedes definition of a nondeterministic preautomaton. Therefore, by eliminating the condition c) we provide a possibility to study nondeterministic models. In our opinion, the models derived in this way (pro- toautomata) are interesting objects that can be used for specification and veri- fication of complex systems. References 1. Aho, A.V., Ullman, J.D.: Theory of Parsing, Translation, and Compiling. Prentice- Hall, New York (1972) 2. Arbib, M.A., Manes, E.G.: Machines in a category: an expository introduction. SIAM Rev. 16, 163–192 (1974). 3. Börger, E., Stärk, R.: Abstract State Machines: A Method for High-Level System Design and Analysis. Springer-Verlag, Berlin Heidelberg (2003) 4. Dokuchaev, M., Novikov, B., Zholtkevych, G.: Partial actions and automata. Alg. and Discr. Math. Vol. 11, 2, 51–63 (2011) 5. Eilenberg, S.: Automata, Languages, and Machines, vol. B. Academic Press, New York (1976) 6. Holcombe, W.M.L.: Algebraic Automata Theory. Cambridge Univ. Press (1982) 7. Hollings, C.: Partial actions of monoids. Semigroup Forum. 75, 293–316 (2007) 8. Lallement, G.: Semigroups and combinatorial applications. John Wiley, New York (1979) 9. MacLane, S.: Categories for the Working Mathematician. Springer, Berlin (1971) 10. Megrelishvili, M., Schröder, L.: Globalization of confluent partial actions on topo- logical and metric spaces. Topol. and Appl. 145, 119–145 (2004) 11. Milner, R.: Communicating and Mobile Systems: The Pi Calculus. Cambridge Uni- versity Press, Cambridge (1999) Protoautomata as Models of Systems with Data Accumulation 589 12. Novikov, B., Perepelytsya, I., Zholtkevych, G. Pre-automata as mathematical mod- els of event flows recognisers. In: V. Ermolayev et al. (eds.) Proc. 7-th Int. Conf. ICTERI 2011, 41–50 (2011) 13. Perepelytsya, I., Zholtkevych, G.: On some class of mathematical models for static analysis of critical-mission asynchronous systems. Syst. ozbr. ta viysk. tehn. Vol. 27, 3, 60–63 (2011) 14. Perepelytsya, I., Zholtkevych, G.: Hierarchic Decomposition of Pre-machines as Models of Software System Components. Syst. upravl. navig. i zv’iazku. Vol. 20, 4, 233–238 (2011)