Product Interval Automata: A Subclass of Timed Automata

Deepak D’Souza^{⋆} and P. S. Thiagarajan^{⋆}^{†}

Chennai Mathematical Institute, 92 G. N. Chetty Road, Chennai 600 017, India.

                        {deepak,pst}@smi.ernet.in

Abstract. We identify a subclass of timed automata and develop its theory. These automata, called product interval automata, consist of a network of timed agents. The key restriction is that there is just one clock for each agent and the way the clocks are read and reset is determined by the distribution of shared actions across the agents. We show that the resulting automata admit a clean theory in both logical and languagetheoretic terms. It turns out that the study of these timed automata can exploit the rich theory of partial orders known as Mazurkiewicz traces. An important consequence is that the partial order reduction techniques being developed for timed automata [4, 10] can be readily applied to the verification tasks associated with our automata. Indeed we expect this to be the case even for the extension of product interval automata called distributed interval automata.

1 Introduction

Timed automata as formulated by Alur and Dill [1] have become a standard model for describing timed behaviours. These automata are very powerful in language-theoretic terms. Their languages are not closed under complementation. Further, their language inclusion problem is undecidable and hence cannot be reduced to the emptiness problem which is decidable. Hence in order to solve verification problems posed as language inclusion problems, one must use deterministic timed automata for specifications (which can be easily complemented) or one must work with a restricted class of timed automata that possess the desired closure properties.

Here we follow the second route and propose a subclass of timed automata called product interval automata (PI automata). Roughly speaking, such an automaton will consist of a network of timed agents ∥_{i=1}^{K} A_{i} where each A_{i} will operate over an alphabet Σ_{i} of events. Further, there will be a single clock c_{i} associated with each agent i. The agents communicate by synchronising on the timed executions of common events. Suppose a is an event in which the agents {1, 3, 4} participate. Then the timing constraint governing each a-execution will

⋆ A part of this work has been supported by BRICS, Computer Science Dept., Aarhus University. † A part of this work has been supported by the IFCPAR Project 1502-1.

only involve the clocks {c_{1}, c_{3}, c_{4}}. Moreover, the set of clocks that is reset at the end of each a-execution will be {c_{1}, c_{3}, c_{4}}. Thus the distribution Σ̃ = {Σ_{i}}_{i=1}^{K} of events over the agents will canonically determine the usage of clocks; so much so, we can avoid mentioning the clocks altogether once we fix Σ̃.

This method of structuring timed automata has a number of advantages. In particular, one can provide naturally decomposed and succinct presentations of timed automata with large (control) state spaces. Admittedly, the technique of presenting a global timed automaton as a product of component timed automata has been used by many authors starting from [1]. What is new here, as explained above, is that our decomposed presentation places a corresponding restriction on the manner in which clocks are read and reset. It is worth pointing out that the model considered by Yi and Jonsson [24] in the framework of timed CSP can be easily represented as PI automata. Their main result, in our terms, is that language inclusion problem for PI automata is decidable. We establish a variety of results concerning PI automata which subsume the decidability of the language inclusion problem.

In principle, one could view our automata as a restricted kind of labelled timed Petri net. However the semantics we attach to our automata is the standard one for timed automata whereas the semantics one uses for timed Petri nets – with earliest and latest firing times for the transitions – is somewhat different.

A key feature of our automata is that their timed behaviour can be symbolically represented without any loss of information by conventional words. As a consequence, it turns out that their theory can be developed with the help of powerful results available in the theory of Mazurkiewicz traces [6]. We wish to emphasise, our automata will however have a conventional timed semantics with the non-negative reals serving as the time frame. A final aspect of PI automata that we wish to mention is that partial order reduction techniques that are under development [4, 10] can be readily applied to our automata.

In pragmatic terms, it is not clear how much modelling power is lost through the restrictions we place on the usage of clocks. In many multi-agent timed systems it seems sufficient to have just one clock for each agent. For instance, a network of timed automata that communicate through shared variables is used to model and analyse the timed behaviour of asynchronous circuits by Maler and Pnueli [17]. It turns out that product interval automata suffice to represent the same class of timed behaviours.

