=Paper=
{{Paper
|id=Vol-1614/paper_61
|storemode=property
|title=A Complete Axiomatization for Reduced Clock Constraint Specification Language
|pdfUrl=https://ceur-ws.org/Vol-1614/paper_61.pdf
|volume=Vol-1614
|authors=Bogdan Chornomaz, Kirill Rukkas,Kseniia Troino
|dblpUrl=https://dblp.org/rec/conf/icteri/ChornomazRT16
}}
==A Complete Axiomatization for Reduced Clock Constraint Specification Language==
https://ceur-ws.org/Vol-1614/paper_61.pdf
A Complete Axiomatization for Reduced Clock
Constraint Specification Language
Bogdan Chornomaz, Kirill Rukkas, and Kseniia Troino
Department of Computer Science,
Kharkiv National University
Abstract. Clock Constraint Specification Language, or CCSL, is a domain-
specific language designed to model distributed real-time systems in
terms of logical time, that is of sequences of events. Typical applica-
tion of CCSL is to serve as a specification language for verification of
specified systems.
In this paper we provide a sound and complete axiomatic for proposi-
tional logic over large fragment of CCSL which we call reduced CCSL,
or RCCSL. This axiomatics appears to be rather simple, thus enabling
effective verification of RCCSL specifications.
Keywords: time model, verification model, propositional logic, com-
pleteness model, specification language
Key terms: Computation, FormalMethod, SpecificationProcess, Math-
ematicalModel, DistributedSystem
1 Introduction
Models dealing with discrete logical time rather than with real-valued “physical
time” are well known to computer science, one classical example being Lamport’s
algorithm for distributed clock synchronization [2]. In this paper we study model
called Clock Constraint Specification Language (CCSL), proposed by F. Mallet
in his dissertation [3]. Initially developed as UML profile for MARTE, CCSL
later become domain-specific language on its own.
Constraints developed with CCSL allow some obvious logical reasoning, how-
ever the natural question arises: to which extent can this reasoning be carried
out. Considerable efforts involving reasoning about CCSL constraints are put
fromm the standpoint of formal verification of MARTE models with CCSL con-
straints. Usually this verification is carried out by transforming model into some
framework which provides a model-checking ability, for example UPAAL [5] or
Fiacre [1].
We take a different approach, having in mind a rather theoretical goal. We
restrict ourselves with a fragment of CCSL called Reduced CCSL (RCCSL), for
which we provide sound and complete system of axioms for propositional logic
over it. The question of constructing such axiomatics for CCSL itself remains
open.
ICTERI 2016, Kyiv, Ukraine, June 21-24, 2016
Copyright © 2016 by the paper authors
- 14 -
As we see it, this result can be interesting in two ways. First, complete and
sound axiomatic gives way to effective verification of constraint system. On the
other hand, lots of effort are put into extending CCSL by endowing it with clock
compositions or by introducing delays, see for example [4]. These attempts reveal
a demand for deeper understanding of which elementary dependencies between
clock can exist and which expressive power do they bring about. The language
of logic which we utilize here can be exceptionally well suited for answering such
questions.
The structure of the paper is as follows: In Section 2 we introduce basic
terminology from CCSL and from logic background. In Section 3 we introduce
axiomatics which, as we argue later, is a complete and sound axiomatics for
modeling time systems with RCCSL. In Section 4 we take first preliminary steps
towards the proof of completeness. Section 5 contains the most essential part
of the paper, providing the central part of the proof of completeness. Section 6
concludes the paper.
2 CCSL and RCCSL
We start with a short introduction to CCSL terminology following [6]. We define
time structure as a tuple (I, ≤, C, π) where I is at most countable set of instants,
C is a finite set of clocks, ≤ is a preorder on I such that (x] is finite for all x ∈ I,
where (x] is a principal preorder-ideal of x, that is
(x] = {y | y ≤ x};
finally, π is a function π : I 7→ C, mapping each instant into corresponding clock,
such that for every c ∈ C each preimage Ic = π −1 (c) is linearly ordered and
.
nonempty. We denote an equivalence relation corresponding to ≤ by =, that is,
.
x = y if x ≤ y and y ≤ x.
Thus defined, clock systems models a situation when we are given a set
of clocks, each producing signals for which we only know their relative order of
appearance. Signals in different clocks may be incomparable, or, on the contrary,
may happen simultaneously. Proposition 1 in [6] can clarify this parallel.
Proposition 1 For a time structure (I, ≤, C, π), each Ic is well-ordered with
ordinal type at most ω, where ω is first finite ordinal.
In order to visualize time system we use a modified version of Hasse diagram,
see Figure 1 below. Vertical lines depicts instants of corresponding clocks, slanted
lines between clocks depict covering relation of ≤, finally instants equivalent with
respect to ≤ are connected by horizontal lines.
For an instant i of I we define height h(i) of i as the length of the largest
increasing chain in I, ending in i minus one. This is a standard order-theoretic
definition which can be reformulated in an inductive way as follows
– h(i) = 0, whenever i is minimal in I;
- 15 -
5
2
4
3
3
2
1
1
0
0
a b c
Fig. 1. Example of Hasse diagram depicting a time structure with clocks a, b and c.
– h(i) = max {h(j) | j < i} + 1.
Heights of instants are also depicted on Figure 1 below
We say that time system is linear if ≤ is a linear quasi-order, that is ≤
becomes a linear order after factorization by corresponding equivalence relation.
When depicting a linear time system, we will omit slanted and horizontal lines
on Hasse diagram, the order between instants in this case is represented solely
by their relative height.
We define run as a time system with the set I defined as a custom subset of
C × N, with π(a, k) = a and (a, k) ≤ (b, l) if and only if k ≤ l, for all (a, k) and
(b, l) in C × N. In a run every set Ic can be treated as a finite or infinite sequence
of natural numbers. Trivially, every run is a linear time system. On the other
hand, every time system can be considered a run, as stated in the Proposition 2
below, we refer to [6] for proof.
Proposition 2 For a time system T = (I, ≤, C, π) define a run L(I) = (I 0 , C)
where I 0 is defined as
I 0 = {(π(x), h(x)) | x ∈ I)}.
Then L(I) is a linear time system, and if I is linear, then L(I) ∼
= I.
Let us fix a potentially infinite set of clocks C and a set S∗ of binary relation
symbols
S ∗ = {≡, ≺, , ⊆, #} ,
called coincidence, precedence, cause, subclocking and exclusion correspondingly.
Now we introduce CCSL as a propositional language over a set T of terms, where
each term is defined as a triple xRy, x and y are clocks and R is a relational
symbol from S ∗ . Thus, T = C × S × C.
Thus, examples of terms are: a ≡ b, a#a or b ≺ d; and CCSL formulas are:
a ≡ b, ¬(a#b) ∧ a ≺ c, ¬(¬(a#b) ∧ (b 4 c ∨ ¬(a ≡ b))).
- 16 -
Reduced CCSL, or RCCSL, is defined in a similar way, by excluding prece-
dence from the set of possible relational symbols. That is, wee fix
S = {≡, , ⊆, #} .
In the example above, ¬(a#b)∧a ≺ c is not an RCCSL formula, but ¬(a#b)∧a 4
c is.
CCSL terms can be interpreted on time systems with the set of clocks C as
follows:
.
– a ≡ b ⇔ for any x ∈ Ia there is y ∈ Ib ) with x = y and vice versa;
– a ≺ b ⇔ there is a strict extensive h : Ca → Cb , that is, x < h(x), for all
x ∈ Ca ;
– a b ⇔ there is an extensive h : Ca → Cb , that is, x ≤ h(x), for all x ∈ Ca ;
.
– a ⊆ b ⇔ for any x ∈ Ia there is y ∈ Ib ) with x = y ;
.
– a # b ⇔ x 6= y for all x ∈ Ca , y ∈ Cb .
Figure 2 illustrates the interpretation of CCSL terms on time systems.
a≡b a≺b ab a⊆b a#b
Fig. 2. Cause and subclocking relation on clocks a and b
After we interpret all CCSL terms, the interpretation of CCSL formulas on
time systems is straightforward. For example, time system on Figure 1 satisfies
formula (a ≺ b) ∧ (¬(b#c) ∨ ¬(a#c)).
3 Axiomatics
Notice, that not all CCSL formulas, satisfiable as propositional formulas, can be
satisfied on time system. For example, a formula ¬(a ≡ a) is clearly satisfiable
if we put (a ≡ a) = F alse. On the other hand, this formula can hold on no time
structure. In fact, the following formulas, which we call axioms, hold on any time
structure.
- 17 -
Axiomatics A1 (A0 )
1. ≡ is an equivalence relation, which is congruent with respect to every
other relation in S, i.e.
∀∗ ∈ S∀a, b, a0 , b0 ∈ C, a ≡ a0 , b ≡ b0 : a ∗ b ⇔ a0 ∗ b0 ;
2. and ⊆ are quasiorders (i.e. reflexive and transitive) sharing associ-
ated equivalence relation ≡;
3. a ⊆ b ⇒ b a;
4. # is irreflexive and symmetrical;
5. a ⊆ b, b # c ⇒ a # c.
We say that a CCSL formula is valid if it holds under any interpretation
on time structures. We say that an axiomatics is sound if all its axioms are
valid formulas. Similarly, we call axiomatics complete, if any valid formula can
be inferred from it. Throughout the paper, we consider all propositional axioms
and propositional inference rules over CCSL terms to hold.
We denote Axiomatics A1 by A0 and refer to [6] for its soundness. In fact,
in the following two sections we will show that this axiom set is also complete.
Each of the axioms in A0 is not a singular propositional axiom, but rather a set
of axioms, described in generally used terminology.
Define relation structure as a pair (C, R), where R is a subset in T , which we
treat as a valuation on a set of CCSL terms on C. Usually we will write relation
structure simply as R. For each relation symbol ∗ we define its corresponding
relation in a relation structure:
∗R = {(a, b) | a, b ∈ C; (a, ∗, b) ∈ R}
For a set of propositional formulas F over T we write R |= F iff all formulas
in F hold under truth assignment R, and say that R comply with F . Given a time
structure T we define R(T ) as a valuation of terms given by their interpretation
on T . We say that time structure T complies with F , denoted T |= F , if R(T )
does.
Using completeness of propositional logic we infer following general fact,
which is essential for our proof of completeness
Proposition 3 A is complete iff there is a model for a relation structure R
whenever R complies with A.
Proof. (⇒) : Let R comply with A but does not have a model. Let FR be a
propositional formula which holds only for R. As there is no model for R, ¬FR
is a valid formula and thus A ` ¬FR . By propositional inference rules this is
equivalent to the formula ¬A ∨ ¬FR being propositionally valid, but it does not
hold on R, a contradiction.
(⇐) : Let F be a valid formula not inferred from A. Then there is a proposi-
tional structure R such that R complies with A but not with F . By assumption,
there is a time structure T with R(T ) = R. But then F does not hold on T ,
which means F is not valid, a contradiction.
- 18 -
4 Completeness: preliminary reduction
Our first goal is to eliminate relations ≡ and #. We say that relational structure
R is clarified if ≡ is an equivalence relation. We say that time structure is clarified
if its relational structure is.
For a relational structure (C0 , R0 ) we define its factorization as a relational
structure (Ce , Re ), denoted (Ce , Re ) = (C0 ,R0 )/≡0 , such that:
– Ce is a set of equivalence classes of C0 by ≡0 ;
– Re = {([a]≡0 , ∗, [b]≡0 ) | a, b ∈ C0 , ∗ ∈ S; (a, ∗, b) ∈ R0 }.
The fact that ≡0 is a congruence guarantees that the definition of Re is consis-
tent. Obviously, Re is clarified for any R0 . Let us now define simplified axiom
system Ae , which defines axiomatics for clarified time systems.
Axiomatics A2 (Ae )
1. ≡ is an equity;
2. and ⊆ are partial orders;
3 - 5. same as in A0
To justify passing from A0 to Ae let us prove the following two easy lemmas:
Lemma 1 If a relational model RA complies with A0 then RA/≡A complies
with Ae .
Proof.Obvious.
Lemma 2 Given a relational model RA , if there is model for RA/≡A then there
is model for RA .
Proof. Let C be clocks of RA/≡A and let T 0 be a model for RA/≡A . Then clocks
from C are equivalence classes of clocks from CA . Define time system T with
T0
clocks CA such that IaT = I[a] . Now it is a trivial fact to check that T is a model
for RA .
As our next step we relax restrictions on # relation. From Ae we can easily
deduce that
∃c : c ⊆ a, c ⊆ b ⇒ ¬a#b.
Indeed
a#b, c ⊆ a, c ⊆ b ⇒ c#b, c ⊆ b ⇒ c#c,
a contradiction.
It would be convenient for us if this implication would work the other way
as well, i.e. if ∃c : c ⊆ a, c ⊆ b ⇔ ¬a#b. However it is easy to construct a
counterexample to this statement, on the other hand, it is always possible to
”extend” the temporal structure by adding a clock (or several), so that it become
true, see Figure 3 below:
We want to make the same trick, but with relation structures rather than
with temporal structures.
- 19 -
extending
a b a b c
¬a#b ¬a#b
¬(∃c : c⊆a,c⊆b) ∃c : c⊆a,c⊆b
Fig. 3. Extension of a temporal structure
For a relation structure (CA , RA ) and a set of clocks CB ⊆ CA by restriction of
relation structure RA to CB , denoted RA |CB , we understand a relation structure
(CB , RB ), where: \
RB = RA CB × S × CB .
Next, by extension of a relation structure RA we understand a relation struc-
ture RB such that RA = RB |CA . We say that relation structure is subclock-closed,
iff for it holds
∃c : c ⊆ a, c ⊆ b ⇔ ¬a#b (S)
The time structure is subclock-closed iff its relation structure is subclock-closed.
Theorem 1 allows us to consider only subclock-closed relation structures:
Theorem 1 For each relation structure satisfying Ae there is a subclock-closed
extension satisfying Ae .
Proof. Take a non subclock-closed relation structure RA satisfying Ae . Let /
be some strict linear order on the set CA . Define a set R as:
R = {cab | a, b ∈ CA , a / b; ¬a#b, ¬ (∃c : c ⊆ a, c ⊆ b)}.
Define the set of clocks CB of our to-be-constructed system as:
CB = CA ∪ R.
Now we need to define relations RB in three cases: for pair of old clocks, for pair
of new clocks and for a pair of an old and a new clock. In the first case we simply
put RB |CA = RA , which automatically assures that RB is an extension of RA .
In case of two elements from R we put:
cab 4 cde ⇔ cab = cde ;
cab ⊆ cde ⇔ cab = cde ;
cab #cde ⇔ cab 6= cde .
- 20 -
Finally, when elements are from different sets, put:
∀a, b, c : cab 64 d, d 6⊆ cab
and
d 4 cab ⇔ d 4 a or d 4 b;
cab ⊆ d ⇔ a ⊆ d or b ⊆ d;
cab #d ⇔ d#cab ⇔ ¬cab ⊆ d ⇔ a 6⊆ d and b 6⊆ d
Generally, for a pair of clocks a, b from CA such that ¬a#b, ¬ (∃c ∈ CA : c ⊆ a, c ⊆ b)
by cab we understand element cab in case when a/b and element cba in case when
b / a.
Observe, that RB is subclock-closed, indeed:
a, b ∈ CA , ¬a#b, ¬ (∃c ∈ CA : c ⊆ a, c ⊆ b) ⇒ ∃c = cab ∈ CB : c ⊆ a, c ⊆ b
a ∈ CA , cde ∈ R, ¬a#cde ⇒ cde ⊆ a;
cab , cde ∈ R, ¬cab #cde ⇒ cab = cde .
So what is left to check is that RB satisfy Ae , let us do it.
1. and ⊆ are partial orders:
Check the transitivity of : if f 4 e 4 a, a 6= e, e 6= f then, as all elements
in R are not larger than any element of CA , we have two possibilities: either
a, e, f ∈ CA , in which case the transitivity is trivial, or a = cb,d ∈ R, e, f ∈
CA , but then:
e 4 cb,d ⇔ e 4 b or e 4 d ⇒ f 4 b or f 4 d ⇔ f 4 cb,d .
The reflexivity and the fact that associated equivalence relation is an equity
are trivial. The proof for ⊆ is similar.
2. a ⊆ b ⇒ b a: obvious.
3. # is irreflexive and symmetrical: obvious.
4. a ⊆ b, b # c ⇒ a # c:
follows from the fact that RB is subclock-closed and that ⊆ is a partial order,
indeed let ¬a#c then ∃d : d ⊆ a, d ⊆ c. But then d ⊆ a ⊆ b and so ¬b # c, a
contradiction.
Now, if we fix axiom system AF , which is a proper subset of Ae ,
Axiomatics A3 (AF )
1. and ⊆ are partial orders;
2. a ⊆ b ⇒ b a;
then Theorem 1 together with Lemmas 1 and 2 yield the following corollary
- 21 -
Corollary 1 If every subclock-closed relational structure compliant with AF can
be realized by clarified subclock-closed time system, then every relational structure
compliant with A0 can be realized by some time system.
Proof. Let R be a relational structure compliant with A0 . Then by Lemma 1
RE = R/≡ is compliant with Ae . Take a subclock-closed extension RF of RE ,
which exists by Theorem 1. Now RF satisfy Ae and thus AF and by the hy-
pothesis of the corollary there is subclock-closed time system TF such that RF =
R(TF ).
Notice that while R(TF ) contains only interpretations of formulas with 4
and ⊆, by S it can be extended in a straightforward fashion to formulas with #
and ≡. Thus, TF restricted to CF is a model for RF . The claim of the corollary
now follows by Lemma 2.
5 Completeness: modelling ⊆ and 4
Theorem 2 Take a set of clocks C and a pair of partial orders 4 and ⊆ on it,
such that a ⊆ b ⇒ b 4 a. Then there is a subclock-closed time structure T over
the same clocks such that ⊆T =⊆ and 4T =4.
Proof. Let n = |C|. Fix some linear order / on C and denote by ci the i-th clock
in C relative to this order. Fix p linear orders π1 . . . πn on C so that
1. T
each πi is an extension of 4;
2. i=1...p πi =4
Clearly, such orders can be found and p can always be chosen so that p ≤ n.
Next, define function f : C → N+ as:
1
∀y 6= x : y 64 x
f (x) =
X
f (y) otherwise
y4x,y6=x
It is clear that, although this definition is ”recursive”, the recursion is only
seeming: for bottom elements with regards to 4, i.e. for elements of height 1,
the sum is empty, and so f equals 1; for elements of height 2 f is defined via
elements of height 1, etc., see Figure 4 below.
5
2
1
1 1
Fig. 4. Function f recursively defined for a partial order 4
- 22 -
P
Let F = x f (x). Choose l1 , . . . , lp ∈ N as:
l1 = 1;
li = F ∗ (l1 + · · · + li−1 ) + 1.
Or, using a direct formula:
i−1
li = (F + 1) .
Now, define I to be the chain with F ∗ (l1 + · · · + lp ) elements:
I = {(i, c, j) | i = 1 . . . p; c ∈ C; j = 1 . . . li ∗ f (c)}
with order given by
iπi d
i = q, c = d, j ≤ r
So this order is ”almost” lexicographic, except that the second letter is each time
ordered differently, depending of the first one.
Define clock cT in T as:
cT = {(i, d, j) ∈ I | d ⊆ c} .
We claim that thus defined time structure T satisfies the requirements of the
theorem.
From the definition of cT it is obvious that T is subclock-closed, and that it
satisfies ⊆T =⊆. The nontrivial part is to show that T = , which we will do
now by separately showing that T ⊆ and ⊆ T .
1. T ⊆ :
Let a, b ∈ C, a 4 b. Then for each i we have a ≤πi b. Define the function
h : aT → bT as:
h(i, x, j) = (i, b, ga (i, x, j))
where
ga (i, x, j) = {(i, x0 , j 0 ) ∈ aT | (i, x0 , j 0 ) ≤ (i, x, j)} .
Observe, that to assure that h is correctly defined, we must check that
ga (i, x, j) ≤ li ∗ f (b), but indeed:
ga (i, x, j) = {(i, x0 , j 0 ) ∈ aT | (i, x0 , j 0 ) ≤ (i, x, j)}
≤ {(i, x0 , j 0 ) ∈ aT }
X X
= f (x0 ) ∗ li ≤ f (x0 ) ∗ li
x0 ⊆a x0 4a
X
≤ f (x0 ) ∗ li = li ∗ f (b).
x0 4b,x0 6=b
So h is defined correctly, it is obviously strictly increasing and from (i, x, j) ∈
aT follows x 4 a 4 b, and ∀w : (i, x, j) > (i, b, w) yields h(i, x, j) ≤ (i, x, j).
- 23 -
2. ⊆ T :
Take a, b ∈ C, a 64 b, and take k so that
a 6≤πk b ⇔ b ≤πk a.
If a 4T b then there is an increasing function h : aT → bT such that
∀w : h(w) ≤ w. Observe that f (a) ∗ lk elements represented as (k, a, u) do
not belong to bT , from which we conclude:
f (a) ∗ lk ≤ {(i, x, j) ∈ bT | (i, x, j) < (k, a, f (a) ∗ lk )}
= {(i, x, j) ∈ bT | (i, x, j) < (k, a, 1)}
≤ {(k, x, j) ∈ bT | (k, x, j) < (k, a, 1)}
+ {(i, x, j) ∈ bT | i <= k − 1}
≤ {(k, x, j) ∈ bT | a ≤πk x ≤πk b} + {(i, x, j) ∈ I | i <= k − 1}
= 0 + F ∗ (l1 + · · · + lk−1 ) = lk − 1,
a contradiction.
Corollary 2 Every subclock-closed relational structure compliant with AF can
be realized by clarified subclock-closed time system
Combining Corollaries 1, 2 and Proposition 3 we obtain
Theorem 3 Axiom system A0 is complete and sound axiom system with time
systems as its models.
As a spin-off, let us notice that time system constructed in Theorem ?? is a
run and is finite. These properties are also preserved by extension in Theorem 1
and by factorization in Lemma 1. Thus, we have the following propositions.
Statement 1 Axiom system A0 is complete and sound axiom system with runs
as its models.
Statement 2 Axiom system A0 has finite model property.
6 Conclusion and future work
We had constructed sound and complete axiomatics for propositional logic over
RCCSL, with completeness being the nontrivial part of this construction. We
hope that the proposed model-theoretical approach would help to define canon-
ical clock constraints that would be essential from theoretical perspective. As
- 24 -
an example, this paper shows that when arguing about clock constrains, coinci-
dence could be easily removed from consideration, which is obvious. What is not
so obvious is that arguing about exclusion could be replaced by arguing about
subclocking.
Natural question that arises from this perspective is to extend our result to
wider fragments of logic over CCSL, we formulate it as a series of problems.
Problem 1 What is the complete and sound system of axioms for propositional
logic over CCSL.
Problem 2 What is the complete and sound system of axioms for propositional
logic over CCSL with clock compositions.
Problem 3 What is the complete and sound system of axioms for propositional
logic over CCSL with delays.
Our preliminary research shows that axiom system for complete CCSL might
be much more complicated than the one for RCCSL. On the other hand, aug-
menting CCSL with composition might quite naturally fall into our approach of
extending time systems.
References
1. Dhaussy, P., Menad, M.: A transformation approach for multiform time require-
ments. Software Engineering and Formal Methods, volume 8137 of Lecture Notes
in Computer Science, 1630, (2013) Commun. ACM, 21(7):558565, 1978.
2. Lamport, L.: Time, clocks, and the ordering of events in a distributed system.
Commun. ACM, 21(7):558565, 1978.
3. Mallet, F.: Logical Time @ Work for the Modeling and Analysis of Embedded Sys-
tems, Habilitation thesis. LAMBERT Academic Publishing (2011).
4. Mallet, F., Millo J.-V., Romenska, Y.: State-based representation of CCSL opera-
tors. Research Report RR-8334, INRIA (2013).
5. Mallet, F., Petterson, P., Seceleanu, C., Suryadevara, J.: Verifying MARTE/CCSL
mode behaviors using UPPAAL. Software Engineering and Formal Methods, volume
8137 of Lecture Notes in Computer Science, 115, (2013)
6. Mallet, F.,Zaretska, I., Zholtkevych, G., Zholtkevych, G.: Clocks Model for Spec-
ification and Analysis of Timing in Real-Time Embedded Systems. ICTERI:475-
489 (2013)