=Paper=
{{Paper
|id=None
|storemode=property
|title=Protoautomata as Models of Systems with Data Accumulation
|pdfUrl=https://ceur-ws.org/Vol-1000/ICTERI-2013-p-582-589-SMSV.pdf
|volume=Vol-1000
|dblpUrl=https://dblp.org/rec/conf/icteri/MikhailovaNZ13
}}
==Protoautomata as Models of Systems with Data Accumulation==
https://ceur-ws.org/Vol-1000/ICTERI-2013-p-582-589-SMSV.pdf
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)