From a theoretical standpoint, PI automata are strictly less expressive than event clock automata due to Alur, Fix, and Henzinger [2] and their state-based version [19] which in turn are strictly less powerful than general timed automata. As a result, the logics we develop here will also be strictly less expressive than the corresponding logics presented in [14] for a generalisation of event recording automata called recursive event recording automata. Nevertheless we feel that PI automata are of independent interest due to the reasons sketched earlier. For basic information about timed automata and their logics we cite the surveys [3, 13] and their references. An interesting early instance of timed languages which have nice closure properties and which admit a clean logical characterisation can be found in [22].

In the next section we define PI automata. In section 3 we show that these automata (more precisely their languages) are closed under boolean operations. In section 4 we first present a monadic second order logic denoted TMSO^{⊗} to capture the timed regular languages recognised by PI automata. We then formulate a linear time temporal logic denoted TLTL^{⊗} and sketch automatatheoretic solutions to the satisfiability and model checking problems for TLTL^{⊗} in terms of PI automata.

As we point out in the final section, all our ideas can be extended smoothly to a larger setting in which the underlying “symbolic” automata are asynchronous Büchi automata [11]. The resulting timed automata are called distributed interval automata and they can also be studied using techniques taken from trace theory. It is the case that PI automata are less expressive than distributed interval automata which in turn are less expressive than event recording automata [2]. It turns out that the so called cellular version of distributed interval automata correspond to event recording automata. All these extensions as well detailed proofs of all the results presented below are available in the full paper [7].

2 Product Interval Automata

We fix a finite set of agents P = {1, 2, …, K} and let i, j range over P. A P-distributed alphabet is a family Σ̃ = {Σ_{i}}_{i∈P} where each Σ_{i} is a finite set of actions. We set Σ = ⋃_{i∈P} Σ_{i} and call it the global alphabet induced by Σ̃. We let a, b range over Σ. The set of agents that participate in each occurrence of the action a is denoted by loc(a) and is given by: loc(a) = {i | a ∈ Σ_{i}}. Through the rest of the paper we fix such a P-distributed alphabet Σ̃.

We let ℝ^{>0} and ℝ^{≥0} denote the set of positive and non-negative reals respectively. Without loss of generality we will use intervals with rational bounds to specify timing constraints (and use ∞ as the upper bound to capture unbounded intervals). If an interval is of the form [x, y) or [x, y] we require x to be a positive rational and if an interval is of the form (x, y] or [x, y] we require y to be a positive rational. An interval defines a subset of reals in the obvious way. Let INT be the set of all intervals of ℝ^{>0}.

A product interval automaton over Σ̃ is a structure ({A_{i}}_{i∈P}, Q_{in}), where for each i, A_{i} is a structure (Q_{i}, ⟶_{i}, F_{i}, G_{i}) such that Q_{i} is a finite set of states, ⟶_{i}, the transition relation, is a finite subset of Q_{i} × (Σ_{i} × INT ) × Q_{i}, and F_{i}, G_{i} ⊆ Q_{i} are, respectively, finitary and infinitary acceptance state sets. Q_{in} ⊆ Q = Q_{1} × ⋯ × Q_{K} is a set of global start states.

For convenience we will be interested only in infinite runs of a PI automaton. However in such a run some of the component automata may execute only a finite number of actions. It is for this reason we have two types of accepting states for each component automaton.

In what follows, for an alphabet A we will use A^{∗} and A^{ω} to denote the set of finite and infinite words over A respectively, and let A^{∞} denote the set A^{∗} ∪ A^{ω}.

For a word σ in A^{∞}, we let prf (σ) be the set of finite prefixes of σ. A timed word σ over Σ̃ is an element of (Σ × ℝ^{>0})^{∞} such that:

(i) σ is non-decreasing: if τ(a, t)(b, t′) is a prefix of σ then t ≤ t′. (ii) if τ(a, t)τ′(b, t′) is a prefix of σ with t = t′, then we must have loc(a)∩loc(b) =

∅. Thus, simultaneous actions are allowed but only if they are independent – i.e. their locations are disjoint.

(iii) if σ is infinite, then it must be progressive: for each t ∈ ℝ^{>0} there exists a prefix τ(a, t′) of σ such that t′ > t.

We let TΣ̃^{ω} denote the set of infinite timed words over Σ̃.

Now suppose K = 1 so that P = Σ_{1}. Then the definition above (condition (ii) will not apply) will yield the usual notion of a timed word over the alphabet Σ_{i}. With this in mind, for an alphabet A, we let TA^{∗} and TA^{ω} be the set of finite and infinite (ordinary) timed words over A, respectively, and set TA^{∞} = TA^{∗} ∪TA^{ω}.

