The paper is devoted to the problem specifying causality relationships in distributed (including cyber-physical) systems. This problem is studied based on the coalgebraic approach used authors for studying safety constraints for distributed systems. The special class of coalgebras, 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 complexity of detectors that provides to control respond time of the detectors in the system.
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 modern technical systems are, as a rule, compound and smart. Moreover, such systems can be hybrid in the sense that ones consisted of physical, cybernetic (software), 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 designed 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 domainspecific 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
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 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. us = k 2 N : s(k u k
if k < juj juj) otherwise
n 1 A = fu 2 X j nu 2 Ag where A
X and n 2 X: For s 2 X1 and m 2 N, we denote by sm:: the next X-sequence sm:: = k 2 N : 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 = k 2 N : 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.
s 2 S if for any m 2 N, s0::m = s00::m for some s0 2 S. XN such that 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 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 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.
(
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. In Table 1, “ +” means disjoint union, 1 = f+g 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
Join( ; a) = (x; y) 2 a :
+ tr x; (ay)( out x) if (ay)( out x) = + otherwise
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 (1a) (1b) Join(f; g) = f
g: 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 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:: ; – now 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: 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
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
The logic clock model considers clock tick notification streams as the only information 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; tri is a universal arrow from X into NC X.
A final SNC-system nSNC is defined on the set NCN of all schedules and has s 2 NCN : s1:: as the transition function and s 2 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 are described with using the endofunctor DNC : Set ! Set defined like to [1, Sec. 4.3] namely
DNC X = (1 + X)NC for any object X of category Set; DNC f = 2 (1 + X)NC : n 2 NC : f ( +n) iofthenrw=ise+
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 2 a are remained without changing. 6
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 2 C as follows occc =
u 2 NC : 2 In this section, C is some clock set 8 <
0 if u = occc u0 if u = u0n for u0 2 NC ; n 2 NC, and c 2= n : occc u0 + 1 if u = u0n for u0 2 NC ; n 2 NC, and c 2 n This function counts how many times the corresponding clock ticked if the schedule begin coincides with the function argument. 6.1
Let V NC NC then an NC-detector cV is called a counter-based NC-detector if it is defined as follows cV = NC cV = x 2 NC : n 2 NC :
+ if hn; xi 2 V x + n otherwise where x + n = c 2 C : (x cx)c+ 1 oitfhcer2wnise .
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 2 cA if and only if P meets the following condition that
u00::m 2= P and u000::k 2= P for all 0 < m
occc u0 = occc u00 for each c 2 C.
for any v 2 NC+,
u0v 2 P is equivalent to u00v 2 P whenever u0; u00 2 NC+ are such
ju0j, 0 < k
ju00j and
(
NC
NC and x 2 cV, (cV) x meets condition (
Proof. Let us assume P = (cV) x for some V NC NC and x 2 cV and take u0; u00 2 NC+ such that u00::m 2= P and u00::k 2= P for all 0 < m ju0j, 0 < k ju00j and occc u0 = occc u00 for each c 2 C.
Then the first group of conditions ensures cV+(x; u0); cV+(x; u00) 2 cV and the condition occc u0 = occc u00 for each c 2 C ensures cV+(x; u0) = c+(x; u00). V Now, for an arbitrary v 2 NC+ and 0 < k jvj, we have (see [1, Lemma 1]) cV+(x; u0v0::k) = cV+(cV+(x; u0); v0::k)
= cV+(cV+(x; u00); v0::k) = cV+(x; u00v0::k) Thus, one can conclude u0v 2 P is equivalent to u00v 2 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 (
To do this let us take
V = fhn; xi 2 NC
NC j vn 2 P for some v 2 NC such that x = c 2 C : occc vg and check that (cV) z = P where z = c 2 C : 0 i.e. that for any u 2 NC+, u 2 (cV) z iff u 2 P .
Let us assume that u 2 (cV) z.
If u = n for some n 2 NC then n 2 (cV) z means (cVz) n = + i.e. n 2 P because of c 2 C : occc v = z iff v = .
If u 2 (cV) z and m = juj > 1 then for x0 = z, we have xk+1 = (cVxk)(u k) 2
cV whenever k = 0; : : : ; m 2 and (cVxm 1)(u(m 1)) = +. In other words,
hu k; xki 2= V where k = 0; : : : ; m 2 and hu(m 1); xm 1i 2 V.
Thus, u0::k 2= P for any 0 < k m 1 but there exists v 2 NC such that
vu(m 1) 2 P and c 2 C : occc v = c 2 C : occc u0::m 1. But the condition
vu(m 1) 2 P implies v0::l 2= P for any 0 < l jvj due to P is a prefix free set.
Thus, condition (
Now assume u 2 P and m = juj.
Then we have u0::k 2= P for any k such that 0 < k < m and hu(m 1); c 2
C : occc u0::m 1i 2 V due to the definition of V. One can conclude that huk; c 2
C : occc u0::ki 2= V for any 0 k < m 1. Indeed, otherwise there exists 0 k <
m 1 and v 2 NC such that v(uk) 2 P and c 2 C:occc v = c 2 C:occc u0::k.
But condition (
NC and x 2 cV then P = (cV0) z 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 2= P , u00::m; u000::k 2= n 1 P for all 0 < m ju0j and 0 < k ju00j, and occc u0 = occc u00 for any c 2 C then nu00::m 2= P and nu000::k 2= P . Theorem 1 ensures (nu0)v 2 P and (nu00)v 2 P are equivalent for any v 2 NC+ i.e. u0v 2 n 1 P and u00v 2 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 = fc1+; c1 ; : : : ; c+m; cmg for some m > 1 and define the next NC-detector q q = fc1; : : : ; cmg q = u 2 fc1; : : : ; cmg : n 2 NC :
+ 8 ufckg if n = fck g
+ >>>> for some k = 1; : : : ; m <
u0 if u = fckgu0 and n = fck g >>>:> otherfworisseome k = 1; : : : ; m Also, let us take P = (q) , and fci+gfcj+g; fcj+gfci+g 2 NC+ for any 1 i 6= j m. Then it is evident q+( ; fci+gfcj+g) 6= +, q+( ; fcj+gfci+g) 6= +, and occck fci+gfcj+g = occck fcj+gfci+g for all k = 1; : : : ; m. In other words, fci+g 2= P , fci+gfcj+g 2= P , fcj+g 2= P , fcj+gfci+g 2= P , and occck fci+gfcj+g = occck fcj+gfci+g for all k = 1; : : : ; m.
The assumption P = (cV) x for some V NC NC and x 2 cV leads to the equivalence of the statements fci+gfcj+gfci g 2 P and fcj+gfci+gfci g 2 P due to Lemma 1.
But the definition of q ensures fci+gfcj+gfci g 2= P and fcj+gfci+gfci g 2 P . This contradiction proofs that for any V NC NC and x 2 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 ck+ and ck can be interpreted as append and pop operations respectively for the kth 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
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 below 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 = fx 2 NC j hn; xi 2 Vg are recursively enumerable for all n 2 NC. This claim follows directly from the finiteness of NC. In other words, to specify a recursively enumerable set V NC NC is equivalent to specify the set fVn j n 2 NCg of recursively enumerable subsets of NC.
Due to Matiyasevich-Davis-Robinson-Putnam theorem (see, [6]), the last is equivalent to specifying for any n 2 NC a polynomial Pn such that
Vn = fx 2 NC j Pn(x; y1; : : : ; ys) = 0 for some y1; : : : ; ys 2 Ng:
Thus, any family of the species fPn 2 Z[x1; : : : ; xm; y1; : : : ; ys] j n 2 NCg where
m is the cardinal number of C and s is some positive natural number specifies
the set V NC NC as follows
(
9 y1 2 N; : : : ; ys 2 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 = fc1; c2g and consider the clock constraints specification defined as in Table 2. This specification 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
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 corresponding 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 simulating the counter-based detector with the defining set specified by polynomials fPn(x1; : : : ; xm; y1; : : : ; ys) j n 2 NCg under assumption that the clock set is enumerated as follows C = fc1; : : : ; cmg. Also, we choose some algorithm enumerating 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 counterbased detectors with specifying its composite structure (see Fig. 1). The simulator 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 channel and writing the corresponding data items using the interface of component NotificationLog in accordance with the next algorithm.
NotificationListener:
(
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 reasonable 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 complexity of their components? These questions define the directions of our future research.