Clock Constraint Speci cation Language, or CCSL, is a domainspeci c language designed to model distributed real-time systems in terms of logical time, that is of sequences of events. Typical application of CCSL is to serve as a speci cation language for veri cation of speci ed systems. In this paper we provide a sound and complete axiomatic for propositional logic over large fragment of CCSL which we call reduced CCSL, or RCCSL. This axiomatics appears to be rather simple, thus enabling e ective veri cation of RCCSL speci cations.
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 [
ever the natural question arises: to which extent can this reasoning be carried
out. Considerable e orts involving reasoning about CCSL constraints are put
fromm the standpoint of formal veri cation of MARTE models with CCSL
constraints. Usually this veri cation is carried out by transforming model into some
framework which provides a model-checking ability, for example UPAAL [
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.
- 14
As we see it, this result can be interesting in two ways. First, complete and
sound axiomatic gives way to e ective veri cation of constraint system. On the
other hand, lots of e ort are put into extending CCSL by endowing it with clock
compositions or by introducing delays, see for example [
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 rst 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
We start with a short introduction to CCSL terminology following [
Proposition 1 For a time structure (I; ; C; ), each Ic is well-ordered with ordinal type at most !, where ! is rst nite ordinal.
For an instant i of I we de ne 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 de nition which can be reformulated in an inductive way as follows { h(i) = 0, whenever i is minimal in I; 2 1 0 a - 15 3 0 b 5 4 c 3 2 1 { h(i) = max fh(j) j j < ig + 1.
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.
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 nite or in nite 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 [
Proposition 2 For a time system T = (I; ; C; ) de ne a run L(I) = (I0; C) where I0 is de ned as
I0 = f( (x); h(x)) j x 2 I)g: Then L(I) is a linear time system, and if I is linear, then L(I) = I.
symbols of binary relation S
= f ; ; ; ; #g ; 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 de ned as a triple xRy, x and y are clocks and R is a relational symbol from S . Thus, T = C S C.
a b, :(a#b) ^ a c, :(:(a#b) ^ (b 4 c _ :(a b))).
c is.
c is not an RCCSL formula, but :(a#b)^a 4
CCSL terms can be interpreted on time systems with the set of clocks C as follows: { a b , for any x 2 Ia there is y 2 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 2 Ca; {{ aa bb ,, ftohre:raeniys xan2eIxatetnhseirvee ihs :yC2a !Ib)Cwb,itthhaxt =i:s,yx; h(x), for all x 2 Ca; { a # b , x 6= y for all x 2 Ca, y 2 Cb. Notice, that not all CCSL formulas, satis able as propositional formulas, can be satis ed on time system. For example, a formula :(a a) is clearly satis able 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.
is an equivalence relation, which is congruent with respect to every other relation in S, i.e.
8 2 S8a; b; a0; b0 2 C; a a0; b b0 : a b , a0 b0; 2. and are quasiorders (i.e. re exive and transitive) sharing associated equivalence relation ; 3. a b ) b a; 4. # is irre exive and symmetrical; 5. a b; b # c ) a # c.
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.
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.
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 de ne its corresponding relation in a relation structure:
R = f(a; b) j a; b 2 C; (a; ; b) 2 Rg
For a set of propositional formulas F over T we write R j= F i all formulas in F hold under truth assignment R, and say that R comply with F . Given a time structure T we de ne R(T ) as a valuation of terms given by their interpretation on T . We say that time structure T complies with F , denoted T j= F , if R(T ) does.
Proposition 3 A is complete i 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 propositional 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. Our rst goal is to eliminate relations and #. We say that relational structure R is clari ed if is an equivalence relation. We say that time structure is clari ed if its relational structure is.
{ Re = f([a] 0 ; ; [b] 0 ) j a; b 2 C0; 2 S; (a; ; b) 2 R0g.
The fact that 0 is a congruence guarantees that the de nition of Re is consistent. Obviously, Re is clari ed for any R0. Let us now de ne simpli ed axiom system Ae, which de nes axiomatics for clari ed 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.
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. De ne time system T with clocks CA such that IaT = I[Ta0] . Now it is a trivial fact to check that T is a model for RA.
deduce that Indeed a contradiction.
as well, i.e. if 9c : 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.
Next, by extension of a relation structure RA we understand a relation structure RB such that RA = RBjCA . We say that relation structure is subclock-closed, i for it holds The time structure is subclock-closed i its relation structure is subclock-closed.
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. De ne a set R as:
R = fcab j a; b 2 CA; a / b; :a#b; : (9c : c a; c b)g:
CB = CA [ R: Now we need to de ne 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 rst case we simply put RBjCA = RA, which automatically assures that RB is an extension of RA.
cab 4 cde , cab = cde; cab
cde , cab = cde; cab#cde , cab 6= cde: Finally, when elements are from di erent sets, put: 8a; b; c : cab 64 d; d 6 cab and
d , a d 4 cab , d 4 a or d 4 b; cab d or b d; cab#d , d#cab , :cab d , a 6 d and b 6 d
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: b) a; b 2 CA; :a#b; : (9c 2 CA : c
a; c a 2 CA; cde 2 R; :a#cde ) cde cab; cde 2 R; :cab#cde ) cab = cde: b) ) 9c = cab 2 CB : c a; a; c b
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 2 CA, in which case the transitivity is trivial, or a = cb;d 2 R; e; f 2
e 4 cb;d , e 4 b or e 4 d ) f 4 b or f 4 d , f 4 cb;d: The re exivity and the fact that associated equivalence relation is an equity are trivial. The proof for is similar. 2. a b ) b a: 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 9d : d a; d c. But then d a b and so :b # c, a contradiction.
Axiomatics A3 (AF ) 1. 2. a and b ) b are partial orders;
a; then Theorem 1 together with Lemmas 1 and 2 yield the following corollary Corollary 1 If every subclock-closed relational structure compliant with AF can be realized by clari ed 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 hypothesis of the corollary there is subclock-closed time system TF such that RF = R(TF ).
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
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 = jCj. 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 2. Ti=1:::p i =4
Next, de ne function f : C ! N+ as: 8 1 > f (x) = <
X >: y4x;y6=x
8y 6= x : y 64 x f (y) otherwise It is clear that, although this de nition 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 de ned via elements of height 1, etc., see Figure 4 below.
1 2 5 1
1
(l1 +
+ lp) elements:
I = f(i; c; j) j i = 1 : : : p; c 2 C; j = 1 : : : li f (c)g with order given by 2 i < q (i; c; j) (q; d; r) , 64 i = q; c > i d i = q; c = d; j r So this order is "almost" lexicographic, except that the second letter is each time ordered di erently, depending of the rst one.
cT = f(i; d; j) 2 I j d cg :
satis es 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 2 C; a 4 b. Then for each i we have a h : aT ! bT as: h(i; x; j) = (i; b; ga(i; x; j)) i b. De ne the function where ga(i; x; j) = f(i; x0; j0) 2 aT j (i; x0; j0) (i; x; j)g :
ga(i; x; j) li f (b), but indeed: ga(i; x; j) = f(i; x0; j0) 2 aT j (i; x0; j0) (i; x; j)g f(i; x0; j0) 2 aT g =
X f (x0) li x0 a
X x04b;x06=b
X f (x0) li x04a f (x0) li = li f (b):
aT follows x 4 a 4 b, and 8w : (i; x; j) > (i; b; w) yields h(i; x; j) (i; x; j).
T :
a 6 k b , b k a: If a 4T b then there is an increasing function h : aT ! bT such that 8w : 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
f(i; x; j) 2 bT j (i; x; j) < (k; a; f (a) lk)g = f(i; x; j) 2 bT j (i; x; j) < (k; a; 1)g f(k; x; j) 2 bT j (k; x; j) < (k; a; 1)g + f(i; x; j) 2 bT j i <= k
1g = 0 + F (l1 + + lk 1) = lk
1; f(k; x; j) 2 bT j a k x k bg + f(i; x; j) 2 I j i <= k 1g a contradiction.
Corollary 2 Every subclock-closed relational structure compliant with AF can be realized by clari ed subclock-closed time system
Theorem 3 Axiom system A0 is complete and sound axiom system with time systems as its models.
Statement 1 Axiom system A0 is complete and sound axiom system with runs as its models.
Statement 2 Axiom system A0 has nite model property. 6
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 de ne canonical clock constraints that would be essential from theoretical perspective. As an example, this paper shows that when arguing about clock constrains, coincidence 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.
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.