Let σ ∈ TΣ̃^{ω}. Then σ ↾ i is the i-projection of σ. It is the timed word over Σ_{i} obtained by erasing from σ all appearances of letters of the form (a, t) with a ∉ Σ_{i}. It is easy to check that σ ↾i belongs to TΣ_{i}^{∞}.

Finally, let τ be a finite timed word over Σ̃. Then time_{i}(τ) is given inductively by: time_{i}(ϵ) = 0. Further, time_{i}(τ′(a, t)) = t if a ∈ Σ_{i}, and equals time_{i}(τ′) otherwise. Thus time_{i}(τ) is the time at which the last i-action took place during the execution of τ. This notion will play an important role in the rest of the paper. We can now define the timed language accepted by a PI automaton.

Let A = ({A_{i}}_{i∈P}, Q_{in}) be a PI automaton over Σ̃ and let σ ∈ TΣ̃^{ω}. Then a run of A over σ is a map ρ : prf (σ) → Q such that

1. ρ(ϵ) ∈ Q_{in}

2. Suppose τ(a, t) is a prefix of σ. Then for each i ∈ loc(a), there exists a

transition ρ(τ)[i] ⟶_{i}^{(a,I)} ρ(τ(a, t))[i] with (t − time_{i}(τ)) ∈ I. Further, for each i ∉ loc(a) we have ρ(τ)[i] = ρ(τ(a, t))[i].

A run ρ of A on σ is accepting iff for each i ∈ P:

(i) If σ ↾i is finite then ρ(τ)[i] ∈ F_{i} where τ is a prefix of σ such that τ ↾i = σ ↾i. (ii) If σ ↾i is infinite then ρ(τ)[i] ∈ G_{i} for infinitely many τ ∈ prf (σ).

We set L(A) to be the set of words in TΣ̃^{ω} accepted by A (i.e. those on which A has an accepting run).

We can solve the emptiness problem for PI automata by reducing it to the emptiness problem for timed Büchi automaton (TBA) as formulated by Alur and Dill [1]. The concerned timed simulation is the obvious one and the details can be found in [7]. In going from a P I automaton to a timed automaton, there will be a 2^{O(K)} blow-up in the size of the automaton.

3 Closure under boolean operations

Here we wish to show that the class of languages accepted by PI automata (over Σ̃) is closed under boolean operations. Using the notion of proper interval sets, we will transform the relevant problems to the domain of ordinary trace languages. We can then apply known constructions involving trace languages to obtain the desired results.

It will be useful to first study a single component of a PI automaton. To this end, let A be a finite alphabet of actions. Then an interval alphabet based on A is a finite subset of A × INT . Let Γ be an interval alphabet based on A. Then an interval automaton over Γ is a structure B = (Q, ⟶, Q_{in}, F, G) where Q is a finite set of states, ⟶⊆ Q × Γ × Q is a transition relation, Q_{in} ⊆ Q is a set of initial states, F ⊆ Q is a set of finitary accepting states and G ⊆ Q is a set of infinitary accepting states. L(B) ⊆ TA^{∞}, the language of timed words accepted by B is now defined in the obvious way. (To be pedantic, one can set P = {1} and Σ_{1} = A and apply the definitions from the previous section.) There is also a symbolic language L_{sym}(B) ⊆ Γ^{∞} that one can associate with B in the classical manner. The finite words in L_{sym}(B) are accepted using members of F and the infinite words are accepted by viewing G as a Büchi condition (see [21] for a standard treatment). It is also the case that there is a natural map tw : Γ^{∞} → TA^{∞} such that tw(L_{sym}(B)) = L(B). The map tw can be defined as follows:

Let σ̂ ∈ Γ^{∞} and σ ∈ TA^{∞}. Then σ ∈ tw(σ̂) iff |σ| = |σ̂| and for each prefix τ(a, t) of σ and each prefix τ̂(b, I) of σ̂ with |τ| = |τ̂| we have a = b and t − time(τ) ∈ I. The function time is of course given inductively by time(ϵ) = 0 and time(τ′(a′, t′)) = t′. As usual, for L ⊆ Γ^{∞} we set tw(L) = ⋃_{σ̂∈L} tw(σ̂). To sum up, the simple observation we wish to start with is:

