=Paper=
{{Paper
|id=Vol-2604/paper1
|storemode=property
|title=Understanding Safety Constraints Coalgebraically
|pdfUrl=https://ceur-ws.org/Vol-2604/paper1.pdf
|volume=Vol-2604
|authors=Grygoriy Zholtkevych,Maksym Labzhaniia
|dblpUrl=https://dblp.org/rec/conf/colins/ZholtkevychL20
}}
==Understanding Safety Constraints Coalgebraically==
https://ceur-ws.org/Vol-2604/paper1.pdf
Understanding Safety Constraints Coalgebraically
Grygoriy Zholtkevych[0000−0002−7515−2143] and Maksym
Labzhaniia[0000−0002−2666−3959]
Department of Theoretical and Applied Computer Science
School of Mathematics and Computer Science
V.N. Karazin Kharkiv National University
4, Svobody Sqr., Kharkiv, 61022, Ukraine
g.zholtkevych@karazin.ua; m.labzhaniia@gmail.com
Abstract. Safety constraints are crucial to the development of mission-
critical systems. The practice of developing software for systems of this
type requires reliable methods for identifying and analysing project arte-
facts. This paper proposes a coalgebraic approach to understanding be-
havioural constraints for systems of a kind. The advantage of the pro-
posed approach is that it gives a framework for providing abstract se-
mantic models of the domain-specific languages designed for specifying
behavioural constraints.
Keywords: behavioural constraint, safety constraint, coalgebra, final
coalgebra, coalgebraical semantic model, final semantics
Acknowledgement. G. Zholtkevych thanks professors R. de Simone, F. Mallet,
and L. Liquori for detailed discussions of the problems related to this paper
during his internship at Inria Sophia Antipolis - Médi and Campus France for
funding this internship.
1 Introduction
A lot of modern technical systems are compound and smart. Moreover, they are
hybrid in the sense that ones consisted of both physical and cybernetic (soft-
ware) components. In other words, we can state that modern technical systems
of such a kind are cyber-physical systems (see, for example, [11]). This requires
the corresponding approaches to designing these systems. First of all, we need to
remark that software complex of such a system contains necessarily reactive com-
ponents i.e. programs intending rather for providing the required behaviour of
the system than for handling data [12]. This is because of the incorrect behaviour
of a complex technical system can have serious and some times catastrophic con-
sequences for the system surroundings. Thus, we should classify such systems as
safety-critical [4]. As well-known, specification and analysis of the behavioural
requirements is the most critical phase under safety-critical systems development
process [7] taking into account the fact that a most of system faults and errors
are consequences of incorrect specifications or of incomplete analysis. Hence,
Copyright © 2020 for this paper by its authors.
Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
we need a dependable and mathematically grounded toolkit for specifying and
analysing behavioural constraints for designing such systems.
This paper introduces some general framework for constructing rigorous mod-
els of safety constraints, which can be used for constructing domain-specific lan-
guages for specifying safety constraints. This framework can be included as a
component of the mentioned above development toolkit.
In the paper, we use coalgebraic techniques as the main research method-
ology. This choice is motivated by the fact that universal coalgebras give an
adequate mathematical tool for modelling behaviour of systems [13,9].
Sec. 2 introduces the needed notions and notation for sequences of system
notifications.
For completeness and reader convenience, we have collected the used coalge-
braic concepts in Sec. 3.
Sec. 4 is devoted to studying concrete endofunctors and properties of the
coalgebras corresponding to these endofunctors related to safety constraints.
Finally, Sec. 5 is the central section of the paper. It contains definitions of
the target constructions and results providing achieving of the claimed goals.
2 Basic Concepts and Notation
In this section, we assume that X is a finite set with at least two elements.
Elements of this set are usually interpreted as system notifications.
A mapping (generally speaking partial) s : N → X is called an X-sequence
if for any k ∈ N, s k 0 is defined whenever s k is defined and 0 ≤ k 0 < k.
An X-sequence s is called an X-word if there exists k ∈ N such that s k is
undefined; in contrast, an X-sequence s is called a X-stream if s k is defined
for all k ∈ N.
We use the notation X ∗ for referring to the set of all X-words, and X N for
referring to the set of all X-streams. The set X ∗ contains the sequence defined
nowhere, which is below denoted by .
We use also the notation X ∞ for referring to the set X ∗ X N , and X + for
S
referring to the set of all X-words without the word defined nowhere.
For an X-word u, we denote by |u| the minimal natural number such that
u |u| is undefined.
The value |u| where u ∈ X ∗ is called length of u.
As usually, we identify n ∈ X with the X-word u ∈ X ∗ such that u 0 = n
and u k is undefined if k > 0.
For u ∈ X ∗ and s ∈ X ∞ , we denote by us the next X-sequence
uk if k < |u|
us = λ k ∈ N .
s(k − |u|) otherwise
Below we need in the following set
n−1 · A = {u ∈ X ∗ | nu ∈ A} where A ⊂ X ∗ and n ∈ X.
For s ∈ X ∞ and m ∈ N, we denote by sm.. the next X-sequence
s(k + m) if this value is defined
sm.. = λ k ∈ N .
is undefined otherwise
Also for s ∈ X ∞ and m, l ∈ N, we denote by sm..l the next X-word
s(k + m) if this value is defined and k < l − m
sm..l = λ k ∈ N .
is undefined otherwise
The principal concepts for our studying is given by the following definitions
Definition 1. A subset P ⊂ X ∗ is called prefix-free if u ∈ P ensures u0..m ∈
/
P whenever 0 ≤ m < |u|.
Remark 1. If a prefix-free subset of X ∗ contains then this subset is {}. Indeed,
if a prefix-free subset of X ∗ contains both and another X-word u then u0..0 =
cannot belong to this subset. This contradiction grounds the remark.
Definition 2 (see [2]). A safety constraint is a subset S ⊂ X N such that
s ∈ S if for any m ∈ N, s0..m = s00..m for some s0 ∈ S.
3 Coalgebras Preliminaries
In this section, we remind the basic definitions and facts related to the concept of
a coalgebra in an arbitrary category. In addition, we give some specific concepts
in the case when C = Set.
Thus, we assume the category C and the endofunctor F of C are given and
held fixed in this section (general information on category theory can be found
in [10,3]).
Definition 3. A morphism a of C is called an F -coalgebra if the equality
cod a = F (dom a) is fulfilled. In the case, dom a is called the carrier of a and
denoted below by a.
Definition 4. Let a and b be F -coalgebras then a morphism f : a → b is called
an F -morphism from a into b (symbolically, f : a → b) if the diagram
f
a b
a b commutes
Ff
Fa Fb
or, equivalently, the equation (F f ) a = b f holds.
Proposition 1. The class of F -coalgebras equipped with F -morphisms is a cat-
egory denoted usually by CoalgF (C) or CoalgF if the category C is clear from
the context.
Final objects of this category are very important for constructing semantic mod-
els of programming and specification languages.
Definition 5.
(1) A terminal object of CoalgF if it exists is called a final F -coalgebra, which
is denoted by νF .
(2) For any F -coalgebra a, the unique F -morphism from a into νF is called an
anamorphism and denoted by (a) .
The concept of bisimulation is a key concept in the theory of universal coalgebras.
Definition 6 (see P. Aczel and N. Mendler [1]). A bisimulation of F -
ra rb
coalgebras a and b is a span a ←− r −→ b in category CoalgF (C) such that the
r r
span a ←− a b
r −→ b in category C is a mono-span i.e. the validity of ra h0 = ra h00
and rb h = rb h for any object c in C and morphisms h0 , h00 : c → r ensures
0 00
h0 = h00 .
The next proposition demonstrates that coalgebra morphisms give the simplest
examples of bisimulations.
Proposition 2. For any F -coalgebras a and b and F -morphism f : a → b, the
id
a f
span a ←−− a−
→ b is a bisimulation of a and b.
ida f
Proof. We need to note only that the span a ←−− a −
→ b is evidently a mono-
span. t
u
Proposition 3. Assume that category C is finitely complete and there is a final
ra rb
F -coalgebra then for any bisimulation a ←− r −→ b of F -coalgebras a and b,
there exists a unique monomorphism f : r → P such that ra = pa f and rb = pb f
pa pb (a) (b)
where a ←− P −→ b is the pullback of the cospan a −−→ νF ←−− b.
Proof. Indeed, the definition of an anamorphism ensures the commutativity of
the next diagram
rb
r b
ra (b)
(a)
a νF
pa pb (a) (b)
i.e. for the pullback a ←− P −→ b of the cospan a −−→ νF ←−− b, we have the
existence of a unique morphism f : r → P . One can see that this morphism is a
monomorphism taking into account the mono-span and pullback properties. t u
This statement can be inverted for some class of endofunctors.
Proposition 4. If category C is finitely complete, endofunctor F preserves pull-
(a)
backs, and there exists a final F -coalgebra then the pullback of the cospan a −−→
(b)
νF ←−− b is the greatest bisimulation of F -coalgebras a and b.
pa pb
Proof. Indeed, let a ←− P −→ b be the mentioned above pullback then it is
mono-span and the next diagram
F pb
FP Fb
F pa F (b)
F (a)
Fa F νF
is a pullback diagram. Further, note that the outer square of the following dia-
gram commutes.
pb
P b
ρ
b
∃
F pb
pa FP Fb
F pa F (b)
a F (a)
a Fa F νF
Indeed,
F (a) apa = (νF ) (a) pa considering that (a) is an F -morphism
pa pb
= (νF ) (b) pb using the pullback property for a ←− P −→ b
= F (b) bpb considering that (b) is an F -morphism.
Thus, taking into account the pullback property for the inner subdiagram in
the diagram above, one can derive the existence of ρ ensuring the diagram com-
pa pb
mutativity. But it means that the span a ←− P −→ b can be lifted up to the
corresponding span of coalgebras. t
u
Another concept used below is the concept of subcoalgebra.
Definition 7. Let a ∈ CoalgF (C) and j : j → a be a monomorphism in C with
the domain j then an F -coalgebra c is called a subcoalgebra of a if c = j and
j is lifted upto a coalgebraic monomorphism j : c → a.
We complete this section by enumerating a series of facts specific for the
category Set and endofunctors of this category. If C = Set then an F -coalgebra
is called an F -system due to J. Rutten [13] and the corresponding category is
denoted below by Sys(F ) instead of CoalgF (Set).
It is well-known that category Set is finitely complete. The important class
of endofunctors of the category Set is called the class of polynomial endofunctors
and defined as follows (see, for example, [9])
(1) a constant endofunctor i.e. an endofunctor C X = C for some set C and
C f = idC is a polynomial endofunctor;
(2) if F 1 and F 2 are polynomial endofunctors then the endofunctor F X =
F 1 X × F 2 X and F f = F 1 f × F 2 f is a polynomial endofunctor;
(3) if F 1 and F 2 are polynomial endofunctors then the endofunctor F X =
F 1 X + F 2 X and F f = F 1 f + F 2 f is a polynomial endofunctor (here and
below, “+” refers to a disjunctive sum of sets).
An important property of polynomial endofunctor is that such an endofunctor
preserves pullbacks.
4 Systems as Coalgebras
In this section, we introduce and study some endofunctors, systems related to
the endofunctors, and their property. Note that all considered here endofunctors
are polynomial.
4.1 Discrete Dynamical Systems
The simplest manner for modelling a discrete dynamical system is to represent
it by a pair (X, g) where X is a set called the state set and g : X → X is a
mapping called the dynamics.
It is evident that g can be considered as IdSet -coalgebra of the category Set and,
in this context, X denoted by g.
Morphisms of such coalgebras are mappings that intertwine the dynamics of the
corresponding coalgebras. More precise, for IdSet -coalgebras g and h, a morphism
f : g → h is a mapping f : g → h such that f g = hf .
Easy seen that the final coalgebra exists in this case but it is trivial namely
νIdSet = 1 and νIdSet = id1 . Thus, taking into account that category Set and
functor IdSet satisfy conditions of Prop. 4 one can conclude that any two dynam-
ical systems are bisimilar.
A less trivial example is given by the endofunctor T : Set → Set defined as
follows (here and below, 1 refers to an one-element set {⇓} containing a fault
indicator).
T X = 1 + X for any object X of category Set;
T f = id1 +f for any morphism f of category Set.
A system of such a kind is called a system with termination.
The corresponding class of morphisms (see Def. 4) from a T-system g into a
T-system h contains a mapping f : g → h if and only if for any x ∈ g, either
gx = ⇓ and h(f x) = ⇓ or gx 6= ⇓ and f (gx) = h(f x).
There is a final νT in the category Sys(T). This object is structured as follows
S
νT = 1 + N where 1 + N = N {∞}
⇓ if x = 0
νT = λ x ∈ 1 + N . ∞ if x = ∞
x − 1 otherwise
For a T-system g, the corresponding anamorphism (g) is defined as follows
if g (k) x 6= ⇓ for all k ∈ N+
∞
(g) = λ x ∈ g . (k+1)
min{k ∈ N | g x = ⇓} otherwise
where
g (1) = g
if g (k) x = ⇓
(k+1) ⇓
g =λx∈g. (k) for k ∈ N+ .
g(g x) otherwise
Note 1. Everybody familiar with the concept of a monad can easily see that g (k)
is the k th -power of g in the corresponding Kleisli category.
4.2 Systems with Output
In this subsection, we consider the class of dynamical systems equipped with a
mechanism for the external monitoring of the current system state. We use the
term a system with output for referring to a system of this class. Following
the coalgebraic approach, we model systems of this class as coalgebras, which
signature is defined by the corresponding endofunctor SN : Set → Set that is
defined as follows
SN X = N × X for any object X of category Set;
SN f = idN ×f for any objects X and Y of category Set and a morphism
f :X →Y.
In this definition, N refers to a finite set of possible output values.
Thus, a system with output is a mapping σ : σ → SN σ where σ is a set
called usually the system state set. Taking into account the universality of the
product (see, [10, Sec. III.4] or [3, Sec. 2.4]), one can see that an SN -system σ
is uniquely represented as σ = hσout , σtr ii where σout = prN σ : σ → N and
σtr = prσ σ : σ → σ called respectively the output and transition functions
of the system.
The general coalgebraic framework (see Def. 4) gives the following concept
of an SN -morphism: for SN -system σ and τ , a mapping f : σ → τ is called an
SN -morphism if (τout )f = σout and (τtr )f = f (σtr ).
There is a final object νSN in the category Sys(SN ). This object is structured
as follows
νSN = NN ;
(νSN )out = λ s ∈ NN . s 0;
(νSN )tr = λ s ∈ NN . λ k ∈ N . s(k + 1).
For an N-system σ, the corresponding anamorphism (σ) is defined by the next
formula
k
(σ) = λ x ∈ σ . λ k ∈ N . σout (σtr x).
Thus, the proposed model allows considering a point of the final N-system
carrier as an observed behaviour of the system being studied. It means that we
are interested in specifying and analysing constraints that allow distinguishing
an admissible and inadmissible system behaviour.
4.3 Detectors of Behavioural Violations
The remaining part of the paper is devoted to demonstrating that the safeness
of a subset can be described with using the category-theoretic language.
In this subsection, we introduce some class of systems that used as a tool
for distinguishing admissible and inadmissible system behaviours. We refer to
systems of this class as detectors of behavioural violations.
This class is determined with the endofunctor DN : Set → Set defined as
follows
DN X = (1 + X)N for any object X of categorySet;
DN f = λ φ ∈ (1 + X)N . λ n ∈ N . (id1 +f )(φ n)
for any objects X and Y of category Set and a morphism f : X → Y .
We call below a DN -system a detector and for a detector a, we refer to a as
to the detector state set.
A detector morphism f from a detector a into a detector b is (compare with
Def. 4) a mapping f : a → b such that for any x ∈ a and n ∈ N,
(1) (ax) n = ⇓ if and only if (b(f x)) n = ⇓;
(2) if (ax) n 6= ⇓ then b(f x) n = f (ax) n .
Proposition 5. The class Sys(DN ) of N-detectors equipped with detector mor-
phisms forms a category.
Proof is a simple check of the categories axioms. t
u
The following theorem describes a final detector.
Theorem 1. There is a final object in category Sys(DN ) that is structured as
follows
νDN is the set of all prefix-free subsets of N+ ;
⇓ if n ∈ P
νDN = λ P ∈ νDN . λ n ∈ N . .
n−1 · P otherwise
For an a N-detector, the corresponding anamorphism (a) is defined by the next
formula
(a) = λ x ∈ a . {u ∈ N+ |a+ (x, u) = ⇓ and
a+ (x, u0..k ) 6= ⇓ whenever 0 < k < |u|}
where a+ : a × N+ → 1 + a defined as follows
a+ (x, n) = (ax) n x ∈ a, n ∈ N;
⇓ if a+ (x, u) = ⇓
+
a (x, un) = + x ∈ a, n ∈ N, u ∈ N+ .
aa (x, u) n otherwise
The theorem can be derived from [8, Lemma 6] but we give a direct proof, which
details are used below. The proof is preceded by a statement of the facts being
used.
Lemma 1. For any N-detector a, x ∈ a, and u, v ∈ N+ , the equation
+
⇓ if a (x, u) = ⇓
a+ (x, uv) = + + (1)
a a (x, u), v otherwise
holds.
Proof. If a+ (x, u) = ⇓ then a+ (x, uv) = ⇓ by definition of a+ . Hence we below
assume a+ (x, u) 6= ⇓.
Let us use induction on v.
For v = n ∈ N, (1) follows from the definition of a+ .
Assume that v = v 0 n, n ∈ N, and (1) holds for v 0 .
Then under assumption that a+ (x, uv 0 ) = ⇓, we have
a+ (x, u(v 0 n)) = a+ (x, (uv 0 )n) = ⇓
by definition of a+ . Hence, a+ (x, uv) = ⇓.
In the other side, we have a+ (a+ (x, u), v 0 ) = a+ (x, uv 0 ) = ⇓ by induction hy-
pothesis. But then a+ (a+ (x, u), v) = a+ (a+ (x, u), v 0 n) = ⇓ by definition of a+ .
Hence, we have a+ (x, uv) = a+ (a+ (x, u), v).
In contrary, assumption that a+ (x, uv 0 ) 6= ⇓ gives
a+ (x, uv) = a+ (x, u(v 0 n)) = a+ (x, (uv 0 )n)
= a a+ (x, uv 0 ) n by definition of a+
= a a+ (a+ (x, u), v 0 ) n
by induction hypothesis
+ + 0 + +
= a (a (x, u), v n) = a (a (x, u), v) by definition of a+ .
Thus, the lemma is proved. t
u
Lemma 2. If P ⊂ N+ is prefix-free then n−1 · P ⊂ N+ and it is prefix-free
whenever n ∈ N and n ∈
/ P.
Proof. Firstly, n ∈ / n−1 ·P i.e. n−1 ·P ⊂ N+ . Further, if u ∈ n−1 ·P
/ P ensures ∈
−1
and u0..m ∈ n · P for 0 ≤ m < |u| then nu ∈ P and nu0..m ∈ P . Taking into
account nu0..m = (nu)0..m+1 , one can obtain a contradiction, which completes
the proof. t
u
Lemma 3. Any prefix-free subset P of N+ can be represented as the following
disjunctive union
X
P = NP + n · Pn where
n∈N\NP (2)
−1
NP = {n ∈ N | n ∈ P } and Pn = n · P.
Proof. Assume u ∈ P then either u = n for some n ∈ N or |u| > 1. In the
first case, we have u ∈ NP and, therefore, u belongs to the right side of (2). In
another case, u = (u 0)u1.. where (u 0) ∈ / NP and |u1.. | > 0 i.e. u1.. ∈ (u 0)−1 ·P
and u belongs to the right side of (2).
Now P assume u belongs to the right side of (2) then either u ∈ NP or u ∈
n · Pn . In the first case, we have u = n ∈ NP i.e. u ∈ P by definition
n∈N\NP
of NP . In another case, u ∈ n · Pn where n ∈ N \ NP . Hence, u = nu1.. and
u1.. ∈ n−1 · P . The last means that u ∈ P . t
u
Now all is ready for proving Theorem 1.
Proof (Proof of Theorem 1). Firstly, νDN : νDN → DN νDN due to Lemma 2.
Hence, νDN is an N-detector.
Further, let us show that the mapping (a) : a → νDN defined above for any
N-detector a is an N-detector morphism.
If (ax) n = ⇓ then n ∈ (a) x i.e. νDN ((a) x) n = ⇓.
Conversely, if νDN ((a) x) n = ⇓ then n ∈ (a) x i.e. (ax) n = ⇓.
If (ax) n 6= ⇓ then either (a) x = ∅ or this equation is wrong.
In the first case, a+ (x, u) 6= ⇓ for any u ∈ N+ and, therefore, (a) (ax) n = ∅
too. Also, we have
νDN ( (a) x) n = (νDN ∅)n = n−1 · ∅ = ∅ = (a) (ax) n .
In another case, we have both (ax) n 6= ⇓ and (a) x 6= ∅.
If u ∈ νDN ( (a) x) n = n−1 · ( (a) x) then nu ∈ (a) x i.e. a+ (x, nu) = ⇓ but
a+ (x, nu0..m ) 6= ⇓ whenever m < |u|. Hence, for any m ≤ |u| and v = u0..m , we
have
a+ (x, nv) = a+ (a+ (x, n), v) = a+ ((ax) n, v) (3)
due to Lemma 1 and by definition of a+ . Hence, one can conclude that
u ∈ (a) (ax) n .
Conversely, if u ∈ (a) (ax) n then (3) guarantees a+ (x, nu) = ⇓ but
a+ (x, nu0..m ) 6= ⇓ whenever m < |u|. It means that u ∈ n−1 · ( (a) x) =
νDN ( (a) x) n.
Thus, we have checked the N-detector morphism properties for (a).
For completing the proof, we need to show that (a) is the only N-detector mor-
phism from a into νDN i.e. f = (a) for any f : a → νDN .
Assume f x = ∅ then we have the next chain of equivalent statements
fx = ∅
n−1 · (f x) = ∅ for all n ∈ N
νDN (f x) n = ∅ for all n ∈ N by definition of νDN
(ax) n 6= ⇓ and f (ax) n = ∅ for any n ∈ N due to the N-morphism
properties
+ +
a (x, u) 6= ⇓ for all u ∈ N by induction on u
(a) x = ∅ by definition of (a).
Hence, f x = ∅ iff (a) x = ∅.
Now using induction on |u|, prove that u ∈ f x if and only if u ∈ (a) x.
If |u| = 1 then we have the next chain of equivalent statements.
n ∈ f x for some n ∈ N
νDN (f x) n = ⇓ by definition of νDN
(ax) n = ⇓ due to the N-morphism properties
n ∈ (a) x by definition of (a).
Hence, u ∈ f x iff u ∈ (a) x for any u ∈ N+ such that |u| = 1.
If |u| = m > 1 and the required statement is true for v ∈ N+ such that |v| < m
then we have the next chain of equivalent statements.
u ∈ fx
u1.. ∈ (u 0)−1 · (f x)
u1.. ∈ νDN (f x) (u 0) by definition of νDN
and due to Lemma 3
u1.. ∈ f (ax) (u 0) due to the N-morphism
properties
u1.. ∈ (a) (ax)(u 0) by induction hypothesis
a+ (ax)(u 0), u1.. = ⇓ but
a+ (ax)(u 0), u1..k 6= ⇓ whenever k < m
by definition of (a)
a+ x, (u 0)u1.. = ⇓ but
a+ x, (u 0)u1..k 6= ⇓ whenever k < m
due to Lemma 1
u ∈ (a) x by definition of (a).
Thus, f = (a) . t
u
Below we need a characterisation of the subsets of νDN that are carriers of
subcoalgebras. The next proposition gives this characterisation.
Proposition 6. A subset C ⊂ νDN is the carrier of a subcoalgebras of the final
detector defined by the natural embedding jC : C → νDN if and only if the
condition
for any P ∈ C and n ∈ N, either n∈P or n−1 · P ∈ C
is fulfilled.
Proof boils down to simply checking the requirements of definitions. t
u
5 Coalgebraic Understanding Safety Constraints
The general coalgebraic framework for recognising violations of the behaviour of
a system with output is introduced and studied in this section.
5.1 Functor Join and Its Properties
This subsection defines bifunctor Join (see Theorem 2), which is the key tool for
our studying. The importance of this bifunctor is related to the fact it preserves
bisimulations (see Theorem 3).
Firstly assuming σ and a is a system with output N and an N-detector
respectively, one can define the system with termination Join(σ, a) : σ × a →
T(σ × a) as follows
⇓ if (ay)(σout x) = ⇓
Join(σ, a) = λ (x, y) ∈ σ × a . (4a)
σtr x, (ay)(σout x) otherwise
Further for systems σ and τ with output N and N-detectors a and b, an SN -
morphism f : σ → τ , and a detector morphism g : a → b, we define the mapping
Join(f, g) : σ × a → τ × b by the formula
Join(f, g) = f × g. (4b)
Theorem 2. Rules (4) determine a bifunctor Join : Sys(SN ) × Sys(DN ) →
Sys(T).
Proof. Firstly, let us check that for any f : σ → τ and g : a → b where σ, τ ∈
Sys(SN ) and a, b ∈ Sys(DN ), Join(f, g) is a T-morphism from Join(σ, a) into
Join(τ, b).
Indeed, let Join(σ, a) (x, y) = ⇓ where x ∈ σ, y ∈ a then we have the next
chain of equivalent statements
Join(σ, a) hx, yi = ⇓
(ay)(σout x) = ⇓ by definition of Join(σ, a)
(ay)(τout (f x)) = ⇓ due to f is an SN -morphism
b(gy) τout (f x) = ⇓ due to g is a DN -morphism
Join(τ, b) hf x, gyi = ⇓ by definition of Join(τ, b)
Join(τ, b) Join(f, g)hx, yi = ⇓ by definition of Join(f, g)
Now assume that Join(σ, a) hx, yi = 6 ⇓ (it means (ay)(σout x) 6= ⇓) where x ∈ σ,
y ∈ a then
Join(f, g) Join(σ, a) hx, yi = Join(f, g) σtr x, (ay)(σout x)
= f (σtr x), g (ay)(σout x)
by definitions of Join(σ, a) and Join(f, g).
Further,
Join(f, g) Join(σ, a) hx, yi = τtr (f x), g (ay) τout (f x)
= τtr (f x), b(gy) τout (f x)
taking into account that f is an SN -morphism, and g is a DN -morphism.
Finally,
Join(f, g) Join(σ, a) hx, yi = Join(τ, b) f x, gy
= Join(τ, b) Join(f, g)hx, yi
by definitions of Join(τ, b) and Join(f, g) respectivelly.
Thus, Join(f, g) is a T-morphism (see Subsec. 4.1).
Taking into account rule (4b) one can conclude that Join is a bifunctor. t
u
pσ pτ
Theorem 3. Let σ ←− ρ −→ τ be a bisimulation of systems σ and τ with output
qa qb
N and a ←− r −→ b be a bisimulation of N-detectors a and b then Join(ρ, r) is
a bisimulation of Join(σ, a) and Join(τ, b).
Proof. Let us consider the span
Join(pσ ,qa ) Join(pτ ,qb )
Join(σ, a) ←−−−−−−− Join(ρ, r) −−−−−−−→ Join(τ, b).
pσ ×qa pτ ×qb
It is sufficient to show that the corresponding span σ×a ←−−−− ρ×r −−−−→ τ ×b
in Set is a mono-span.
Assume some mappings g, h : S → ρ × r with common domain S satisfy the
equations (pσ × qa )g = (pσ × qa )h and (pτ × qb )g = (pτ × qb )h. These mappings
can be uniquely represented as follows g = hgρ , gr i and h = hhρ , hr i respectively
where gρ , hρ : S → ρ and gr , hr : S → r.
Taking into account that
(pσ × qa )g = (pσ × qa )hgρ , gr i = hpσ gρ , qa gr i and
(pσ × qa )h = (pσ × qa )hhρ , hr i = hpσ hρ , qa hr i
we have hpσ gρ , qa gr i = hpσ hρ , qa hr i i.e. pσ gρ = pσ hρ and qa gr = qa hr due to
properties of product. Similarly, we have pτ gρ = pτ hρ and qb gr = qb hr from
condition (pτ × qb )g = (pτ × qb )h.
Then one can derive gρ = hρ using the conditions pσ gρ = pσ hρ and pτ gρ = pτ hρ
pσ pτ
and the bisimulation σ ←− ρ −→ τ .
Similarly, we have gr = hr due to the conditions qa gr = qa hr and qb gr = qb hr
qa qb
and the bisimulation a ←− r −→ b.
pσ ×qa pτ ×qb
Thus, g = h and, therefore, the considering span σ × a ←−−−− ρ × r −−−−→ τ × b
is realy a mono-span. t
u
5.2 Safety Constraints and Detectors
This subsection is central to the paper. Here we establish an association between
N-detectors and some subsets of NN . Further, we prove this class of subsets is
exactly the class of safety constraints.
First of all for s ∈ NN , let us define the following system [s] with output
namely
[s] = sk.. | k ∈ N and [s] = λ t ∈ [s] . t 0, t1.. .
Further for any N-detector a and x ∈ a, let us define the following set
JaKx = {s ∈ NN | (Join([s], a))hs, xi = ∞}.
The next simple fact is useful below.
Lemma 4. For s ∈ NN , an N-detector a, and x ∈ a,
if a+ (x, s0..m ) = ⇓
(m) ⇓
Join([s], a) hs, xi = + for m > 0.
hsm.. , a (x, s0..m )i otherwise
Proof. For proving we apply induction on m. If m = 1 then the equation holds
due to (4a).
Now assume the equation holds for some m > 1.
(m)
Let Join([s], a) hs, xi = ⇓ then a+ (x, s0..m ) = ⇓ by induction hypothesis.
(m+1)
The definition of a+ ensures a+ (x, s0..m+1 ) = ⇓. But Join([s], a) hs, xi =
⇓ by definition. Hence, the equation holds in this case.
(m)
Finally, assume Join([s], a) hs, xi =
6 ⇓ then
(m)
Join([s], a) hs, xi = hsm.. , a+ (x, s0..m )i
by induction hypothesis i.e. a+ (x, s0..m ) 6= ⇓. Thus,
(m+1) (m)
Join([s], a) hs, xi = Join([s], a) Join([s], a) hs, xi
= Join([s], a) hsm.. , a+ (x, s0..m )i.
(m+1)
Now applying (4a), we obtain the required expression for Join([s], a) hs, xi.
t
u
Lemma 5. For any N-detector a and x ∈ a, the set JaKx is a safety constraint.
Proof. Indeed, let us assume the existence of s ∈ / JaKx such that the equation
s00..m = s0..m holds for any m ∈ N and for some s0 ∈ JaKx depending in generally
on m.
The fact s ∈ / JaKx ensures (Join([s], a))hs, xi = K for some K ∈ N. It means (see
Lemma 4) a+ x, s0..K+1 = ⇓. Let s0 ∈ JaKx such that s0 = s0..K+1 then
0..K+1
a+ x, s00..K+1 = ⇓ and, therefore, (Join([s0 ], a))hs0 , xi = K. But (Join([s0 ], a))hs0 , xi =
∞ by the assumption s0 ∈ JaKx . This contradiction completes the proof. t
u
The following lemma is less simple.
Lemma 6. For any safety constraint S ⊂ NN , there exist an N-detector aS and
x ∈ aS such that JaS Kx = S.
Proof. Let us define the N-detector aS as follows (note that ∈ aS )
[
aS = {} u ∈ N+ | u = s0..|u| for some s ∈ S
⇓ if un ∈/ aS
aS = λ u ∈ aS . λ n ∈ N .
un otherwise
and prove that JaS K = S.
Let us assume s ∈ S then s0..m ∈ aS for any m ∈ N. Hence, a+ S (s0..m , s m) =
s0..m+1 ∈ aS for each m i.e. (Join([s], aS ))hs, i = ∞. Thus, s ∈ JaS K .
Conversely assume s ∈ JaS K then (Join([s], aS ))hs, i = ∞ and, therefore,
(m)
Join([s], aS ) hs, i =
6 ⇓ for each m > 0. Lemma 4 ensures
s0..m = a+
S (, s0..m ) ∈ aS for all m > 0
(m)
that guarantees existence s(m) ∈ S such that s0..m = s0..m . Now using the
safeness of S, one can conclude s ∈ S. t
u
Theorem 4 (about universal detector). A subset S ⊂ NN is a safety con-
straint if and only if there exist P ∈ νDN such that S = JνDN KP .
Proof. Lemmas 5 and 6 ensure that a subset S ⊂ NN is a safety constraint if
and only if there exist an N-detector a and x ∈ a such that S = JaKx . Let us
take P = (a) x and prove (Join([s], a))hs, xi = (Join([s], νDN ))hs, P i.
Indeed, for the T-morphism Join id[s] , (a) : Join([s], a) → Join([s], νDN ), we
have
Join id[s] , (a) hs, xi = id[s] × (a) hs, xi = hs, P i. (5)
Using the equation
(Join([s], a)) = (Join([s], νDN )) ◦ Join id[s] , (a)
that follows from the definition of an anamorphism, one can derive from (5) the
follows
(Join([s], a))hs, xi = (Join([s], νDN ))hs, P i.
Considering the last equation holds whenever P = (a) x, one can conclude that
S = JaKx = JνDN KP . t
u
Corollary 1. A subset S ⊂ NN is a safety constraint if and only if it is equal
/ P for any m > 0} for some prefix-free subset of N+ .
to {s ∈ NN | s0..m ∈
Proof. It follows immediately from Theorem 4. t
u
Corollary 2. For any N-detectors a and b and x ∈ a and y ∈ b, the equation
(a) x = (b) y is sufficient for JaKx = JbKy .
Proof. The statement is true due to the construction method of P used in the
proof of Theorem 4. t
u
5.3 Families of safety Constraints
Theorem 4 proved in the previous subsection establishes that for the family of
all safety constraints, there is a universal detector, i.e. a detector that recognises
any safety constraint of the family when the detector configured appropriately.
Such a general result, however, cannot be used in the practice of developing
software tools, if only because computability considerations limit our expressive
capabilities for specifying safety constraints and, in particular, guarantee the
impossibility of specifying an arbitrary prefix-free set. Therefore, we need to
consider more specific families of safety constraints. In this subsection, we try to
outline some general approach to solving this problem.
We begin with the next definition.
Definition 8. A family of safety constraints F is below called a family with
a universal detector if F = {JaKx | x ∈ a} for some N-detector a being called
in this case a universal detector for F.
Theorem 5. A family of safety constraints F is a family with a universal de-
tector if and only if there exists C ⊂ νDN that meets the following conditions
for any P ∈ C,
(6a)
either n ∈ P or n−1 · P ∈ C for an arbitrary n ∈ N
for any safety constraint S,
S ∈ F if and only if there exists P ∈ C such that S = JνDN KP (6b)
Proof. Firstly, let us assume the family F is a family with a universal detector
then Prop. 6 guarantees the validity of conditions (6).
Conversely, let us define the next mapping a : C → DN C
⇓ if n ∈ P
a=λ P ∈C.λ n∈N.
n−1 · P otherwise
The correctness of this definition is ensured by (6a), hence a is an N-detector
and, due to (6b), it is a universal detector. t
u
Corollary 3. A family of safety constraints F is a family with a universal de-
tector if and only if
{P ∈ νDN | JνDN KP ∈ F}
is the carrier of a subcoalgebra of νDN .
Now we consider three specific safety constraint family and demonstrate that
each of them is a family with a universal detector.
Regular Safety Constraints Here we consider the safety constraint family R
formed as follows a safety constraint S belongs to R if and only if there exists
a detector a with the finite carrier such that S = JaKx for some x ∈ a. We call a
safety constraint belonging this family a regular safety constraint.
Theorem 6. The family of regular safety constraints is a family with a universal
detector.
Proof. Let us consider
C = {P ⊂ N+ | P = (a) x for some detector a with finite carrier and x ∈ a}
then any P ∈ C is a regular prefix-free subset of N+ (see, for example,
[6, Theorem 1]).
Now let us check that C satisfies conditions (6). Indeed, Lemma 2 ensures n−1 ·P
is prefix-free for any n ∈ N such that n ∈ / P.
Hence, we need only due to Theorem 5 to check that n−1 · P is a regular set
under assumption n ∈ / P . To do this we consider a finite Eilenberg machine
hQ, T ⊂ Q × N × Q, I ⊂ Q, F ⊂ Qi
that accepts only words from P (see [5]) and construct the new finite Eilenberg
machine
hQ, T ⊂ Q × N × Q, I 0 ⊂ Q, F ⊂ Qi
where I 0 = {q ∈ Q | hq 0 , n, qi ∈ T for some q 0 ∈ I}. It is evident that the
constructed machine accepts exactly n−1 · P and, therefore, n−1 · P ∈ C. t
u
Decidable Safety Constraints Here we consider the safety constraint family
D formed as follows a safety constraint S belongs to D if and only if there exists
P ∈ νDN such that P is decidable and S = JνDN KP . We call a safety constraint
belonging this family a decidable safety constraint.
Theorem 7. The family of decidable safety constraints is a family with a uni-
versal detector.
Proof. To prove the theorem is sufficient to check that the family of a decidable
prefix-free subset of N+ satisfies condition (6a). But this is really true because
one can check the statement u ∈ n−1 · P for a decidable prefix-free subset P
of N+ , any u ∈ N+ , and n ∈ N such that n ∈ / P , by checking nu ∈ P with a
decision procedure for P . t
u
Recursively Enumerable Safety Constraints Here we consider the safety
constraint family RE formed as follows a safety constraint S belongs to RE if
and only if there exists P ∈ νDN such that P is recursively enumerable and
S = JνDN KP . We call a safety constraint belonging this family a recursively
enumerable safety constraint.
Theorem 8. The family of recursively enumerable safety constraints is a family
with a universal detector.
Proof. Similarly to proof of the previous theorem, we need to furnish a semi-
decision procedure for checking the statement u ∈ n−1 · P with a recursively
enumerable prefix-free subset P of N+ , any u ∈ N+ , and n ∈ N such that
n∈ / P . This procedure is as follows
(1) run parallelly checkings nu0..k ∈ P for k = 1, . . . , |u|;
(2) wait for any of these runs to halt;
(3) report success if the halting run is the run for checking nu ∈ P .
An event waited in item (2) may do not happen if nu ∈ / n−1 · P .
/ P i.e. u ∈
If the wait in paragraph (2) is completed then only for one 0 < k ≤ |u| the
corresponding checking is completed due to P is prefix-free.
u ∈ n−1 · P or equivalently nu ∈ P if and only if the checking with number
|u| − 1 is halted.
In other cases, nu ∈/ P i.e. u ∈/ n−1 · P .
Thus, the furnished procedure is really a semi-decision procedure for the state-
ment u ∈ n−1 · P . t
u
6 Conclusion
Summing up the mentioned above we can conclude that subdetectors of a final
detector correspond to families of safety constraints with universal detectors.
These families are candidates for semantic models of domain-specific languages
for specification of safety constraints.
Of course, the obtained results tell nothing how to construct such languages.
But they turn this problem into more precisely defined.
We can identify as problems for further studying the follows
(1) Give syntactic characterisation of regular safety constraints family.
(2) Understand what classes of grammars (for example, context-free) define
proper families of safety constraints.
(3) Can we use complexity classes for defining families of safety constraints with
universal detectors?
(4) Understand how compositional theory of detectors can be developed.
An especial area of further research is the dissemination of the proposed
approach for the specification and analysis of causality constraints, formulated
in terms of the logical clock model. Now authors are working on the paper
“Understanding Logical Clock Model Coalgebraically”.
References
1. Aczel, P., Mendler, N.: A final coalgebra theorem. In: Proc. CTCS’89, Lecture
Notes in Comput. Sci., vol. 389, pp. 357–365. Springer (1989)
2. Alpern, B., Schneider, F.: Recognizing safety and liveness. Distributed Computing
2, 117–126 (1987)
3. Awodey, S.: Category Theory. Oxford University Press, 2nd edn. (2010)
4. Bowen, J., Stavridou, V.: Safety-critical systems, formal methods and standards.
Software Engineering Journal 8(4), 189–209 (1993)
5. Eilenberg, S.: Automata, Languages and Machines, vol. A. Academic Press (1974)
6. G. Zholtkevych and N. Polyakovska: Machine Learning Technique for Regular
Pattern Detector Synthesis: toward Mathematical Rationale. In: Computational
Linguistics and Intelligent Systems, CEUR Workshop Proceedings, vol. 2362, pp.
254–265. CEUR-WS (2019)
7. Grant, E.S.: Requirements engineering for safety critical systems: An approach for
avionic systems. In: 2nd IEEE International Conference on Computer and Com-
munications (ICCC). pp. 991–995. IEEE (2016)
8. Jacobs, B.: Objects And Classes, Co-Algebraically. In: Freitag, B., et al. (eds.)
Object Orientation with Parallelism and Persistence, The Springer International
Series in Engineering and Computer Science, vol. 370, pp. 83–103. Springer, Boston,
MA (1996)
9. Jacobs, B.: Introduction to Coalgebra: Towards Mathematics of States and Obser-
vation. Cambridge Tracts in Theoretical Computer Science, Cambridge University
Press (2017)
10. Lane, S.M.: Categories for the Working Mathematician. Springer, 2nd edn. (2010)
11. Lee, E.A.: Cyber Physical Systems: Design Challenges. Tech. Rep. UCB/EECS-
2008-8, EECS Department, University of California, Berkeley (Jan 2008), http:
//www2.eecs.berkeley.edu/Pubs/TechRpts/2008/EECS-2008-8.html
12. Mana, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems:
Specifications. Springer–Verlag (1992)
13. Rutten, J.: Universal coalgebra: a theory of systems. Theor. Comput. Sci. 249,
3–80 (2000)