=Paper=
{{Paper
|id=Vol-2732/20200029
|storemode=property
|title=Understanding Clock Constraints Coalgebraically
|pdfUrl=https://ceur-ws.org/Vol-2732/20200029.pdf
|volume=Vol-2732
|authors=Grygoriy Zholtkevych,Maksym Labzhaniia
|dblpUrl=https://dblp.org/rec/conf/icteri/ZholtkevychL20
}}
==Understanding Clock Constraints Coalgebraically==
https://ceur-ws.org/Vol-2732/20200029.pdf
Understanding Clock 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. The paper is devoted to the problem specifying causality re-
lationships in distributed (including cyber-physical) systems. This prob-
lem is studied based on the coalgebraic approach used authors for study-
ing safety constraints for distributed systems. The special class of coal-
gebras, counter-based detectors, is introduced and studied in the paper.
It is shown that this approach allows using the technique of Diophantine
equations for specifying clock constraints of the system being studied.
The advantage of the approach is the possibility for defining the com-
plexity of detectors that provides to control respond time of the detectors
in the system.
Keywords: a coalgebra, a detector coalgebra, a counter-based detector,
Diophantine equation, Clock Constraint Specification Language
1 Introduction
This paper presents the authors’ research continuing the research presented in
[1] and applying the proposed approach and results in a more specific situation.
The general context of our study is determined by the observation that mod-
ern technical systems are, as a rule, compound and smart. Moreover, such sys-
tems can be hybrid in the sense that ones consisted of physical, cybernetic (soft-
ware), and, maybe, social components. This character of the systems should be
taken into account under designing ones.
The software components of such systems are reactive, that is, they are de-
signed for providing the required behaviour of the system, and not for obtaining
any computational result.
Components of such systems are distributed in space but should act for
guaranteeing the required behaviour of the system in the whole. So, supporting
the necessary causality relationships during operating of system components is
one of the principal problems of designing a system of such a kind.
?
The author 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.
Copyright © 2020 for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
Also, we need to remark the incorrect behaviour of a system of the considering
kind can have serious and some times catastrophic consequences for the system
surroundings. Hence, systems of this class can be characterised as safety-critical
systems. Thus, all designing solutions for them should be rigorous verified.
This research is some attempt to build a foundation for rigorous and effective
specification and analysis of causality relationships in systems of the considering
class.
This paper applies the general framework proposed in [1] for constructing
rigorous models of logical time intended for using under developing domain-
specific languages for specifying causality constraints.
The paper is structured as follows.
Sec. 2 reminds basic concepts and notation.
Sec. 3 contains the necessary definitions and results for understanding the
general coalgebraic framework.
Sec. 4 contains a survey of used below results from [1].
Sec. 5 explains how results mentioned above can be used for specification and
analysis causality constraints.
Sec. 6 is the key in the article. Here, it is introduced the concept of a counter–
based detector; it is explained that this class of detectors is not complete; it is
constructed a Diophantine representation for detectors of this class.
Finally, Sec. 7 presents the construction of a universal simulator based on
the Diophantine representation for counter-based detectors.
2 Basic Concepts and Notation
This section is a copy of the corresponding section of our article [1] and here it is
presented only for providing notation consistency. Thus, 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 = s0 for some s0 ∈ S.
0..m
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 section1 .
Definition 3. A morphism a of C is called an F -coalgebra if the equation
cod a = F (dom a) is fulfilled. In the case, dom a is called the carrier of a and
denoted below by a.
1
General information on category theory can be found in [3,4], proofs of some facts
formulated in the subsection can be found in [1, Sec. 3]
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
Ff
Fa Fb
commutes 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.
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) .
4 Safety Behavioural Constraints
This section contains some servey of the results obtained in [1].
In [1], three endofunctors T, SN , and DN of category Set are considered.
Here N refers to some finite set of system notifications. The definitions of these
functors are given in Table 1.
Table 1. Functors T, SN , and DN definitions
F F X where X ∈ Set F f where X, Y ∈ Set and f : X → Y
⇓ if x = ⇓
T TX = 1 + X Tf = λ x ∈ TX .
f x otherwise
SN SN X = N × X SN f = idN ×f
⇓ if φ n = ⇓
DN DN X = (1 + X)N DN f = λ φ ∈ DN X . λ n ∈ N .
f (φ n) otherwise
In Table 1, “+” means disjoint union, 1 = {⇓} for some ⇓, and “×” means
Cartesian product.
In the mentioned above paper, any SN -system σ : σ → SN σ is interpreted
as a system with output N (see [1, Subsec. 4.2]), any DN -system a : a → DN a
is interpreted as a detector of behavioural violations (see [1, Subsec. 4.3]), and
interrelation between systems with output and detectors is established using the
bifunctor combining a system and a detector into the system with termination
Join : Sys(SN ) × Sys(DN ) → Sys(T)
(see [1, Subsec. 5.1]). This bifunctor is defined as follows, let σ and a be a system
with output N and an N-detector respectively, one can define the system with
termination Join(σ, a) : σ × a → T(σ × a) by the next rules
⇓ if (ay)(σout x) = ⇓
Join(σ, a) = λ (x, y) ∈ σ × a . (1a)
σ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. (1b)
Above, we use the representation σ x = hσout x, σtr xi.
Further in [1], it is proposed to describe the set of streams accepted by a
detector a as follows
– 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.. ;
– now for any N-detector a and x ∈ a, let us define the following set
JaKx = {s ∈ NN | (Join([s], a))hs, xi = ∞}.
One of the main results obtained in [1, Lemmas 5 and 6] is established that any
safety constraint has the described above form.
Below we use this approach for studying causality constraints in distributed
systems.
5 Causality Constraints as a Kind of Safety Behavioural
Ones
Anywhere in this section, C is an arbitrary but fixed finite set of clocks and NC is
the corresponding set of clock notifications that is the set of all non-empty subset
of C. Informally, each message contains a list of clocks had ticked at the same
time as the message was sent. Thus, notifications are no longer atomic entities
or, in other words, first-class citizens. Now, clock ticks are atomic entities or,
in other words, first-class citizens, whose combinations are notifications. In this
section, we show how the results obtained in [1] should be adjusted for this more
specific situation.
5.1 Clock and Schedules Coalgebraically
The logic clock model considers clock tick notification streams as the only infor-
mation available about temporal order between events. These streams are called
schedules in the model context. Thus, the coalgebraic meaning of schedules is
related to the endofunctor SNC : Set → Set defined like to the endofunctor SN
from [1, Subsec. 4.2] namely
SNC X = NC × X for any object X of category Set;
SNC f = idNC ×f for any objects X and Y of category Set and a morphism
f :X→Y
then a system equipped with the clock set C is an SNC -system.
In other words, a system equipped with a clock set C is a mapping
σ : X → SNC X that both specifies the state transition σtr : X → X and
the corresponding ensemble of clock ticks σout : X → NC of the system such
that σ = hσout , σtr i is a universal arrow from X into NC × X.
A final SNC -system νSNC is defined on the set NCN of all schedules and has
λ s ∈ NCN . s1.. as the transition function and λ s ∈ NCN . s 0 as the output
function (see, [1, Subsec. 4.2]).
Due to the general results mentioned in [1, Sec. 3 and Subsec. 4.2], our
capacity to formulate causality constraints for any system equipped with a clock
set C are limited by statements in schedules terms only.
5.2 Detectors of Causality Constraint Violations
Detectors of causality constraint violations are described with using the endo-
functor DNC : Set → Set defined like to [1, Sec. 4.3] namely
DNC X = (1 + X)NC for any object X of category Set;
NC ⇓ if φ n = ⇓
DNC f = λ φ ∈ (1 + X) . λ n ∈ NC .
f (φ n) otherwise
for any objects X and Y of category Set and a morphism f : X → Y .
Definitions of bifunctor Join, sets of the form JaKx where a is an NC-detector,
and x ∈ a are remained without changing.
6 Counter-based Detectors and Their Diophantine
Representation
In this section, we consider a special class of NC-detectors2 . Some detectors
of this class are used for defining semantics of Clock Constraint Specification
Language (CCSL) [5].
In this section, we use the function occc : NC∗ → N associated with c ∈ C as
follows
0 if u =
occc = λ u ∈ NC∗ . occc u0 if u = u0 n for u0 ∈ NC∗ , n ∈ NC, and c ∈ /n
occc u0 + 1 if u = u0 n for u0 ∈ NC∗ , n ∈ NC, and c ∈ n
2
In this section, C is some clock set
This function counts how many times the corresponding clock ticked if the sched-
ule begin coincides with the function argument.
6.1 Counter-based Detectors
Let V ⊂ NC × NC then an NC-detector cV is called a counter-based NC-detector
if it is defined as follows
cV = NC
C ⇓ if hn, xi ∈ V
cV = λ x ∈ N . λ n ∈ NC .
x + n otherwise
(x c) + 1 if c ∈ n
where x + n = λ c ∈ C . .
xc otherwise
Our nearest aim is to establish whether the family of causality constraints
recognised by counter-based detectors is a family with a universal detector.
The first step for achieving the claimed aim is given by the next theorem.
Theorem 1. Let P be a prefix-free subset of NC+ then there exists A ⊂ NC×NC
such that (cA) x = P for some x ∈ cA if and only if P meets the following
condition
for any v ∈ NC+ ,
u0 v ∈ P is equivalent to u00 v ∈ P whenever u0 , u00 ∈ NC+ are such
that (2)
u00..m ∈
/ P and u000..k ∈
/ P for all 0 < m ≤ |u0 |, 0 < k ≤ |u00 | and
0 00
occc u = occc u for each c ∈ C.
For proving the theorem, we need some auxiliary results.
Lemma 1. For any V ⊂ NC × NC and x ∈ cV , (cV) x meets condition (2).
Proof. Let us assume P = (cV) x for some V ⊂ NC × NC and x ∈ cV and
take u0 , u00 ∈ NC+ such that u00..m ∈
/ P and u00..k ∈/ P for all 0 < m ≤ |u0 |,
00 0 00
0 < k ≤ |u | and occc u = occc u for each c ∈ C.
Then the first group of conditions ensures c+ 0 + 00
V (x, u ), cV (x, u ) ∈ cV and the
condition occc u = occc u for each c ∈ C ensures cV (x, u ) = c+
0 00 + 0 00
V (x, u ).
+
Now, for an arbitrary v ∈ NC and 0 < k ≤ |v|, we have (see [1, Lemma 1])
0 0
c+ + +
V (x, u v0..k ) = cV (cV (x, u ), v0..k )
00 00
= c+ + +
V (cV (x, u ), v0..k ) = cV (x, u v0..k )
Thus, one can conclude u0 v ∈ P is equivalent to u00 v ∈ P .
Proof (Proof of Theorem 1). Taking into account Lemma 1, we need only to
prove that for any prefix-free P ⊂ NC satisfying condition (2), there exists
V ⊂ NC × NC such that P = (cV) x for some x ∈ cV .
To do this let us take
V = {hn, xi ∈ NC × NC |
vn ∈ P for some v ∈ NC∗ such that x = λ c ∈ C . occc v}
and check that (cV) z = P where z = λ c ∈ C . 0 i.e. that for any u ∈ NC+ ,
u ∈ (cV) z iff u ∈ P .
Let us assume that u ∈ (cV) z.
If u = n for some n ∈ NC then n ∈ (cV) z means (cV z) n = ⇓ i.e. n ∈ P because
of λ c ∈ C . occc v = z iff v = .
If u ∈ (cV) z and m = |u| > 1 then for x0 = z, we have xk+1 = (cV xk )(u k) ∈
cV whenever k = 0, . . . , m − 2 and (cV xm−1 )(u(m − 1)) = ⇓. In other words,
hu k, xk i ∈
/ V where k = 0, . . . , m − 2 and hu(m − 1), xm−1 i ∈ V.
Thus, u0..k ∈ / P for any 0 < k ≤ m − 1 but there exists v ∈ NC∗ such that
vu(m − 1) ∈ P and λ c ∈ C . occc v = λ c ∈ C . occc u0..m−1 . But the condition
vu(m − 1) ∈ P implies v0..l ∈ / P for any 0 < l ≤ |v| due to P is a prefix free set.
Thus, condition (2) ensures u = u0..m−1 (u(m − 1)) ∈ P .
Now assume u ∈ P and m = |u|.
Then we have u0..k ∈ / P for any k such that 0 < k < m and hu(m − 1), λ c ∈
C . occc u0..m−1 i ∈ V due to the definition of V. One can conclude that huk, λ c ∈
C . occc u0..k i ∈
/ V for any 0 ≤ k < m − 1. Indeed, otherwise there exists 0 ≤ k <
m−1 and v ∈ NC∗ such that v(uk) ∈ P and λ c ∈ C.occc v = λ c ∈ C.occc u0..k .
But condition (2) ensures u0..k (uk) = u0..k+1 ∈ P for some 0 ≤ k < m−1. Thus
c+ +
V (z, u0..k ) ∈ cV for 0 < k < m and cV (z, u) = ⇓. Therefore we have u ∈ (cV) z.
Corollary 1. If P = (cV) x for some V ⊂ NC × NC and x ∈ cV then P = (cV0) z
for some V0 ⊂ NC × NC and z = λ c ∈ C . 0.
Corollary 2. The family of clock constraints being detected by counter-based
detectors is a constraint family with a universal detector.
Proof. To prove this fact, we use [1, Theorem 5]. Assume P = (cV) z for some
V ⊂ NC × NC .
Let n ∈ / P , u00..m , u000..k ∈
/ n−1 · P for all 0 < m ≤ |u0 | and 0 < k ≤ |u00 |, and
occc u = occc u for any c ∈ C then nu00..m ∈
0 00
/ P and nu000..k ∈
/ P . Theorem 1
0 00
ensures (nu )v ∈ P and (nu )v ∈ P are equivalent for any v ∈ NC+ i.e.
u0 v ∈ n−1 · P and u00 v ∈ n−1 · P are equivalent.
Theorem 1 allows us to show the impossibility of confining ourselves to counters
based detectors, as shown in the next example and the remark following after
it.
−
Example 1. Let us take C = {c+ + −
1 , c1 , . . . , cm , cm } for some m > 1 and define the
next NC-detector q
q = {c1 , . . . , cm }∗
u{ck } if n = {c+
k}
for some k = 1, . . . , m
q = λ u ∈ {c1 , . . . , cm }∗ . λ n ∈ NC . u0 if u = {ck }u0 and n = {c− k}
for some k = 1, . . . , m
⇓ otherwise
Also, let us take P = (q) , and {c+ + + +
i }{cj }, {cj }{ci } ∈ NC
+
for any 1 ≤ i 6=
j ≤ m. Then it is evident q (, {ci }{cj }) 6= ⇓, q (, {cj }{c+
+ + + + +
i }) 6= ⇓, and
occc± {c+
i }{c +
j } = occc
+
j
+
i
+
± {c }{c } for all k = 1, . . . , m. In other words, {c } ∈
i / P,
k k
{c+ +
/ P , {c+
i }{cj } ∈ / P , {c+
j }∈
+
/ P , and occc± {c+
j }{ci } ∈
+
i }{cj } = occc± {c+ +
j }{ci }
k k
for all k = 1, . . . , m.
The assumption P = (cV) x for some V ⊂ NC × NC and x ∈ cV leads to the
− −
equivalence of the statements {c+ + + +
i }{cj }{ci } ∈ P and {cj }{ci }{ci } ∈ P due
to Lemma 1.
− −
But the definition of q ensures {c+ +
/ P and {c+
i }{cj }{ci } ∈
+
j }{ci }{ci } ∈ P . This
C
contradiction proofs that for any V ⊂ NC × N and x ∈ cV , P = (cV) x is false.
Remark 2. This abstract example has practical value. Indeed, let we have m(m >
1) servers each of them provides access to the queue being stored by it. Then
−
c+
k and ck can be interpreted as append and pop operations respectively for the
th
k queue.
Example 1 guarantees the behaviour like to a queue behaviour for the system of
the servers cannot be ensured by a counter-based detector.
Remark 3. Reasoning similar to the reasoning given in Example 1 leads to the
conclusion that the behaviour like to a stack for the system of the servers cannot
be ensured by a counter-based detector.
6.2 Diophantine Representation of a Counter-Based Detector
The definition of a counter-based detector ensures that such a detector cV is
uniquely defined by the corresponding set V ⊂ NC × NC , which below is referred
as the defining set of a counter-based detector. Hence, to specify cV we need
to specify V. Taking into account that any tool for specifying a set can specify a
recursively enumerable set only, we concentrate on counter-based detectors with
the recursively enumerable determining set. Such a counter-based detector is be-
low called a recursively defined counter-based detector. Everywhere below
we consider counter-based detectors with the recursively enumerable defining set
only.
Note that a set V ⊂ NC × NC is recursively enumerable if and only if the
sets Vn = {x ∈ NC | hn, xi ∈ V} are recursively enumerable for all n ∈ NC.
This claim follows directly from the finiteness of NC. In other words, to spec-
ify a recursively enumerable set V ⊂ NC × NC is equivalent to specify the set
{Vn | n ∈ NC} of recursively enumerable subsets of NC .
Due to Matiyasevich-Davis-Robinson-Putnam theorem (see, [6]), the last is equiv-
alent to specifying for any n ∈ NC a polynomial Pn such that
Vn = {x ∈ NC | Pn (x, y1 , . . . , ys ) = 0 for some y1 , . . . , ys ∈ N}.
Thus, any family of the species {Pn ∈ Z[x1 , . . . , xm , y1 , . . . , ys ] | n ∈ NC} where
m is the cardinal number of C and s is some positive natural number specifies
the set V ⊂ NC × NC as follows
(1) let us select some enumeration {c1 , . . . , cm } of clocks from C;
(2) let us associate natural variable xi with clock ci (1 ≤ i ≤ m);
(3) for each n ∈ NC, let us specify polynomials Pn ∈ Z[x1 , . . . , xm , y1 , . . . , ys ];
(4) let us assume
hn, xi ∈ V iff ∃ y1 ∈ N; . . . ; ys ∈ N, Pn (x, y1 , . . . , ys ) = 0.
Below we refer to this manner of specifying the defining set of a counter-based
detector as to a Diophantine Representation of the detector.
Example 2 (of a Diophantine Representation). Let us assume C = {c1 , c2 } and
consider the clock constraints specification defined as in Table 2. This specifica-
Table 2. An example of a Diophantine Representation
c1 c2 P (x1 , x2 , y1 ) Diophantine set
0 1 x1 − x2 + y1 {(x1 , x2 ) ∈ N2 | x1 ≤ x2 }
1 0 1 + x1 − x2 + y1 {(x1 , x2 ) ∈ N2 | x1 < x2 }
1 1 x1 − x2 + y1 {(x1 , x2 ) ∈ N2 | x1 ≤ x2 }
tion determines that clock c1 is strictly faster than clock c2 and can be considered
as a specification of the Lamport’s relation “happen before” (see [7]).
Note that the rows corresponding to the situation c1 does not tick but c2
ticks and also to the situation c1 and c2 tick at the same time are coincide in
columns 3 and 4. Hence, we can represent Table 2 as follows
c2 ⇒ x1 − x2 + y1 = 0
c1 ∧ ¬c2 ⇒ 1 + x1 − x2 + y1 = 0
7 Universal Diophantine Simulator of Recursive
Counter-Based Detectors
In this section, we use Diophantine Representation for describing a universal
algorithm simulating any counter-based detector if its defining set is recursive.
The main advantage of this result is that it gives a metric for estimating the
complexity of the detector and the detection problem. Namely, the number of
additional variables and the power of the polynomial representing the corre-
sponding Diophantine set can be used for defining such a metric. The detailed
discussion of this problem one can find in [8].
Let us assume the the universal Diophantine simulator is set up for simu-
lating the counter-based detector with the defining set specified by polynomials
{Pn (x1 , . . . , xm , y1 , . . . , ys ) | n ∈ NC} under assumption that the clock set is
enumerated as follows C = {c1 , . . . , cm }. Also, we choose some algorithm α enu-
merating the set Ns without repetitions. We mean below that α i is the i-th
member of this enumeration.
We begin describing the universal Diophantine simulator of recursive counter-
based detectors with specifying its composite structure (see Fig. 1). The simula-
Fig. 1. Composite structure of the universal Diophantine simulator of recursive
counter-based detectors
tor consists of one passive component (NotificationLog) and two active ones
(NotificationListener and NotificationHandler).
Component NotificationLog is a data store that allows to write data items
in append and direct access modes and to read ones in direct access mode.
Component NotificationListener provides listening the notifications chan-
nel and writing the corresponding data items using the interface of component
NotificationLog in accordance with the next algorithm.
NotificationListener:
(1) xk ← 0 for k = 1, . . . , m
(2) wait on receiving a notification
(3) let the received notification be n then append to NotificationLog the
item (x1 , . . . , xm , n, 0)
(4) xk ← xk + 1 for k = 1, . . . , m such that ck ∈ n
(5) go to (2)
Component NotificationHandler provides handling data items stored with
NotificationLog for recognising behaviour violation in accordance with the
following algorithm.
NotificationHandler:
(1) i ← 0
(2) j ← 0
(3) try to read j-th element from NotificationLog
(4) if the attempt is successful then
(5) let (x1 , . . . , xm , n, t) be the reading result
(6) (y1 , . . . , ys ) ← α t
(7) if Pn (x1 , . . . , xm , y1 , . . . ys ) = 0 then
signal about the recognised violation and terminate the handling
(8) rewrite (x1 , . . . , xm , n, t + 1) at j-th entry of NotificationLog
(9) j ←j+1
(10) if j > i then i ← i + 1 and j ← 0
(11) go to (3)
(12) else go to (2)
Of course, the proposed universal Diophantine detector is not efficient. For
providing efficiency a detector, we need to require the decidability of Diophantine
problems related to the detector. For example, we can consider detectors with
linear in y1 , . . . , ys the related to them Diophantine problems. In this case, the
complexity of a detector is determined by the complexity of generalized Euclid’s
algorithm finding the greatest common divisor of coefficients for the correspond-
ing polynomials. Perhaps, other classes of decidable Diophantine problems give
also detectors with the controllable complexity.
8 Conclusion
Summing up the mentioned above we can conclude that idea to use the coal-
gebraic approach for studying logical time in distributed systems gives some
interesting results.
First of all, we see that the coalgebraic technique developed in [1] can be
used in this more special case. Of course, in this case, we have a possibility
enriching the model by using the specific structure of a notification set. It gives
us to introduce a mechanism of counting clock ticks and to use values of the
corresponding counters for formulating behavioural constraints.
Unfortunately, such an arithmetization does not provide specifying all rea-
sonable causality constraints as it is demonstrated by Example 1 and Remark 3.
But it provides a possibility to use a concept of Diophantine complexity [8] for
classifying causality constraints of such a kind in accordance with the efficiency
of detecting algorithms.
We need to note that assessing the efficiency of detecting algorithms requires
answers the following questions
– How to build new detectors from simpler ones?
– Do such constructions possess the universality property?
– Can assess the complexity of the constructed detectors based on the com-
plexity of their components?
These questions define the directions of our future research.
References
1. Zholtkevych, G., Labzhaniia, M.: Understanding Safety Constraints Coalgebraically.
In: Computational Linguistics and Intelligent Systems, CEUR Workshop Proceed-
ings, vol. 2604, pp. 1–19. CEUR-WS (2020)
2. Alpern, B., Schneider, F.: Recognizing safety and liveness. Distributed Computing
2, 117–126 (1987)
3. Mac Lane, S.: Categories for the Working Mathematician. Springer, 2nd edn. (2010)
4. Awodey, S.: Category Theory. Oxford University Press, 2nd edn. (2010)
5. André, C.: Syntax and Semantics of the Clock Constraint Specification Language
(CCSL). Tech. Rep. 6925 version 2, Inria (June 2009), https://hal.inria.fr/
inria-00384077/document
6. Matiyasevich, Y.: Hilbert’s 10th Problem. The MIT Press (1993)
7. Lamport, L.: Time, Clocks, and the Ordering of Events in a Distributed System.
CACM 21(7), 558–565 (1978)
8. Matiyasevich, Y.V.: Diophantine complexity. Journal of Soviet Mathematics 55,
1603–1610 (1991)