Proposition 1. Let B be an interval automaton over the interval alphabet Γ (based on A). Then L(B) = tw(L_{sym}(B)). □

Now we turn to proper interval sets. We say that I ⊆ INT is proper iff I is a finite partition of (0, ∞). An interval alphabet Γ based on A is said to be proper iff for each a in A, the set of intervals Γ_{a} is proper where Γ_{a} = {I | (a, I) ∈ Γ }. The next observation which is easy to verify is crucial for our purposes.

Proposition 2. Let Γ be a proper interval alphabet based on A and let σ ∈ TA^{∞}. Then there exists a unique word σ̂ ∈ Γ^{∞} such that σ ∈ tw(σ̂). □

The uniqueness of σ̂ as stated in the above result is the key to reducing the study of timed languages to the study of trace languages in the present setting. This can be achieved by embedding interval alphabets into proper interval alphabets. To formalise this idea, let I, I′ ⊆ INT . Then I′ is said to cover I iff each interval in I can be expressed as the union of a set of intervals taken from I′. Clearly the choice of such a set of intervals (for a given member of I) will be unique in case I′ is a proper interval set.

Let Γ and Γ′ be two interval alphabets based on the alphabet A. Then Γ′ covers Γ iff Γ′_{a} covers Γ_{a} for each a ∈ A.

We will say that L ⊆ TA^{∞} is a regular interval language over A iff there exists an interval alphabet Γ based on A and an interval automaton B over Γ such that L = L(B). For convenience we will often say “interval language” to mean “regular interval language.”

Proposition 3. Let A be a finite alphabet of actions.

(i) Suppose Γ is an interval alphabet based on A. Then one can effectively construct a proper interval alphabet Γ′ based on A such that Γ′ covers Γ.

(ii) The class of interval languages over A is closed under boolean operations.

Proof sketch. (i) follows from the observation that given an interval set I = {I_{1}, …, I_{m}} we can form the set X ∪ {0, ∞} = X′ where X is the set of rational numbers that appear as bounds of the intervals in I. Let X′ = {0, x_{1}, …, x_{n}, ∞} with 0 < x_{1} < x_{2} < ⋯ < x_{n} < ∞. Then

I′ = {(0, x_{1}), [x_{1}, x_{1}], (x_{1}, x_{2}), [x_{2}, x_{2}], …, (x_{n}, ∞)}

is a proper interval set which covers I.

To prove (ii), one first observes that closure under union is obvious. So let B be an interval automaton over the interval alphabet Γ. Then we can construct Γ′ such that Γ′ is proper and covers Γ. Let B = (Q, ⟶, Q_{in}, F, G). Then we construct the interval automaton B′ = (Q, ⟹, Q_{in}, F, G) over Γ′ where ⟹⊆

Q×Γ′×Q is given by: q ⟹^{(a,I′)} q′ iff there exists q ⟶^{(a,I)} q′ in B such that I′ ⊆ I. It is easy to verify that L(B) = L(B′). Using classical techniques we can now find an interval automaton B′′ over Γ′ such that L_{sym}(B′′) = (Γ′)^{∞}−L_{sym}(B′). Since Γ′ is proper we can now use proposition 2 to conclude that L(B′′) = TA^{∞} − L(B′). □

The technique used in the second part of the proof is deployed in different contexts to establish many of our results. It is for this reason we have presented some of the key details in a very simple setting.

We can now address the main concerns of this section. To show closure under boolean operations of the languages accepted by PI automata, we will first characterise these languages using interval languages. Let {L_{i}} be a family of languages such that L_{i} ⊆ TΣ_{i}^{∞} for each i. (Recall Σ̃ = {Σ_{i}}_{i∈P}.) Then ⊗(L_{1}, …, L_{K}) denotes the language L ⊆ TΣ̃^{ω} defined as:

σ ∈ L iff σ ↾i ∈ L_{i} for each i.

We will say that L ⊆ TΣ̃^{ω} is a regular direct product interval language iff there exists a family {L_{i}} such that each L_{i} is a regular interval language over Σ_{i} and L = ⊗(L_{1}, …, L_{K}). A regular product interval language over Σ̃ is a finite union of regular direct product interval languages over Σ̃. Again, for convenience, we will often say “product interval language” to mean “regular product interval language” etc..

Theorem 1. Let L ⊆ TΣ̃^{ω}. Then L is a product interval language iff there exists a PI automaton B over Σ̃ such that L = L(B). □

