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.
Theory of abstract state machines or abstract automata is widely applied in
di erent areas of Computer Science. While the early applications of automata
theory were connected with theory of compilators design (see, for example, [
But the practice of modelling system behaviour based on the automata approach 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 [
In this paper, we consider a more general class of automaton-liked systems |
the class of protoautomata. All necessary information from the theory of
semigroups, automata theory, and category theory can be found in the monographs
[
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 de ned for a 2 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
We will use the de nition of the automaton in the following form (the condition of the niteness is ignored): De nition 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 2 X and u; v 2
x" = x; x(uv) = (xu)v: (1) (2)
More general concept is the following
De nition 2 (see [
b) if xu 6= ? and (xu)v 6= ?, then x(uv) 6= ? and equality (2) is ful lled; c) if xu 6= ? and x(uv) 6= ?, then (xu)v 6= ? and equality (2) is ful lled.
The preautomata over the monoid phisms are such maps ' : X ! Y that form a category PAut( ); its mor(8 a 2 )(8 x 2 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: De nition 3. A globalization of the preautomaton X is an automaton Z with an injection : X ! Z such that for all a 2 , x 2 X
xa 6= ? =) (x)a 2 (X) =) ? 6= (x)a = (xa); xa 6= ? & (xa) = (x)a: Obviously, is a morphism of PAut(M ). We also call it a globalization. De nition 4. A globalization : X ! Z is called universal if for any globalization 0 : X ! Z0 there is an unique morphism { : Z ! Z0 such that 0 = { . The following construction gives an universal globalization (obviously unique up to isomorphism) for any preautomaton X 99K X. De ne a relation ` on the set X : (x; ab) ` (xa; b) () xa 6= ?: Let ' be an equivalence relation generated by `, and XU = (X )= '. An equivalence class of ' containing a pair (x; a) is denoted by [x; a]. For [x; a] 2 XU and b 2 , we set [x; a]b = [x; ab]. Thus a complete action on XU is de ned. Theorem 1. The automaton XU with a morphism U : X ! XU : x 7! [x; "] is the universal globalization of the preautomaton X.
Proof. See [4, Theorem 2] 3
(4) tu The main object of this paper is a generalization of the notion of preautomaton: De nition 5. A protoautomaton is a partial mapping X (x; a) 7! xa such that 99K X :
b) if xu 6= ? and (xu)v 6= ?, then x(uv) 6= ? and equality (2) is ful lled. We will also denote the protoautomaton from this de nition simply by X, if it does not cause a confusion.
Example 1. Let S be a free subsemigroup of and : X S ! X an automaton. De ne a partial mapping X 99K X as an extension of , putting xu = ? for u 2 n S; so we get a protoautomaton over . Note that in general it is not a preautomaton. In addition, this example shows that the automaton over an in nite alphabet can be represented as a protoautomaton over a two-letter alphabet.
Example 2. Let X = fx; yg be a two-element set, L a subset of protoautomaton X 99K X putting for a 6= " . De ne a xa = y; if a 2 L; ?; if a 2= L; and ya = ?. This example shows that protoautomata recognize all languages.
We denote the category of protoautomata with morphisms de ned 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 XU as in Sec. 2, but in this case the morphism U is not injective in general.
In this situation, the concept of a re ector is useful. We recall its de nition
[
C D(!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 ':
(x; a) ] (y; b) () (9 a0; b0; p 2
)(a = a0p & b = b0p & xa0 = yb0 6= ?): Let be the equivalence relation generated by ]. Then coincides with '.
Proof. If (x; a) ] (y; b) then
(x; a) = (x; a0p) ` (xa0; p) = (yb0; p) a (y; b0p) = (y; b); whence '.
Conversely, if (x; a) ` (y; b), then a = cb; y = xc for some c 2 ` ]. Consequently, ' . Hence tu Remark 1. Obviously, ` is re exive and transitive, while ] is re exive and symmetric.
Lemma 2. Let X be a protoautomaton, Y be a preautomaton (both over ), : X ! Y be a morphism, x; y 2 X, a 2 . 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 2 X, b1; : : : ; bn 2 .
Proof has completed 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 2 X, a; b 2 . Then [x; a] = [y; b] implies (x)a = (y)b.
Apply induction on n. Since x = z1b1 6= ? then (x) = that (x) = (zn)bn 6= ?. By de nition of the relation ] (z1)b1. Suppose bn = cp; a = dp; znc = yd 6= ? for some c; d; p 2 . Then (zn)c 6= ? and by the induction Since Y is a preautomaton then (zn)(cp) 6= ?. (x) = (zn)(cp) = (znc)p = (yd)p = ( (y)d)p = (y)a: tu tu
1. [X; "] is a re ector for X in the category PAut( ),
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 2 X we have (x) = U (x) = ([x; "]).
It follows from Lemma 2 that is well-de ned.
2) Similarly, using Lemma 3.
3) Follows from 1), 2), and the following well-known fact [
Example 3. Let X = fx; y; z; tg, p; u; v 2 n f"g. We set zu = zv = t; z(up) = x; z(vp) = y and sw = ? for all s 2 X; w 2 n f"; p; u; vg. In such a manner X turns into a protoautomaton. Since (x; ") ] (z; up) ] (z; vp) ] (y; ") then [x; "] = [y; "] and the re ection morphism of X is non-injective.
A large class of protoautomata is contained in the following example. 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 2 X, u 2 , 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
It is well known [
Recall the necessary de nitions: De nition 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 2 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 2 Set), X is a binary relation such that X f"g . A morphism : (X; ) ! (Y; ) of Rel( ) is a map : X ! Y such that ( x; u) 2 for (x; u) 2 .
Next, let F be a forgetful functor F : PtAut( ) protoautomaton X 99K X to the pair (X; ) with Rel( ) mapping each = f(x; u) j xu 6= ?g.
Theorem 3. For each object (X; ) 2 Rel( ) there is a protoautomaton that is free on it with respect to the forgetful functor F .
Proof. For (X; ) 2 Rel( ) construct a protoautomaton M = ( de ning the action by the rule 99K ), (x; u)v = (x; uv); if (x; uv) 2
?; if (x; uv) 2= : Then F M = ( ; ^), where ^ = f((x; u); v) j (x; u)v = (x; uv)g . De ne 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): Then for any u 2 one can obtain
(x; u) = (x; ")u = (x)u; i.e. 5 is uniquely determined
tu 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
subclass whose instances are called preautomata. Machines of the subclass are used
for modelling behaviour systems for complex event processing as it was shown
earlier [
Therefore, by eliminating the condition c) we provide a possibility to study nondeterministic models. In our opinion, the models derived in this way (protoautomata) are interesting objects that can be used for speci cation and verication of complex systems.