Safety constraints are crucial to the development of missioncritical systems. The practice of developing software for systems of this type requires reliable methods for identifying and analysing project artefacts. This paper proposes a coalgebraic approach to understanding behavioural constraints for systems of a kind. The advantage of the proposed approach is that it gives a framework for providing abstract semantic models of the domain-specific languages designed for specifying behavioural constraints.
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 (software) 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 components 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 consequences 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, 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 models of safety constraints, which can be used for constructing domain-specific languages 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 methodology. 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 coalgebraic 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
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 2 N, s k0 is defined whenever s k is defined and 0 k0 < k.
An X-sequence s is called an X-word if there exists k 2 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 2 N.
We use the notation X for referring to the set of all X-words, and XN 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 X1 for referring to the set X S XN, and X+ for referring to the set of all X-words without the word defined nowhere.
For an X-word u, we denote by juj the minimal natural number such that u juj is undefined.
The value juj where u 2 X is called length of u.
As usually, we identify n 2 X with the X-word u 2 X such that u 0 = n and u k is undefined if k > 0.
For u 2 X and s 2 X1, we denote by us the next X-sequence us = For s 2 X1 and m 2 N, we denote by sm:: the next X-sequence sm:: = s(k + m) if this value is defined is undefined otherwise Also for s 2 X1 and m; l 2 N, we denote by sm::l the next X-word sm::l = s(k + m) if this value is defined and k < l is undefined otherwise m
The principal concepts for our studying is given by the following definitions
P whenever 0 m < juj.
X is called prefix-free if u 2 P ensures u0::m 2= Remark 1. If a prefix-free subset of X contains then this subset is f g. 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 s 2 S if for any m 2 N, s0::m = s00::m for some s0 2 S.
3
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 a a F a f F f b
b F b commutes or, equivalently, the equation (F f ) a = b f holds.
Proposition 1. The class of F -coalgebras equipped with F -morphisms is a category 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 models of programming and specification languages.
(
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 coalgebras a and b is a span a ra r r!b b in category CoalgF (C) such that the span a ra r r!b b in category C is a mono-span i.e. the validity of rah0 = rah00 and rbh0 = rbh00 for any object c in C and morphisms h0; h00 : c ! r ensures h0 = h00.
The next proposition demonstrates that coalgebra morphisms give the simplest examples of bisimulations. span a ida a !f b is a bisimulation of a and b.
Proposition 2. For any F -coalgebras a and b and F -morphism f : a ! b, the Proof. We need to note only that the span a ida a !f b is evidently a monospan. tu Proposition 3. Assume that category C is finitely complete and there is a final F -coalgebra then for any bisimulation a ra r r!b b of F -coalgebras a and b, there exists a unique monomorphism f : r ! P such that ra = paf and rb = pbf where a pa P p!b b is the pullback of the cospan a (a!) nF (b) b. Proof. Indeed, the definition of an anamorphism ensures the commutativity of the next diagram ra r a rb (a) b
(b) nF i.e. for the pullback a pa P p!b b of the cospan a (a!) nF (b) 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. tu This statement can be inverted for some class of endofunctors. nF 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)
b is the greatest bisimulation of F -coalgebras a and b.
Proof. Indeed, let a pa P p!b b be the mentioned above pullback then it is mono-span and the next diagram is a pullback diagram. Further, note that the outer square of the following diagram commutes.
pa
P a
F pa
F P F a 9 a
F pb F (a)
pb F P
F a F pa
F b
F (b) F nF F pb F (a) b
b F b
F (b) F nF Indeed,
F (a) apa = (nF ) (a) pa = (nF ) (b) pb =
F (b) bpb considering that (a) is an F -morphism using the pullback property for a pa P considering that (b) is an F -morphism. p!b b Thus, taking into account the pullback property for the inner subdiagram in the diagram above, one can derive the existence of ensuring the diagram commutativity. But it means that the span a pa P p!b b can be lifted up to the corresponding span of coalgebras. tu Another concept used below is the concept of subcoalgebra.
Definition 7. Let a 2 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])
(
C f = idC is a polynomial endofunctor;
(
F 1 X F 2 X and F f = F 1 f F 2 f is a polynomial endofunctor;
(
An important property of polynomial endofunctor is that such an endofunctor preserves pullbacks. 4
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 nIdSet = 1 and nIdSet = id1. Thus, taking into account that category Set and functor IdSet satisfy conditions of Prop. 4 one can conclude that any two dynamical 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 f+g 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 2 g, either gx = + and h(f x) = + or gx 6= + and f (gx) = h(f x).
There is a final nT in the category Sys(T). This object is structured as follows nT = 1 + N nT = x 2 1 + N : <8 + if x = 0
1 if x = 1 : x 1 otherwise where 1 + N = N Sf1g For a T-system g, the corresponding anamorphism (g) is defined as follows (g) = x 2 g :
1 if g(k)x 6= + for all k 2 N+
minfk 2 N j g(k+1)x = +g otherwise
where
g(
= g g(k+1) = x 2 g :
+ if g(k)x = + g(g(k)x) otherwise for k 2 N+: Note 1. Everybody familiar with the concept of a monad can easily see that g(k) is the kth-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 SN f = idN
X for any object X of category Set; 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; trii 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 nSN in the category Sys(SN). This object is structured as follows nSN (nSN)out = (nSN)tr = = NN; s 2 NN : s 0; s 2 NN : k 2 N : s(k + 1).
For an N-system formula ( ) =
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.
, the corresponding anamorphism ( ) is defined by the next 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 category Set; DN f = 2 (1 + X)N : n 2 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 2 a and n 2 N,
(
Proposition 5. The class Sys(DN) of N-detectors equipped with detector morphisms forms a category.
Proof is a simple check of the categories axioms.
The following theorem describes a final detector. tu Theorem 1. There is a final object in category Sys(DN) that is structured as follows nDN is the set of all prefix-free subsets of N+; nDN = P 2 nDN : n 2 N : n 1+ P iofthner2wPise .
For an a N-detector, the corresponding anamorphism (a) is defined by the next formula (a) = x 2 a : fu 2 N+ ja+(x; u) = + and
a+(x; u0::k) 6= + whenever 0 < k < jujg where a+ : a
N+ ! 1 + a defined as follows a+(x; n) = (ax) n a+(x; un) =
+ aa+(x; u) n if a+(x; u) = + otherwise x 2 a; n 2 N; x 2 a; n 2 N; u 2 N+: 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 2 a, and u; v 2 N+, the equation a+(x; uv) =
+ a+ a+(x; u); v if a+(x; u) = + 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 2 N, (
Assume that v = v0n, n 2 N, and (
Then under assumption that a+(x; uv0) = +, we have
a+(x; u(v0n)) = a+(x; (uv0)n) = + by definition of a+. Hence, a+(x; uv) = +.
In the other side, we have a+(a+(x; u); v0) = a+(x; uv0) = + by induction hypothesis. But then a+(a+(x; u); v) = a+(a+(x; u); v0n) = + by definition of a+. Hence, we have a+(x; uv) = a+(a+(x; u); v).
In contrary, assumption that a+(x; uv0) 6= + gives
= a+(a+(x; u); v0n) = a+(a+(x; u); v) by definition of a+:
(
Lemma 2. If P N+ is prefix-free then n 1 P whenever n 2 N and n 2= P . by definition of a+ by induction hypothesis
Proof. Firstly, n 2= P ensures 2= n 1 P i.e. n 1 P N+. Further, if u 2 n 1 P and u0::m 2 n 1 P for 0 m < juj then nu 2 P and nu0::m 2 P . Taking into account nu0::m = (nu)0::m+1, one can obtain a contradiction, which completes the proof.
Lemma 3. Any prefix-free subset P of N+ can be represented as the following
disjunctive union
tu
(
X n2NnNP P = NP + n Pn
where
NP = fn 2 N j n 2 P g and Pn = n 1 P:
Proof. Assume u 2 P then either u = n for some n 2 N or juj > 1. In the
first case, we have u 2 NP and, therefore, u belongs to the right side of (
Now assume u belongs to the right side of (
P n Pn. In the first case, we have u = n 2 NP i.e. u 2 P by definition n2NnNP of NP . In another case, u 2 n Pn where n 2 N n NP . Hence, u = nu1:: and u1:: 2 n 1 P . The last means that u 2 P . tu Now all is ready for proving Theorem 1.
Proof (Proof of Theorem 1). Firstly, nDN : nDN ! DN nDN due to Lemma 2. Hence, nDN is an N-detector.
Further, let us show that the mapping (a) : a ! nDN defined above for any N-detector a is an N-detector morphism.
If (ax) n = + then n 2 (a) x i.e. nDN((a) x) n = +.
Conversely, if nDN((a) x) n = + then n 2 (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 2 N+ and, therefore, (a) (ax) n = ? too. Also, we have
nDN( (a) x) n = (nDN ?)n = n 1 ? = ? = (a) (ax) n : In another case, we have both (ax) n 6= + and (a) x 6= ?.
If u 2 nDN( (a) x) n = n 1 ( (a) x) then nu 2 (a) x i.e. a+(x; nu) = + but
a+(x; nu0::m) 6= + whenever m < juj. Hence, for any m juj and v = u0::m, we
have
a+(x; nv) = a+(a+(x; n); v) = a+((ax) n; v)
(
Conversely, if u 2 (a) (ax) n then (
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 morphism from a into nDN i.e. f = (a) for any f : a ! nDN.
Assume f x = ? then we have the next chain of equivalent statements f x = ? n 1 (f x) = ? for all n 2 N nDN(f x) n = ? for all n 2 N (ax) n 6= +
and f (ax) n = ? for any n 2 N a+(x; u) 6= + (a) x = ? for all u 2 N+ by definition of nDN due to the N-morphism properties by induction on u by definition of (a): Hence, f x = ? iff (a) x = ?.
Now using induction on juj, prove that u 2 f x if and only if u 2 (a) x. If juj = 1 then we have the next chain of equivalent statements. Hence, u 2 f x iff u 2 (a) x for any u 2 N+ such that juj = 1.
If juj = m > 1 and the required statement is true for v 2 N+ such that jvj < m then we have the next chain of equivalent statements.
by definition of nDN due to the N-morphism properties by definition of (a): by definition of nDN and due to Lemma 3 due to the N-morphism properties by induction hypothesis due to Lemma 1 by definition of (a): n 2 f x for some n 2 N nDN(f x) n = + (ax) n = + n 2 (a) x u 2 f x u1:: 2 (u 0) 1 (f x) u1:: 2 nDN(f x) (u 0) u1:: 2 f (ax) (u 0) u1:: 2 (a) (ax)(u 0) a+ (ax)(u 0); u1:: = + but a+ x; (u 0)u1:: = + but u 2 (a) x a+ (ax)(u 0); u1::k 6= + whenever k < m by definition of (a) a+ x; (u 0)u1::k 6= + whenever k < m Thus, f = (a) . tu Below we need a characterisation of the subsets of nDN that are carriers of subcoalgebras. The next proposition gives this characterisation. Proposition 6. A subset C nDN is the carrier of a subcoalgebras of the final detector defined by the natural embedding jC : C ! nDN if and only if the condition for any P 2 C and n 2 N; either n 2 P or
Proof boils down to simply checking the requirements of definitions. 5
The general coalgebraic framework for recognising violations of the behaviour of a system with output is introduced and studied in this section. 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
Join( ; a) = (x; y) 2 a :
+ tr x; (ay)( out x) if (ay)( out x) = + otherwise Further for systems morphism f : Join(f; g) :
and with output N and N-detectors a and b, an
SN! , and a detector morphism g : a ! b, we define the mapping
a ! b by the formula
Join(f; g) = f
g:
tu
(4a)
(4b)
Theorem 2. Rules (
Sys(DN) ! Proof. Firstly, let us check that for any f : ! and g : a ! b where ; 2 Sys(SN) and a; b 2 Sys(DN), Join(f; g) is a T-morphism from Join( ; a) into Join( ; b).
Indeed, let Join( ; a) (x; y) = + where x 2 , y 2 a then we have the next chain of equivalent statements
Join( ; a) hx; yi = + (ay)( outx) = + (ay)( out(f x)) = + b(gy)
out(f x) = + Join( ; b) hf x; gyi = + Join( ; b)
Join(f; g)hx; yi = + by definition of Join( ; a) due to f is an SN -morphism due to g is a DN -morphism by definition of Join( ; b) by definition of Join(f; g) Now assume that Join( ; a) hx; yi 6= + (it means (ay)( outx) 6= +) where x 2 , y 2 a then
Join(f; g)
Join( ; a) hx; yi = Join(f; g)
trx; (ay)( outx) = f ( trx); g (ay)( outx) 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. TNhaenodreamqa3.rLqe!bt b pbe a bpi!simubleataiobnisoimfuNla-dtieotnecotofrssysateamnsd batnhden Jwoiitnh(o;urt)puist a bisimulation of Join( ; a) and Join( ; b). tu Proof. Let us consider the span
Join( ; a) Join(p ;qa) Join( ; r) Join(p ;qb!) Join( ; b): It is sufficient to show that the corresponding span 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 ; gri and h = hh ; hri respectively where g ; h : S ! and gr; hr : S ! r.
Taking into account that a p qa r p q!b (p (p qa)g = (p qa)h = (p qa)hg ; gri = hp g ; qagri qa)hh ; hri = hp h ; qahri and we have hp g ; qagri = hp h ; qahri i.e. p g = p h and qagr = qahr due to properties of product. Similarly, we have p g = p h and qbgr = qbhr from and the bisimulation ! .
Similarly, we have gr = hr due to the conditions qagr = qahr and qbgr = qbhr and the bisimulation a qa r q!b b.
Thus, g = h and, therefore, the considering span a p qa r p q!b is realy a mono-span. 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 2 NN, let us define the following system [s] with output namely [s] = sk:: j k 2 N and [s] = t 2 [s] : t 0; t1:: : Further for any N-detector a and x 2 a, let us define the following set
JaKx = fs 2 NN j (Join([s]; a))hs; xi = 1g: The next simple fact is useful below.
Lemma 4. For s 2 NN, an N-detector a, and x 2 a,
Join([s]; a) (m)hs; xi =
+ hsm::; a+(x; s0::m)i if a+(x; s0::m) = + otherwise for m > 0: 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.
Let Join([s]; a) (m)hs; xi = + then a+(x; s0::m) = + by induction hypothesis. The definition of a+ ensures a+(x; s0::m+1) = +. But Join([s]; a) (m+1)hs; xi = + by definition. Hence, the equation holds in this case.
Finally, assume Join([s]; a) (m)hs; xi 6= + then
Join([s]; a) (m)hs; xi = hsm::; a+(x; s0::m)i by induction hypothesis i.e. a+(x; s0::m) 6= +. Thus,
Join([s]; a) (m+1)hs; xi = Join([s]; a)
Join([s]; a) (m)hs; xi = Join([s]; a) hsm::; a+(x; s0::m)i: Now applying (4a), we obtain the required expression for Join([s]; a) (m+1)hs; xi. Lemma 5. For any N-detector a and x 2 a, the set JaKx is a safety constraint. Proof. Indeed, let us assume the existence of s 2= JaKx such that the equation s00::m = s0::m holds for any m 2 N and for some s0 2 JaKx depending in generally on m.
The fact s 2= JaKx ensures (Join([s]; a))hs; xi = K for some K 2 N. It means (see Lemma 4) a+ x; s0::K+1 = +. Let s0 2 JaKx such that s00::K+1 = s0::K+1 then a+ x; s00::K+1 = + and, therefore, (Join([s0]; a))hs0; xi = K. But (Join([s0]; a))hs0; xi = 1 by the assumption s0 2 JaKx. This contradiction completes the proof. tu The following lemma is less simple.
x 2 aS such that JaS Kx = S.
Proof. Let us define the N-detector aS as follows (note that 2 aS )
NN, there exist an N-detector aS and aS = f g [
u 2 N+ j u = s0::juj for some s 2 S aS = u 2 aS : and prove that JaS K = S.
Let us assume s 2 S then s0::m 2 aS for any m 2 N. Hence, aS+(s0::m; s m) = s0::m+1 2 aS for each m i.e. (Join([s]; aS ))hs; i = 1. Thus, s 2 JaS K . Conversely assume s 2 JaS K then (Join([s]; aS ))hs; i = 1 and, therefore, Join([s]; aS ) (m)hs; i 6= + for each m > 0. Lemma 4 ensures
s0::m = aS+( ; s0::m) 2 aS for all m > 0 that guarantees existence s(m) 2 S such that s(0m:: m) = s0::m. Now using the safeness of S, one can conclude s 2 S. tu Theorem 4 (about universal detector). A subset S NN is a safety constraint if and only if there exist P 2 nDN such that S = JnDNKP . 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 2 a such that S = JaKx. Let us take P = (a) x and prove (Join([s]; a))hs; xi = (Join([s]; nDN))hs; P i. Indeed, for the T-morphism Join id[s]; (a) : Join([s]; a) ! Join([s]; nDN), we have
Join id[s]; (a)
hs; xi = id[s]
(a) hs; xi = hs; P i:
(
(Join([s]; a))hs; xi = (Join([s]; nDN))hs; P i: Considering the last equation holds whenever P = (a) x, one can conclude that S = JaKx = JnDNKP .
Corollary 1. A subset S NN is a safety constraint if and only if it is equal to fs 2 NN j s0::m 2= P for any m > 0g for some prefix-free subset of N+. Proof. It follows immediately from Theorem 4.
Corollary 2. For any N-detectors a and b and x 2 a and y 2 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. 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 = fJaKx j x 2 ag 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
detector if and only if there exists C nDN that meets the following conditions
for any P 2 C;
either n 2 P
or
Proof. Firstly, let us assume the family F is a family with a universal detector
then Prop. 6 guarantees the validity of conditions (
Conversely, let us define the next mapping a : C ! DN C a = The correctness of this definition is ensured by (6a), hence a is an N-detector and, due to (6b), it is a universal detector.
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 2 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 = fP
N+ j P = (a) x for some detector a with finite carrier and x 2 ag then any P 2 C is a regular prefix-free subset of N+ (see, for example, [6, Theorem 1]).
Now let us check that C satisfies conditions (
Hence, we need only due to Theorem 5 to check that n 1 P is a regular set under assumption n 2= 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; I0 Q; F Qi where I0 = fq 2 Q j hq0; n; qi 2 T for some q0 2 Ig. It is evident that the constructed machine accepts exactly n 1 P and, therefore, n 1 P 2 C. tu 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 2 nDN such that P is decidable and S = JnDNKP . 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 universal 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 2 n 1 P for a decidable prefix-free subset P of N+, any u 2 N+, and n 2 N such that n 2= P , by checking nu 2 P with a decision procedure for P . 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 2 nDN such that P is recursively enumerable and S = JnDNKP . 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
semidecision procedure for checking the statement u 2 n 1 P with a recursively
enumerable prefix-free subset P of N+, any u 2 N+, and n 2 N such that
n 2= P . This procedure is as follows
(
In other cases, nu 2= P i.e. u 2= n 1 P .
Thus, the furnished procedure is really a semi-decision procedure for the statement u 2 n 1 P . tu 6
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
(
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”.