Using the theory of product languages [15], which is a natural subclass of Mazurkiewicz trace languages and the technique used in the proof of Proposition 3 we can now show:

Theorem 2. The class of product interval languages over Σ̃ is closed under boolean operations.

4 A logical characterisation of product interval languages

Our goal here is to first develop a logical characterisation of product interval languages in terms of a monadic second order logic. We shall then present a related linear time temporal logic for reasoning about timed behaviours captured by PI automata. As done in the previous section it will be convenient to first concentrate on the one component case.

Let A be a finite alphabet of actions. Here and in the logics to follow, we assume a supply of individual variables x, y, … and set variables X, Y, . . .. For each a ∈ A we have a unary predicate Q_{a}. There are also predicates of the form Δ(x, I) in which x is an individual variable, and I is a member of INT .

The syntax of the logic TMSO(A) is given by:

\begin{aligned}TMSO(A) & ::= & x ∈ X | x < y | Q_{a}(x) | Δ(x, I) | φ ∨ φ′ | ∼ φ | \\ & & (∃x)φ | (∃X)φ. \end{aligned}

A structure for this logic is a pair (σ, 𝕀) where σ ∈ TA^{∞} and 𝕀 is an interpretation which assigns to each individual and set variable, an element and subset, respectively, of the set pos(σ). We define pos(σ) to be the set {1, 2, …, |σ|} in case σ is finite, and {1, 2, …} if σ is infinite. As is customary, σ can be also viewed as a map from pos(σ) into A with σ(n) for n ∈ pos(σ) having the obvious meaning. We will use this view of σ whenever convenient. Turning now to the semantics, let (σ, 𝕀) be a structure. Then σ ⊧_{𝕀} (x < y) iff 𝕀(x) <′ 𝕀(y). (Here <′ is the usual ordering over the integers). Further, σ ⊧_{𝕀} Q_{a}(x) iff σ(𝕀(x)) = (a, t) for some t. As for the predicate Δ(x, I), we have

σ ⊧_{𝕀} Δ(x, I) iff t − time(τ) ∈ I, where τ(a, t) is the prefix of σ s.t.
|τ(a, t)| = 𝕀(x).

The semantics of the logical connectives ∼, and ∨, and the existential quantifiers ∃x and ∃X are given in the expected manner. For a sentence φ ∈ TMSO(A) we set L(φ) = {σ ∈ TA^{∞} | σ ⊧ φ}.

We can now use the classical logical characterisation of ω-regular languages and the notion of proper interval alphabets to establish:

Theorem 3. Let L ⊆ TA^{∞}. Then L is an interval language iff there exists a sentence φ ∈ TMSO(A) such that L = L(φ).

Next we wish to present the logic TMSO^{⊗}(Σ̃) which will characterise product interval languages. The syntax of the logic is given by:

TMSO^{⊗}(Σ̃) ::= φ(i) | ∼ α | α ∨ β | α ∧ β

where for each formula φ(i) we require φ ∈ TMSO(Σ_{i}).

A structure for the logic is a pair (σ, {𝕀_{i}}_{i∈P}), where σ ∈ TΣ̃^{ω} and for each i ∈ P, 𝕀_{i} is an interpretation for individual and set variables over the set of positions pos(σ ↾i). As for the semantics,

σ ⊧_{{𝕀_{i}}_{i∈P}} φ(i) iff σ ↾i ⊧_{𝕀_{i}} φ.

The boolean operators ∼, ∨ and ∧ are interpreted in the usual manner. Once again, for a sentence φ ∈ TMSO^{⊗}(Σ̃), we set L(φ) = {σ ∈ TΣ̃^{ω} | σ ⊧ φ}.

Theorem 4. Let L ⊆ TΣ̃^{ω}. Then L is a product interval language iff L = L(φ) for some sentence φ ∈ TMSO^{⊗}(Σ̃).

This result is established by exploiting Theorem 1 and yet again the notion of proper interval alphabets.

As a natural temporal logic counterpart of TMSO^{⊗}(Σ̃), we present here the logic TLTL^{⊗}(Σ̃). Again, we will build up the formulas in two steps. For ease of presentation, we will not deal with atomic propositions here. Where necessary, they can be introduced component-wise and dealt with easily.

TLTL(Σ_{i}) ::= ⊤ | ∼ φ | φ ∨ φ′ | ⟨a, I⟩φ | Oφ | φUφ′ .

For each formula of the form ⟨a, I⟩φ, we require that a ∈ Σ_{i}.

The formulas of TLTL^{⊗}(Σ̃) are simply boolean combinations of TLTL(Σ_{i})- formulas:

TLTL^{⊗}(Σ̃) ::= φ(i) | ∼ α | α ∨ β.

Here we require from each formula of the form φ(i) that φ ∈ TLTL(Σ_{i}).

The semantics of this logic is given by defining the relation σ ⊧ α with σ ∈ TΣ̃^{ω}. To spell out the details, σ ⊧ φ(i) iff σ ↾ i, ϵ ⊧_{i} φ. The relation ⊧_{i} is defined in the obvious way. For instance,

σ, τ ⊧_{i} ⟨a, I⟩φ iff there exists t such that τ(a, t) ∈ prf (σ) and
σ, τ(a, t) ⊧_{i} φ and t − time(τ) ∈ I.

On the other hand σ, τ ⊧_{i} Oφ iff there exists τ(a, t) ∈ prf (σ) such that σ, τ(a, t) ⊧_{i} φ.

For each α in TLTL^{⊗}(Σ̃) we define L(α) = {σ ∈ TΣ̃^{ω} | σ ⊧ α}. Clearly, α is satisfiable iff L(α) is non-empty.

Theorem 5. For each α in TLTL^{⊗}(Σ̃) we can effectively construct a PI automaton A_{α} such that L(α) = L(A_{α}) and the number of global states of A_{α} is 2^{O(|α|)}. Further, the largest constant mentioned in the i^{th} component of A_{α} is at most the largest i-type constant mentioned in α.

Proof sketch. The proof follows the usual automata-theoretic techniques. To account for negation correctly, the local transition relations of A_{α} must be over proper alphabets. The obvious idea of converting α into a formula which mentions only intervals taken from a proper interval set will cause an exponential blow-up. To avoid this, we define the (Fisher-Ladner) closure of α to be smallest set of formulas containing the subformulas of α and satisfying: If (φUφ′)(i) is in the closure then so is O((φUφ′)(i)). Let CL be the closure of α and CL_{i} = CL ∩ TLTL(Σ_{i}) for each i. We now define an i-type atom to be a propositionally consistent subset of CL_{i} which satisfies: If ⟨a, I⟩φ and ⟨b, I′⟩φ′ are in the atom then a = b and I ∩ I′ ≠ ∅. We can now use i-type atoms to manufacture the i-local states. The i-local transition relation can then be chosen to be proper. The remaining details are guided by the way the logic LTL^{⊗}(Σ) is dealt with in [20]. □

Using theorem 5, and the emptiness check for PI automata in section 2, we can decide satisfiability of α in time 2^{O(|α|+K log K)}. In fact, we can show:

Corollary 1. The satisfiability problem for TLTL^{⊗}(Σ̃) is PSPACE-complete.

Given a formula α in TLTL^{⊗}(Σ̃) we can check the emptiness of the automaton A_{α} of theorem 5 non-deterministically while using space polynomial in the size of α. The argument is similar to the one in [1]. The fact that the problem is PSPACE-hard follows from the observation that the satisfiability problem for LTL can be reduced to the satisfiability problem for the one-agent case of TLTL^{⊗}(Σ̃).

Next suppose we consider a real-time program Pr modelled by a PI automaton A_{Pr}, and a formula α of TLTL^{⊗}(Σ̃). Then Pr is said to meet the specification α iff L(A_{Pr}) ⊆ L(α). The model checking problem for TLTL^{⊗}(Σ̃) is to determine whether Pr meets the specification α. It is not difficult to show:

Theorem 6. The model checking problem for TLTL^{⊗}(Σ̃) is PSPACE complete.

We have not studied in detail the power and limitations of TLTL^{⊗}(Σ̃) from a pragmatic standpoint. We have explored TLTL^{⊗}(Σ̃) here mainly because it is the natural temporal logic suggested by TMSO^{⊗}(Σ̃), the characteristic logic for PI automata. In fact, it is not difficult to show that TLTL^{⊗}(Σ̃) is expressively equivalent to the first-order fragment of TMSO^{⊗}(Σ̃).

In order to provide some example properties that can be stated in this timed temporal logic, we first sketch briefly how product interval automata can be used to model asynchronous digital circuits. (The full details will appear elsewhere.) Our starting point is the circuit model developed in [17] using inertial delays. The behaviour of a k-gate circuit χ, denoted L(χ), can be defined as a subset of TΣ^{∞}, where Σ is the alphabet {0, 1}^{k} × {0, 1}^{k}. An element of {0, 1}^{k} will represent the visible values of the gate outputs. The occurrence of an action (s, s′) will indicate the visible values of the gate outputs going from s to s′ due to the simultaneous switching of an appropriate set of gates. We can associate with χ, a (k + 1)-component product interval automaton A_{χ} such that L(A_{χ}) = L(χ). We use one component for each gate in the circuit. This component will keep track of the switching status of the gate (whether excited or quiescent); and, in case it is in an excited state, the time elapsed since its excitement was initiated last. The (k +1)-th component keeps track of the current vector of visible values. Suppose its state is s and it permits an action (t, t′) at s, then it will be the case that s = t. It will also be the case that the circuit allows the transition from t to t′ through the switching of a subset of gates that are excited at t. Furthermore, the distribution of actions across the components is such that the action (t, t′) will involve – apart from the component k+1 – all those components whose switching status is affected by the switches. As for timing constraints, the component i will have timing constraints that enforce the inertial delay corresponding to the output wire of gate-i, while the (k + 1)-th component will be free of any timing constraints.

We can use the logic TLTL^{⊗}(Σ̃) to express (and hence model-check) a variety of properties of χ. Two examples of such properties are:

– If the input signals to χ stabilise then the behaviour of χ eventually stabilises.

– gate i is d-persistent; whenever it becomes excited it turns quiescent only through its switching and further more this switching occurs within d time units since it got excited.

5 Distributed Interval Automata

Here we consider a more expressive class of distributed timed automata but having the same flavour as PI automata. The extension we have in mind will parallel the extension of product automata to asynchronous automata in the setting of traces as detailed in [15].

We shall continue to work with the P-distributed alphabet Σ̃. An a-interval for us will be a map J : loc(a) → INT . Let INT^{(a)} be the set of a-intervals. An a-interval, viewed as a rectangular region, will constitute the guard constraining the timed occurrence of an a-action.

In the definition of our automata and elsewhere we will often write {X_{i}} to denote the family {X_{i}}_{i∈P}. A distributed interval automaton over Σ̃ is a structure

A = ({Q_{i}}, {⟶_{a}}_{a∈Σ}, Q_{in}, {F_{i}, G_{i}})

where the various components of A are defined as follows. While doing so we will also develop some notations.

(i) Each Q_{i} is a finite non-empty set called the set of i-local states. Let P be a non-empty subset of P. Then a P -state is a map q : P → ⋃_{i∈P} Q_{i} such that q(i) ∈ Q_{i} for each i ∈ P. An a-state is just a loc(a)-state and a P-state will be called a global state. We let Q_{a} denote the set of a-states and Q_{P} the set of global states.

(ii) ⟶_{a} is a finite subset of Q_{a} × INT^{(a)} × Q_{a} for each a ∈ Σ. (iii) Q_{in} ⊆ Q_{P} is the set of global initial states. (iv) F_{i}, G_{i} ⊆ Q_{i} for each i.

Thus a distributed interval automaton is a timed version of an asynchronous Büchi automaton as formulated in [18] which in turn is a minor variant of the original formulation due to Gastin and Petit [11]. If one ignores the acceptance conditions then an asynchronous automaton can be viewed as a labelled 1-safe Petri net. Consequently a distributed interval automaton can also be viewed as a timed 1-safe Petri net. However, as pointed out in the introduction, the timed semantics we assign to our automata is not the semantics one encounters in the literature concerning timed Petri nets [5].

We can now systematically extend the theory of PI automata – as sketched in the previous sections – to distributed interval automata. The details can be found in [7].

It turns out that the so called cellular version of distributed interval automata, has the same expressive power as the event recording automata [2]. In this version of asynchronous automata there will be one component for each letter in Σ and one clock associated with each component. The interesting fact is that in the untimed setting both versions of asynchronous automata have the same expressive power. Once again we refer the reader to [7] for the details.

References

1. R. Alur, D. L. Dill: A theory of timed automata, Theoretical Computer Science 126: 183–235 (1994).

2. R. Alur, L. Fix, T. A. Henzinger: Event-clock automata: a determinizable class of timed automata, Proc. 6th International Conference on Computer-aided Verification, LNCS 818, 1–13, Springer-Verlag (1994).

3. R. Alur, T. A. Henzinger: Logics and Models of Real Time: A Survey, in Real-Time: Theory in Practice, J. W. de Bakker, H. Huizing, W. -P. de Roever, G. Rozenberg (Eds.), LNCS 600, 74–106, (1992).

4. J. Bengtsson, B. Jonsson, J. Lilius, W Yi: Partial Order Reductions for Timed Systems, Proc. CONCUR ’98, LNCS 1466 (1998).

5. B. Berthomieu, M. Diaz: Modelling and Verification of Time Dependent Systems Using Time Petri Nets, IEEE trans. on Soft. Engg. Vol 17, No. 3, March 1991

6. V. Diekert, G. Rozenberg: The Book of Traces, World Scientific, Singapore (1995).

7. D. D’Souza, P. S. Thiagarajan: Distributed Interval Automata, Internal Report TCS-98-3, Chennai Mathematical Institute (1998). (available at

http://www.smi.ernet.in/techreps/)

8. W. Ebinger, A. Muscholl: Logical definability on infinite traces, Theoretical Computer Science 154: 67–84 (1996).

9. T. A. Henzinger, P. W. Kopke, A. Puri, P. Varaiya: What’s decidable about hybrid automata?, Proc. 27th Annual Symposium on Theory of Computing, 373–382, ACM Press (1995).

10. M. Minea: Partial Order Reduction for Model Checking of Timed Automata. To appear in the Proceedings of CONCUR’99.

11. P. Gastin, A. Petit: Asynchronous cellular automaton for infinite traces, Proceedings of ICALP ’92, LNCS 623, 583–594 (1992).

12. R. Gerth, D. Peled, M. Vardi, P. Wolper: Simple On-the-fly Automatic Verification of Linear Temporal Logic. Proc. 15th IFIP WG 6.1 Int. Workshop on Protocol Specification, Testing, and Verification. North-Holland Publ. (1995).

13. T. A. Henzinger: It’s About Time: Real-Time Logics Reviewed, Proc. CONCUR ’98, LNCS 1466, 366–372 (1998).

14. T. A. Henzinger, J.-F. Raskin, and P.-Y. Schobbens: The regular real-time languages, Proc. 25th International Colloquium on Automata, Languages, and Programming 1998, LNCS 1443, 580–591 (1998).

15. J. G. Henriksen, P. S. Thiagarajan: A Product Version of Dynamic Linear Time Temporal Logic, Proc. CONCUR ’97, LNCS 1243, 45–58, (1997).

16. N. Klarlund, M. Mukund, M. Sohoni: Determinizing Büchi Asynchronous Automata, Proceedings of FSTTCS 15, LNCS 1026, 456–470 (1995).

17. O. Maler, A. Pnueli: Timing Analysis of Asynchronous Circuits using Timed Automata, in Proc. CHARME ’95, LNCS 987, 189–205 (1995).

18. M. Mukund, P. S. Thiagarajan: Linear Time Temporal Logics over Mazurkiewicz Traces, Proc. MFCS 96, LNCS 1113, 62–92 (1996).

19. J. -F. Raskin, P. -Y. Schobbens: State-clock Logic: A Decidable Real-Time Logic, Proc. HART ’97: Hybrid and Real-Time Systems, LNCS 1201, 33–47 (1997).

20. P. S. Thiagarajan: A Trace Consistent Subset of PTL, Proc. CONCUR ’95, LNCS 962, 438–452 (1995).

21. W. Thomas: Automata on Infinite Objects, in J. V. Leeuwen (Ed.), Handbook of Theoretical Computer Science, Vol. B, 133–191, Elsevier Science Publ., Amsterdam (1990).

22. Th. Wilke: Specifying Timed State Sequences in Powerful Decidable Logics and Timed Automata, in Formal Techniques in Real-Time and Fault-Tolerant Systems, LNCS 863, 694–715 (1994).

23. G. Winskel, M. Nielsen: Models for Concurrency, in S. Abramsky, D. Gabbay (Eds.) Handbook of Logic in Computer Sc., Vol. 3, Oxford Univ Press (1994).

24. W. Yi, B. Jonsson: Decidability of Timed Language-Inclusion for Networks of Real-Time Communicating Sequential Processes, in Proc. FST&TCS 94, LNCS 880