A Logical Study of Distributed Timed Automata

Thesis

Submitted in partial fulfilment of the requirements

for the degree of Doctor of Philosophy

By

Deepak D’Souza

Chennai Mathematical Institute, Chennai.

Under the Supervision of Prof. P. S. Thiagarajan

Chennai Mathematical Institute, Chennai.

Birla Institute of Technology and Science Pilani (Rajasthan) India

January 2000.

Acknowledgements

The work in this thesis would not have been possible without the guidance and encouragement of my advisor Prof. P. S. Thiagarajan. During the course of my Ph. D. I have had many occasions to draw on his resourcefulness, clarity of thought, and his wealth of experience as a researcher. I have learnt from him the virtues of rigour and professionalism, and I am grateful to him for having kept me focussed at the times it mattered most. In short, I thank him for being a model advisor.

I am very grateful to Dr. Madhavan Mukund, who has been in many ways a role model for me. Throughout my stay at CMI I have relied heavily on his advice in technical (and non-technical!) matters and his readiness to help has always been heartening. It has been a pleasure to discuss several topics in this thesis with him, and much of the material presented here has benefited from his comments.

I am grateful to the others in the CS group at CMI, Dr. Narayan Kumar and Dr. K. V. Subrahmanyam for the several discussions I have had with them. Kumar in particular has been very patient in discussing several philosophical aspects of my thesis with me. A special word of thanks is due to P. Madhusudan who has been my course-mate since the start of my Ph. D. I have benefited a great deal from his inquiring mind and maturity of thought. I have also had many useful discussions with A. Srinivasan and K. Sambaiah on several topics in this thesis.

B. Meenakshi has been an immense help to me in preparing this thesis. She has painstakingly gone through each draft and given me very valuable feedback. Thanks Shoba, for all the help, the companionship, and especially for keeping me on course.

I would like to thank Mogens Nielsen and Thomas Hune for an enjoyable summer at BRICS, Aarhus University, where a part of this work was completed.

A special word of thanks to the CS faculty at Matscience and CMI, for the excellent course work they took us through. The close cooperation between Matscience and CMI indeed made for a very conducive working environment for us students.

I would like to thank the administrative staff at CMI—S. Sripathy, V. Vijaylakshmi, Rajeshwari Nair and G. Samson, for all the help they have rendered over the years.

Finally, I would like to dedicate this thesis to my parents, especially my late mother, who would have been the happiest to see this thesis in print.

Deepak D’Souza Chennai, January 2000.

Birla Institute of Technology & Science Pilani Rajasthan

\underline{Certificate}

This is to certify that the thesis entitled “A Logical Study of Distributed Timed Automata” and submitted by Deepak D’Souza (ID. No. 1994PZYF772) for award of Ph. D. Degree of the Institute, embodies original work done by him under my supervision.

Signature in full of the Supervisor:

Name: P. S. Thiagarajan

Designation: Professor,

Chennai Mathematical Institute,

Date: Chennai.

Contents

Acknowledgements i

1 Introduction 1 1.1 Model checking for timed systems . . . . . . . . . . . . . . . . 3 1.2 Analysing timed automata . . . . . . . . . . . . . . . . . . . . 6 1.3 Contributions of this thesis . . . . . . . . . . . . . . . . . . . . 8 1.4 Related Work . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 1.5 Organisation of the thesis . . . . . . . . . . . . . . . . . . . . 14

2 Interval Automata 16 2.1 Preliminary notions . . . . . . . . . . . . . . . . . . . . . . . . 16 2.2 Interval automata and their languages . . . . . . . . . . . . . 22 2.3 Checking emptiness . . . . . . . . . . . . . . . . . . . . . . . . 24 2.4 Closure under boolean operations . . . . . . . . . . . . . . . . 26 2.5 A logical characterisation . . . . . . . . . . . . . . . . . . . . . 29

3 Product interval automata 35 3.1 Preliminaries . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 3.2 Product interval automata . . . . . . . . . . . . . . . . . . . . 36 3.3 Checking emptiness . . . . . . . . . . . . . . . . . . . . . . . . 37 3.4 Product interval languages . . . . . . . . . . . . . . . . . . . . 40 3.5 Closure under boolean operations . . . . . . . . . . . . . . . . 43 3.6 A logical characterisation . . . . . . . . . . . . . . . . . . . . . 44

4 Timed product-LTL 46 4.1 TLTL over a single component . . . . . . . . . . . . . . . . . . 47 4.2 Product TLTL . . . . . . . . . . . . . . . . . . . . . . . . . . 51 4.3 Expressive completeness of TLTL^{⊗} . . . . . . . . . . . . . . . 54

5 Modelling asynchronous circuits 59 5.1 The non-deterministic delay model . . . . . . . . . . . . . . . 59 5.2 Modelling a circuit as a PIA . . . . . . . . . . . . . . . . . . . 62 5.3 Proof of correctness . . . . . . . . . . . . . . . . . . . . . . . . 63 5.4 Properties expressed in TLTL^{⊗} . . . . . . . . . . . . . . . . . 65

6 Distributed interval automata 67 6.1 Preliminaries . . . . . . . . . . . . . . . . . . . . . . . . . . . 67 6.2 Distributed interval automata . . . . . . . . . . . . . . . . . . 71 6.3 Checking emptiness . . . . . . . . . . . . . . . . . . . . . . . . 74 6.4 Closure under Boolean Operations . . . . . . . . . . . . . . . . 77 6.5 Timed trace languages . . . . . . . . . . . . . . . . . . . . . . 79 6.6 A logical characterisation . . . . . . . . . . . . . . . . . . . . . 82

7 Cellular interval automata 87 7.1 Preliminaries . . . . . . . . . . . . . . . . . . . . . . . . . . . 88 7.2 Cellular interval automata . . . . . . . . . . . . . . . . . . . . 92 7.3 Closure and logical properties . . . . . . . . . . . . . . . . . . 95 7.4 Event recording automata . . . . . . . . . . . . . . . . . . . . 96

8 Conclusion 100 8.1 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 100 8.2 Future Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . 102

Bibliography 103

List of Publications 107

Chapter 1

Introduction

The work in this thesis falls in the broad area of research in computer science known as formal verification. Formal verification involves proving mathematically that the design of a system satisfies its specification. The term system is used here to mean any kind of algorithmic activity, like a computer program, a traffic signalling system, or a controller in a chemical plant.

Formal verification must be distinguished from the field of testing, where one tests the actual implementation of the system under different systematically generated test conditions. As is to be expected, these test cases cannot cover all possible scenarios. Formal verification on the other hand aims to prove that the design of the system is correct, i.e. it satisfies its specification, in all possible scenarios. Both techniques must however be seen as complementary activities. Each is applicable in a different phase of system development—verification in the design phase, and testing in the post-implementation stage—and together they contribute to an increased level of confidence in the correct working of the system.

The importance of formal methods in ensuring the correct working of a system cannot be over emphasised. Errors in safety critical systems like railway signalling systems, avionics software, and controllers in nuclear reactors, can be catastrophic in terms of loss of human life and property. Most errors are subtle, difficult to simulate, and hence beyond the scope of human inspection. Furthermore these errors are, more often than not, errors in the design of the system. Thus the use of formal methods in the design phase of system development can be a big step towards building correctly functioning systems.

Formal methods in verification can be broadly classified under the two approaches of theorem proving and model checking. Theorem proving typically involves an axiomatisation of the constructs of a programming language. An assertion about a program is proved by a series of logical deductions, using precisely defined inference rules. This method is only semi-automatic in the sense that while portions of the proof can be carried out by the theorem proving tool, the user must guide the general direction of the proof by laying down sub-goals.

Model checking on the other hand is a fully automatic method of verification. This is largely because it restricts itself to essentially finite state systems. The term “model checking” is derived from the fact that in this method one checks whether the system is a “model” of the given specification, in much the same manner that one checks whether a truth assignment satisfies a given propositional logic formula.

In model checking, the system to be verified is modelled as a transition system comprising states, which can be thought of as a collection of propositions describing that state, and transitions or actions which cause a change from one state to another. Thus, if the system to be modelled is a program, then a state in the model would comprise a description of the current values of the variables and the location counter in the program. For example, the

propositions location-counter = 1 and request = false could describe

the current state of a program. Each statement in the program, like request := true is an action which typically causes a change in the current state of the program.

Specifications in this framework are given in Temporal Logic, a specification language originally proposed by Pnueli in [P77]. The operators in temporal logic like “always” and “eventually” have proved to be well suited for specifying safety and liveness properties of systems. A safety property says that something undesirable never happens. For example, a safety property could require that “two processes are never in their critical sections simultaneously.” A liveness property on the other hand asserts that the system makes progress: “if a process asks for a resource, then its request is eventually granted.”

Temporal logic specifications are essentially interpreted over runs of the system. These are valid sequences of states and actions that the system can execute. Temporal logic specifications are usually classified as being either linear time or branching time. In the branching time framework, the behaviour of the system is viewed as a run tree which incorporates the branching due to non-deterministic choices made by the system. In the linear time setting, one views the behaviour of the system as comprising the set of valid runs of the system. In particular, we say a system satisfies a linear time temporal logic (LTL) formula φ if every run of the system satisfies φ.

The automata-theoretic approach to model checking introduced by Vardi and Wolper [VW86] allows the model checking problem to be phrased as a purely automata-theoretic problem. This permits the application of wellstudied automata-theoretic algorithms to the problem of model checking. In the linear time setting, the system is modelled as a finite state automaton S, which recognises exactly the runs of the system. A temporal logic specification φ can be converted to an automaton A_{φ} which recognises exactly the the models of φ. Thus the model checking problem “Does S satisfy φ?” can be rephrased as: is L(S) ⊆ L(A_{φ})? This is equivalent to checking if L(S) ∩ L(A_{¬φ}) = ∅. Here A_{¬φ} is an automaton accepting the models of the negation of φ, and is hence also the complement of the language accepted by A_{φ}.

A pleasant feature of this framework of model checking is its connection to logic. In the early sixties Büchi had showed that language recognition by automata was the same as logical definability by S1S—a monadic second order logic interpreted over words. LTL was later shown to be expressively equivalent to the first-order fragment of S1S. This, along with the fact that it has a decision procedure which is exponential in the size of the formula as against the non-elementary decision procedure for the first-order fragment of S1S, is often seen as an endorsement of LTL as a good specification logic.

1.1 Model checking for timed systems

This thesis is concerned with the application of model checking techniques in the formal verification of real time systems. These are systems whose behaviour depends crucially on the times at which external events happen, and not just on the ordering of the events. These systems are widespread in everyday life and range from household goods like washing machines and toasters, to safety critical systems like automobile braking systems and plant controllers. Traditional techniques for model checking are inadequate when it comes to reasoning about such systems, since they typically abstract away from quantitative timing information in the system. System models and logics speak only of an event following another, and not of how much later it can happen.

These issues can be brought out through the example of a railroad crossing controller, a popularly cited example of a timed system. Fig 1.1 shows the railroad crossing and an area C around the crossing, called the critical region. The gate controller receives signals, via sensors located on the track, telling it when a train approaches and exits the crossing. The sensors are located so that a train takes at least 2 minutes to reach the critical region C after signalling “approach.” Further, when it leaves the crossing, it sends an “exit” signal to the controller. The “exit” signal can occur anytime between 2 to 5 minutes after the train has entered the critical region. Upon receiving the

controller  critical region C

Figure 1.1: Railroad crossing controller.

“approach” signal, the controller must lower the gate. It begins to lower the gate within a minute of receiving the “approach” signal from the train. Once initiated by the controller, the gate takes at most a minute to lower itself completely. A similar sequence of actions takes place when the train leaves the critical area. Upon receiving the “exit” signal from the train, the controller begins to raise the gate. Again there is a delay of at most a minute for the controller to initiate the “raise” action, and for the gate to raise itself completely.

We make the simplifying assumption that there can be at most one train in the system at a given time. Thus a train cannot “approach” the crossing without all trains before it having exited the crossing.

The crucial question we would like to ask of the system is: is it safe? That is, is it the case that whenever a train is in the critical area, the gate is indeed down. Another question we may be interested in is regarding the utility of the system: if there is no train in the region for 10 minutes, is the gate raised to allow traffic to pass during this period?

A natural way to model the system would be to have a separate transition system for each component—one each for the train, the controller, and the gate—since these components function largely on their own and communicate with each other only for specific tasks related to the crossing. The communication between the components can be modelled by having the components synchronise on common actions. For example the train and controller components must synchronise on the action “approach.” In our method of synchronisation, for the system to execute a synchronising action, all components involved in that action must be ready to execute the action. Thus the train must wait till the controller is ready, before they can jointly perform the “approach” action. This can be interpreted as saying that when

⟹  ⟹  ⟹ {x}  (x > 2) {x} approach in exit (2 < x < 5)  down approach {y}  lower {y} (y < 1) {y} exit (y > 5) raise (y < 1) Train  Controller  Gate lower {z}  (z < 1) {z} {z} raise up (z < 1)

Figure 1.2: Timed automata model of the railroad crossing controller

the train sends the “approach” signal, it must wait for an acknowledgement from the controller before it can continue towards the crossing.

Suppose now that we abstract away from the timing information in the system, and simply model the fact that the components perform a sequence of causally dependent actions. It is not difficult to see that in this case the model we build will turn out to be unsafe. More importantly, the model permits several runs of the system that would otherwise be eliminated due to the timing constraints in the components.

The timed automata of Alur and Dill are transition system based models which are specially meant to capture the time-dependent nature of such systems. These are essentially finite state automata which are extended with a finite set of clock variables. The transitions of these automata are guarded by conditions on the clock variables, like “x > 2,” and also specify a subset of clocks which are to be reset if this transition is taken. These automata generate sequences of action and time-stamp pairs called timed words. Operationally, we can generate timed words from a timed automaton in much the same way that we generate words from a classical automaton: we begin at an initial state and repeatedly take outgoing transitions from the states we visit, outputting the action label in the process. In the case of a timed automaton, we must additionally keep track of the current values of the clocks. We can let time elapse by staying in a state, with the clocks recording this elapsed time. When we choose to take a transition out of the state, the guard on the transition must be satisfied by the current values of the clock variables. The clock vector is then updated by resetting the set of clocks mentioned on the transition.

Figure 1.2 shows the railroad crossing system modelled as a network of timed automata. Each component is modelled as a timed automaton with a single clock variable. The transitions in each automaton are labelled by arrows of the form ⟶_{X}^{a, g} where a is the action label of the transition, X is the set of clocks to be reset along the transition, and g is the guard on the transition. As described earlier, the component automata must synchronise on common actions.

Let us examine the component for the train in some detail. Firstly, we should point out that we have used a single component to model all the trains in the system. This can be done without any loss of generality, since we have assumed that no more than one train can be in the system at a given time. The component has a single clock variable x. The train is initially in its start state (marked with an incoming double arrow in the figure). It can then take the transition labelled “approach” at any time, and reset its clock in the process. It must now let at least 2 minutes elapse before it can do the action “in.” Once again x is reset along this transition. Finally, it can take the transition labelled “exit” anytime between 2 to 5 minutes after the “in” action. Of course, when it is working in tandem with the other components in the system, it must wait till the other components are ready to participate before it can perform synchronisation actions like “approach” and “exit.”

The safety and utility questions about the system can now be phrased in terms of this model. Every consecutive pair of “in” and “exit” actions must be preceded by a “down” action, and there should be no other action of the gate in between. The utility property can be phrased as follows. At any instant, if an “exit” action occurs, and there is no “approach” action in the next 10 minutes, then the gate must perform a “raise” action within 2 minutes.

1.2 Analysing timed automata

The operational semantics we sketched earlier for a timed automaton A can be formalised in terms of an infinite state transition system T_{A}. Each state of this transition system is a pair comprising a state of the automaton, and a clock valuation which assigns to each clock a non-negative real value. The initial states of the transition system are the states of form (s_{0}, v_{0}) where s_{0} is an initial state of the automaton, and v_{0} is the zero valuation, in which all clocks have value 0. Suppose we are in a state (s, v) of this transition system at time t. Then we can take a transition labelled (a, t′) and go to state (s′, v′) provided there exists a transition in the automaton of the form s ⟶_{X}^{a, g} s′ with v + (t′ − t) satisfying the guard g, and v′ being the resulting clock vector obtained from v +(t′ −t) by setting the clocks in X to zero. The valuation v + (t′ − t) is obtained from v by incrementing the value of each clock by (t′ − t).

How do we answer questions—like the ones posed about our model of the railroad crossing controller—when the object we need to reason about is infinite? Alur and Dill showed that this infinite transition system can be quotiented by defining an appropriate bisimulation on the states of the transition system. The quotiented transition system is finite and has the property that it recognises precisely the “untimed” language of the given timed automaton. By the untimed language we mean the classical word language obtained by projecting away the time stamps of the actions. Thus if (a_{1}, t_{1}), (a_{2}, t_{2}), … (a_{n}, t_{n}) were a timed word generated by the original transition system, then the sequence a_{1}, a_{2}, …, a_{n} is a word accepted by the quotiented automaton. Conversely, if a_{1}, a_{2}, …, a_{n} were a word accepted by the quotiented transition system, then there exist times t_{1}, t_{2}, …, t_{n} such that (a_{1}, t_{1}), (a_{2}, t_{2}), …, (a_{n}, t_{n}) is a timed word in the original automaton.

It is pertinent to mention here the method of Berthomieu and Menasche which was one of the early methods of analysing timed systems. Their method, introduced in the context of time Petri nets [BM83], gives a quotienting of the infinite state semantic transition system by a simple subset construction. It turns out that each “subset” state can be described as a special form of convex polytope, and as a result the quotienting leads to a finite state transition system. This transition system (often referred to as the “zone” automaton), recognises the untimed language of the given timed automaton. Though in the worst case the number of states in the zone automaton is no less than those in the “region” automaton of Alur and Dill, the method performs well in practice and is popularly used in timed automata based verification tools like Kronos and Uppaal.

The quotiented automaton accepting the untimed language can be used to answer questions like “does the timed automaton accept any timed word at all?” since this is true if, and only if, the quotiented automaton itself accepts some word. Thus, properties like the safety property of our controller model can be verified directly using the quotiented automaton. However, to be able to check timing properties like the utility property, one must typically convert the specification itself into a timed automaton S, and then check whether L(A) ⊆ L(S). Since timed automata are closed under intersection, one can equivalently check if L(A) ∩ L(S′) = ∅, provided that the complement S′ of S exists.

1.3 Contributions of this thesis

One of the drawbacks of timed automata is that they are not closed under complementation. In fact, the language inclusion problem for this class is undecidable. As a result, if one wants to carry out model checking in this framework, one must either use deterministic specifications (which can be easily complemented) or one must work with a subclass of timed automata which has the required closure properties. From a theoretical standpoint the second route is more appealing, since it would mean identifying a class which parallels the classical untimed framework which, as we sketched earlier, has several advantages. From a practical point of view too, we would like to retain the feature of non-determinism which can be useful in a specification language.

In this thesis we adopt this route and propose suitable subclasses of timed automata and develop their theory. A common feature of these automata is that they comprise a network of timed automata which synchronise on common actions. The main restriction on the component automata is that each has a single clock, which must be reset with every action of that component. The model shown in Fig. 1.2 is in fact such an automaton. (Strictly speaking, the components don’t reset their clocks along every transition—for example the train doesn’t reset its clock along the “exit” action—but it is easy to see that this can be enforced, in this case, without affecting the behaviour of the model.)

The controller model is an instance of a product interval automaton, the weakest subclass we define. Here the synchronisations are determined completely by whether the participating components are willing to take part in the action. By allowing the synchronisations to be specified in a more “global” manner, we obtain the class of distributed interval automata, which are more expressive than product interval automata. Here we are allowed to examine the states of the participating components as well. Finally, we introduce cellular interval automata which are based on a generalization of distributed interval automata, where we have a separate component for each action.

Looked at in another way, these classes of automata are ways of structuring general multi-clock timed automata so as to give us a subclass with a clean theory. As we show, each of these subclasses is closed under the boolean operations of union, intersection and complementation. These automata can be determinized, and hence complemented, due to the disciplined way in which the clocks are reset. In addition, they admit a logical characterisation in terms of a full monadic second order logic interpreted over timed words. Typically, these logics have a timed modality of the form Δ_{i}(x, I) which asserts that at the position x in the timed word, the time since component i last performed an action lies in the interval I.

In the case of product interval automata, we investigate a natural temporal logic suggested by this logical characterisation, called timed product LTL, and denoted TLTL^{⊗}. This logic comprises boolean combinations of assertions about the timed behaviour of each component. We use an actionindexed “next-state” modality ⟨a, I⟩α to specify that the next action of the component in question is labelled a and the time since it last performed an action lies in the interval I. Further, the formula α is true in the resulting state. We give automata-theoretic solutions for the satisfiability and model checking problems for this specification language. This involves constructing a product interval automaton for a given TLTL^{⊗} formula, which recognizes exactly the models of the given formula.

One the contributions of this thesis is the technique used for reasoning about timed automata in terms of classical untimed systems. We show that our automata can be represented symbolically using the notion of a “proper” symbolic alphabet. As a result we can reason about the timed languages of these automata using powerful techniques available in Mazurkiewicz trace theory and automata theory.

As an application of the theory developed here, we use product interval automata to model asynchronous circuits. These are circuits in which there is no common clock pulse which controls the switching of the gates in the circuit. Traditionally, these circuits are considered difficult to design and analyse. Maler and Pnueli [MP95] used a network of timed automata which communicate through shared memory to analyse the behaviour of these circuits. We show that product interval automata suffice to model this class of timed behaviours. In conjunction with TLTL^{⊗}, we can specify and verify some useful properties of these circuits.

A final feature of these automata is that they are well-suited to the application of the recently proposed partial order reduction methods for timed systems [BJ+98, M99]. The method is explained briefly below.

Partial order based reduction methods [V92, KP92, G96] are an established way of tackling the so-called state explosion problem in the verification of distributed systems. The state explosion problem arises due to the fact that a distributed system may have a small description in terms of each of its components, but the actual global state space of the system could be exponentially large in the description of the components. This “explosion” of states can be prohibitively large for verification tools to handle. The partial order based reduction methods aim to tackle this problem by exploiting the structure in the global transition system. They make use of the fact that for certain “trace invariant” properties, it is sufficient to examine just one of the

a (x < 1)  b(y > 1)

Figure 1.3: Causality introduced by timing constraints.

several interleaved runs corresponding to a single partially ordered computation of a distributed system. This often leads to a substantial reduction in the search space for the verification algorithms.

In the presence of timing constraints, however, this independence is destroyed since actions can be locationally independent but still forced into a causal order due to the timing constraints. In the Fig. 1.3 assume that the two components have just synchronised and reset their clocks, so that x = y = 0. Now even if a and b are independent, a is forced to occur before b due to the timing constraints.

Recently Bengtsson et al. [BJ+98] proposed a local-time semantics for networks of timed automata, where the local clocks of each automaton are allowed to progress independently of clocks in other components. Before each synchronising action, the participating components must ensure that the time elapsed locally for each of them are the same. This new semantics preserves the behaviour of the timed system provided we consider only such “synchronised” runs.

In this local time semantics, locationally independent actions are now also independent in the semantic transition system. However we are more interested in their independence in the quotiented transition system (the region or zone automaton) as it is this transition system which is searched during verification. In general, the locational independence may not imply independence in the quotiented transition system, and one has to examine the current region or zone to make sure the transitions don’t disable each other. In [M99] Minea shows that for a certain class of systems called “syncreset” systems in which each component has a single clock which is reset with every action that the component takes part in, locational independence does mean independence in the zone automaton as well.

Product interval automata are indeed instances of such sync-reset systems, and hence systems which are modelled using these automata are amenable to the efficient application of these methods.

However, these methods are still in a nascent stage and the actual gains have not been quantified. The hope is however that although more behaviour is added by the desynchronisation of clocks, the number of zones will turn out to be fewer. This, coupled with the reductions obtained by partial order based methods, is expected to lead to more efficient verification of timed systems.

1.4 Related Work

Subclasses of timed automata

As mentioned earlier, the property of our automata which make them determinizable is that they refer to implicit clocks only, which are reset in a uniform way. In fact it is not difficult to see that we can determinize a general timed automaton using just the classical techniques for determinizing and complementing classical automata, provided the resetting of clocks along transitions is determined solely by the input word.

Some important subclasses of timed automata have been proposed earlier based on this idea. In [AFH94] Alur, Fix and Henzinger proposed a subclass of timed automata called event recording automata. For each action a there is an implicit clock x_{a} which is reset with each occurrence of that action. Thus the clock x_{a} records the time elapsed since the last occurrence of the action a. The authors go on to show that a larger class of automata can be obtained by having another implicit clock for each action, called an event predicting clock, which keeps track of the time yet to elapse before the next occurrence of the action. This class, obtained by using both recording and predicting clocks, is called event clock automata.

These automata were further generalised in [HRS98] to allow the use of recording and predicting clocks for an arbitrary automaton. Roughly speaking, if an automaton A is thought of as running on a given timed word σ starting at time t, then the clock x_{A} records the last time t′ at which A accepted σ starting at t′. This class of automata is called recursive event clock automata.

All three classes above were shown to be closed under boolean operations. In terms of modelling power, event recording automata—expressively the weakest of the three—are believed to be sufficiently powerful.

The classes product interval automata and distributed interval automata which we introduce are less expressive than event recording automata. However, our cellular interval automata have the same expressive power as event recording automata.

Another related piece of work is by Jonsson and Yi [YJ94] in the setting of timed CSP. They show that language inclusion problem is decidable for a class of automata similar to product interval automata, but where the delays are constants and not intervals. We show a variety of results about product interval automata which subsume this result.

Logical characterisations

The logical characterisations we give in this thesis are similar in flavour to Wilke’s characterisation of timed automata via the logic L d^{↔} [W94]. L d^{↔}, called the monadic second order logic of relative distance, is interpreted over timed words in much the same way as Büchi’s MSO for classical words, and is shown to characterise the class of timed languages accepted by timed automata.

However, the fact that timed automata are not closed under complement is reflected in the fact that L d^{↔} is not a full monadic second order logic. It places syntactic restrictions on the formulas, particularly on the use of existential quantification over set variables.

In [HRS98] the authors give a logical characterisation of recursive event clock automata. Once again, their logic, called MinMaxML is not a full monadic second order logic, with the second order quantification being restricted. This is due to the fact that recursive event clock automata are not closed under geometric projection.

In contrast to these characterisations, our automata have full monadic second order logic characterisations. Further, we show that we can extend our methods to obtain a logical characterisation for event recording automata. A logical characterisation along the same lines for event clock automata is worked out in [DH99].

Timed temporal logics

Several temporal logics proposed for use as specification languages for timed systems turn out to be undecidable when interpreted over a dense time domain [AH93]. We discuss here two logics which are known to have decidable satisfiability problems—the Metric Interval Temporal Logic (MITL) of Alur, Feder and Henzinger, and the Event Clock Temporal Logic of Raskin and Schobbens. In fact it was shown recently in [HRS98] that both logics have the same expressive power, albeit differing complexities of decision procedures. In addition, MITL and EventClock TL are shown to be expressively equivalent to the first order fragment of MinMaxML, the monadic second order logic characterising recursive event clock automata.

MITL was introduced in [AFH96]. The logic uses an interval-indexed version of the “until” modality U_{I} which constrains formulas to be satisfied during the specified period. For example, the formula □(p ⇒ ◇_{[1,2]}q) says that at all points t in the timed word, whenever p is true at t, there is a later point t′ in the word where q is true, and t′ − t ∈ [1, 2]. MITL restricts the interval I to be non-singular, i.e. I should not of the form [c, c]. In the absence of this restriction, the logic is shown to be undecidable.

Satisfiability of MITL formulas are shown to be EXPSPACE-complete, while the fragment of MITL which uses intervals which either begin at 0 or end at ∞—called MITL_{0,∞}—is equally expressive [HRS98] and is PSPACEcomplete.

In [RS97] Raskin and Schobbens define a timed temporal logic based on event clock automata called State Clock Logic and later called Event Clock Temporal Logic in [HRS98]. Along with the usual “until” operator, they have “history” and “prophesy” operators. The history operator is of the form ◁_{I}α and means that the formula α was last true t time units ago, for some t ∈ I. The prophesy operator ▷_{I} has a similar interpretation.

The problem of deciding satisfiability of an Event Clock Logic formula is shown to be PSPACE-complete [HRS98]. In both MITL and Event Clock Logic, the satisfiability problem is solved along the lines of classical LTL, by defining a timed automaton (in the case of Event Clock Logic, an event clock automaton) which recognizes exactly the models of the given formula. In both cases the number of clocks used is proportional to the length of the given formula.

The temporal logic we study, TLTL^{⊗}, is less expressive than MITL. Our main motivation for examining TLTL^{⊗} is that it is the natural temporal logic suggested by TMSO^{⊗}, our monadic second order logic characterising product interval automata. As we show, TLTL^{⊗} is expressively equivalent to the first order fragment of TMSO^{⊗}.

The satisfiability of TLTL^{⊗} is also PSPACE-complete. TLTL^{⊗} has one advantage, however, in that the number of clocks in its formula automata is equal to the number of components in the system, whereas for both MITL and Event Clock Logic it is proportional to the size of the given formula.

Results from trace theory

This thesis draws on several well-known results from the theory of distributed systems. We summarise these results here.

Regular trace languages were studied by Mazurkiewicz as a way of describing the behaviour of distributed systems. Zielonka gave an automata theoretic characterisation of regular trace languages using asynchronous automata, and asynchronous cellular automata [Z87]. This characterisation was later extended to ω-regular trace languages, using asynchronous Büchi automata by Gastin and Petit [GP92].

Diekert and Muscholl [DM94] showed that asynchronous Büchi automata are equivalent to deterministic asynchronous Muller automata, and hence are closed under complementation. Muscholl [M94] later gave a direct construction for the complementation of asynchronous Büchi automata. However this did not involve determinizing these automata. Independently, Klarlund, Mukund, and Sohoni [KMS95] gave a direct determinization construction for Büchi asynchronous automata.

In terms of logical definability, Thomas [Tho89] gave a logical characterisation of regular trace languages in terms of a monadic second order logic interpreted over traces represented as labelled partial orders. This result was later extended to ω-regular trace languages by Ebinger and Muscholl [EM96].

The closure properties of regular product languages, a subclass of regular trace languages, are studied by Thiagarajan in [Thi95]. The logic product-LTL is proposed in this paper as a way of specifying trace invariant properties of distributed systems. The satisfiability and model checking problems for this logic are also solved.

1.5 Organisation of the thesis

The material in this thesis is organised as follows. We begin with interval automata, which are the component automata for product interval automata. After introducing the preliminary notions about timed words and timed automata, we define interval automata, and go on to show that they are closed under boolean operations. Finally we exhibit a simple logical characterisation of these timed languages.

The study of interval automata helps us while dealing with product interval automata in Chapter 3. We define these automata and the timed languages accepted by them and show that they are more expressive than interval automata. We show how these automata can be simulated by timed automata. This gives us a way of checking whether the language accepted by a given product interval automaton is empty or not. Next we show that these languages are closed under boolean operations. Finally, we present TMSO^{⊗}, a monadic second order logic which characterises product interval languages.

In Chapter 4 we introduce the timed temporal logic TLTL^{⊗} and study its satisfiability and model checking problems. The chapter ends with a proof of the fact that TLTL^{⊗} is expressively equivalent to the first order fragment of TMSO^{⊗}, the logic characterising product interval automata.

Chapter 5 is devoted to the modelling of asynchronous circuits using product interval automata. We describe the behaviour of a circuit as a timed language over an appropriate alphabet, and show that we can define a product interval automaton which accepts this language. We also give some properties which we can verify using this model in conjunction with the logic TLTL^{⊗}.

We introduce distributed interval automata in Chapter 6. We show that the class of languages accepted by these automata are closed under boolean operations. This chapter contains two detailed sections on a logical characterisation of these languages. We first show that distributed interval languages can be represented as timed trace languages. We then give a logical characterisation of these timed trace languages.

In Chapter 7 we study cellular interval automata, the cellular version of distributed interval automata. To reason about the languages accepted by these automata, we introduce what we call quasi cellular asynchronous automata and show that they have the same expressive power as asynchronous automata. This helps us to show that cellular interval languages are closed under boolean operations, and also that they admit a logical characterisation. Finally we show how these languages are related to event recording automata, and how the techniques introduced this far help us to give a logical characterisation for event recording automata.

We conclude with Chapter 8, where we summarise our results and detail some avenues for further research.

Interval Automata

In this chapter we introduce a restricted class of timed automata called interval automata. These automata have a single clock which is reset along every transition. Effectively, these automata can only measure the time elapsed since the last action performed. As a result, these automata are fairly weak in terms of expressiveness.

However, the class of languages accepted by these automata enjoys some nice closure properties. It is closed under boolean operations and, in addition, admits a simple logical characterisation in terms of a monadic second order logic interpreted over timed words. The techniques introduced here are representative of many of the techniques used subsequently in the thesis. The results too will play an important role, particularly in the next chapter where we deal with product interval automata which are essentially networks of interval automata.

In this chapter we first introduce some preliminary notions about timed words and timed automata. We sketch the construction of the region automata for these automata. We then introduce interval automata and answer some natural questions about them. In particular, we show that the class of languages accepted by these automata are closed under boolean operations. Finally, in Section 2.5 we provide a logical characterisation of these languages.

2.1 Preliminary notions

As usual, for an alphabet A we will use A^{∗} and A^{ω} to denote the set of finite and infinite words over A respectively. We will use A^{∞} to denote the set A^{∗} ∪ A^{ω}.

It will be necessary for us to deal with both finite and infinite words, and in this regard it is convenient to use prefixes to play the role of positions in the word. For a word σ in A^{∞}, prf (σ) will be used to denote the set of finite prefixes of σ. The strict and non-strict prefix relations on finite words will be denoted by ≺ and ⪯ respectively. We will use |σ| to denote the length of a word σ. The empty word will be denoted by ϵ.

Büchi automata

It will be helpful to recall the definition of Büchi automata. The reader is referred to [Tho90] for a comprehensive treatment of this subject.

Definition 2.1 Let A be a finite alphabet. A (mixed) Büchi automaton over the alphabet A is a structure A = (Q, ⟶, Q_{in}, F, G) where

• Q is a finite set of states,

• ⟶⊆ Q × A × Q is the transition relation,

• Q_{in} ⊆ Q is a set of initial states, and

• F, G ⊆ Q are, respectively, the finitary and infinitary acceptance state sets.

Let σ ∈ A^{∞}. A run of A over σ is a map ρ : prf (σ) → Q which satisfies:

• ρ(ϵ) ∈ Q_{in}.

• ρ(τ) ⟶^{a} ρ(τa) for every τa ∈ prf (σ). (q ⟶^{a} q′ is alternate notation for (q, a, q′) ∈⟶).

We say ρ is an accepting run on σ iff either

• σ is finite and ρ(σ) ∈ F, or,

• σ is infinite and ρ(τ) ∈ G for infinitely many τ ∈ prf (σ).

The set of words accepted by A, denoted L_{sym}(A), is defined to be the set of words in A^{∞} on which A has an accepting run. Following established convention, we term a subset L of A^{∞} regular if L = L_{sym}(A) for some Büchi automaton A over A.

It will be convenient for us to sometimes use a generalised Büchi automaton. This is a Büchi automaton in which the infinitary acceptance set is replaced by a family of accepting sets G = {G_{1}, …, G_{m}} with m ≥ 0. Let A = (Q, ⟶, Q_{in}, F, G) be a generalised Büchi automaton, with G = {G_{1}, …, G_{m}} (m ≥ 0). Then a run ρ on a word σ ∈ A^{∞} is defined as done for a Büchi automaton. We say that ρ is accepting iff either • σ is finite and ρ(σ) ∈ F, or,

• σ is infinite and for each i ∈ {1, …, m}, ρ(τ) ∈ G_{i} for infinitely many τ ∈ prf (σ).

A generalised Büchi automaton can be converted to a standard Büchi automaton as follows. Let A be the generalised Büchi automaton above. Define A′ = (Q′, ⟶′, Q′_{in}, F′, G′) where

• Q′ = Q × {0, 1, …, m}

• ⟶′ is given by (q, l) ⟶′^{a} (q′, l′) iff

– q ⟶^{a} q′

– l′ = (l + 1) mod (m + 1) if q′ ∈ G_{l} or l = 0. Otherwise l′ = l.

• Q′_{in} = Q_{in} × {0}.

• F′ = F × {0, …, m}

• G′ = Q × {0}.

It is not difficult to verify that L_{sym}(A) = L_{sym}(A′). We observe that the simulation involves a blow-up of O(m) in the number of states of A.

The problem of checking whether the language accepted by a Büchi automaton is empty can be efficiently solved. This can be done by checking that the language of finite words is empty and that the language of infinite words is empty. The language of finite words is empty iff there is no finitary final state reachable from a start state. The language of infinite words is empty iff there is no cycle (in the underlying graph of the automaton) containing an infinitary final state and reachable from a start state. Both these checks can be carried out by well-known linear time algorithms.

Timed automata

The notion of a timed word is central to this thesis. In what follows we will use ℝ^{>0} and ℝ^{≥0} to denote the set of positive and non-negative reals respectively. The non-negative rationals will be denoted by ℚ^{≥0}.

Definition 2.2 Let Σ be a finite alphabet of actions. A timed word over Σ is a member σ of (Σ × ℝ^{>0})^{∞} such that

1. for all prefixes τ(a, t)(b, t′) of σ we have t < t′ (strict monotonicity).

2. if σ is infinite, then for each t ∈ ℝ^{>0} there exists a prefix τ(a, t′) of σ such that t′ > t (progressiveness).

We use T Σ^{∗} and T Σ^{ω} to denote the set of finite and infinite timed words over Σ, respectively, and set T Σ^{∞} = T Σ^{∗} ∪ T Σ^{ω}.

For a finite timed word τ we will use time(τ) to denote the time of occurrence of the last action in τ. Formally, time(ϵ) = 0, and time(τ(a, t)) = t. Analogously, for a non-empty finite timed word τ we will use action(τ) to denote the last action in τ.

Wherever convenient, we will also use the representation of a timed word σ as a pair (α, η) where α ∈ Σ^{∞} and η : prf (α) → ℝ^{>0}. For an infinite timed word σ we will also sometimes use the representation of σ as (α, η) where α ∈ Σ^{ω} and η : ℕ − {0} → ℝ^{>0}. Here ℕ is the set of natural numbers {0, 1, …}.

In what follows, we will use intervals with rational bounds to specify timing constraints (and use ∞ as the upper bound to capture unbounded intervals). These intervals will be of the form (l, r), [l, r), (l, r], or [l, r], where l, r ∈ ℚ^{≥0} ∪ {∞} with l ≤ r. For an interval of the form (l, r] or [l, r] we require r ≠ ∞. Further, to avoid empty intervals, unless an interval is of the form [l, r], we require l < r. An interval will denote a non-empty, convex subset of reals in the obvious way. For example the interval [1, ∞) denotes the set {t ∈ ℝ | 1 ≤ t}. The set of all intervals will be denoted by Iℝ.

Definition 2.3 A (mixed) timed Büchi automaton, TBA for short, over an alphabet Σ is a structure B = (Q, ⟶, C, Q_{in}, F, G) where:

• Q is a finite set of states,

• Q_{in} ⊆ Q is a set of initial states,

• F, G ⊆ Q are sets of finitary and infinitary accepting states,

• C is a finite set of clocks, and

• ⟶, the transitions of B, is a finite subset of Q×Σ×2^{C} ×G_{C} ×Q where G_{C} is the set of clock constraints (guards) which are conjunctions of atomic guards of the form (x ∈ I), where x ranges over C and I ranges over Iℝ.

Actually this is a mild reformulation of the one given by Alur and Dill in [AD94] and it involves no loss of generality. In what follows a transition (q, a, X, g, q′) will be written as q ⟶_{X}^{a, g} q′. The manner in which the timed automaton accepts a timed word is defined in terms of clock valuations.

A C-valuation is a map v : C → ℝ^{≥0}. Where C is clear from the context we will say valuation instead of C-valuation. We let val_{C} stand for the set of C-valuations. Let v be a valuation and t ∈ ℝ^{≥0}. Then v + t is the valuation given by:

(v + t)(x) = v(x) + t for every x ∈ C.

Suppose v is a valuation, t ∈ ℝ^{≥0} and X ⊆ C. Then the valuation v[t/X] is given by:

v[t/X](y) = \{ \begin{matrix}t & if y ∈ X \\ v(y) & otherwise. \end{matrix}

Finally, 0 is the null-valuation given by:

0(x) = 0 for every x ∈ C.

Next, the notion of a valuation v satisfying a clock constraint g is denoted by v ⊧ g and is defined via:

• v ⊧ x ∈ I iff v(x) ∈ I

• v ⊧ φ ∧ φ′ iff v ⊧ φ and v ⊧ φ′.

Let σ ∈ T Σ^{∞}. Then a run of B over σ is a pair of maps (ρ, ν) where ρ : prf (σ) → Q and ν : prf (σ) → val_{C} are such that the following conditions are satisfied:

• ρ(ϵ) ∈ Q_{in} and ν(ϵ) = 0

• For every τ(a, t) ∈ prf (σ), there exists a transition ρ(τ) ⟶_{X}^{a, g} ρ(τ(a, t)) such that ν(τ) + t ⊧ g and ν(τ(a, t)) = (ν(τ) + t)[0/X].

The run (ρ, ν) is an accepting run iff either

1. σ is finite and ρ(σ) ∈ F, or,

2. σ is infinite and ρ(τ) ∈ G for infinitely many prefixes τ of σ.

L(B) ⊆ T Σ^{∞} the language of timed words accepted by B is then given by:

L(B) = {σ | ∃ an accepting run of B over σ}.

For a timed word σ ∈ T Σ^{∞} let untime(σ) be the word σ̂ ∈ Σ^{∞} obtained by projecting away the time-stamps from σ. For a timed language L ⊆ T Σ^{∞}, untime(L) ⊆ Σ^{∞} will denote the set {untime(σ) | σ ∈ L}.

Alur and Dill showed the following result:

Theorem 2.4 ([AD94]) Given a timed automaton B over an alphabet Σ one can effectively construct a Büchi automaton B′ over Σ such that L(B′) = untime(L(B)).

The first step is to “normalise” the guards in B so that all intervals are integer bounded. This can be done by multiplying all the rational bounds by the least common multiple of all the denominators. This operation does not affect the untimed language of B.

The central idea in this result is the construction of the “region” automaton R(B). Let B = (Q, ⟶, C, Q_{in}, F, G). For each x ∈ C let c_{x} denote the largest interval bound appearing in a guard of the form (x ∈ I) in B. Then a clock region (w.r.t. B) is a convex subset of val_{C} given by inequalities of the form

1. For each clock x ∈ C a constraint of the form c < x < c + 1, x = c, or x > c_{x} where c is an integer such that 0 ≤ c < c_{x}.

2. For each pair of clocks x, y ∈ C, a constraint of the form x − y < c or y − x < c or x − y = c.

The number of clock regions is finite and can be seen to be bounded by

2^{O(|C|)} · |C|! · ∏_{x∈C}(c_{x} + 1)

The automaton R(B) has as its states pairs of the form (q, r) where q ∈ Q and r is a clock region. The initial states are of the form (q_{0}, r_{0}) where q_{0} ∈ Q_{in} and r_{0} is the unique region containing 0. The transition relation

of R(B) is given by: (q, r) ⟶′^{a} (q′, r′) iff there exists an edge q ⟶_{X}^{b, g} q′ in B such that b = a, there exists v ∈ r, v′ ∈ r′ and t ∈ ℝ^{>0} such that v + t ⊧ g, and v′ = (v + t)[0/X]. A state of the form (q, r) is a finitary (respectively infinitary) final state of R(B) iff q ∈ F (respectively q ∈ G) and r ∈ val_{C}.

Regions have the property that for a given region, the truth of any guard of B is invariant across the valuations in it. Further, if r′ is a time successor of r—by this we mean there exists v ∈ r and a t ∈ ℝ^{>0} such that v + t ∈ r′— then for every u ∈ r there exists t ∈ ℝ^{>0} such that u + t ∈ r′.

Using these properties of regions it is possible to show that R(B) accepts the untimed language of B provided B has the property that for every run ρ of B on a non-progressive timed word, ρ is also a run on a progressive timed word.

However, this may not be true of B in general, and one must add extra information in the states of R(B) and define an appropriate Büchi condition to make sure that the run is progressive. The resulting automaton is the automaton B′ promised in the statement of the theorem.

The size of B′ can be seen to be

O(|Q| + |E|) · 2^{O(|C|)} · |C|! · ∏_{x∈C}(c_{x} + 1)

where E is the set of transitions of B. Further, this is also an upper bound on the time needed to generate B′.

We can now check if timed language accepted by B is empty by generating B′ and checking whether the language it accepts is empty. Since B′ is a classical Büchi automaton, and its emptiness can be checked in time linear in its size. Thus, we have:

Corollary 2.5 The emptiness of the timed language accepted by a TBA B can be checked in time

O(|Q| + |E|) · 2^{O(|C|)} · |C|! · ∏_{x∈C}(c_{x} + 1),

where Q and E are the state and edge sets of B respectively, C is the set of clocks used in B, and for each x ∈ C, c_{x} is the largest normalised interval bound appearing in B in a guard of the form (x ∈ I).

Using standard convention we let |B| denote the size of the representation of B, using binary encoding for the numeric constants. Then the above expression can be seen to bounded by 2^{(|B|^{2})}.

2.2 Interval automata and their languages

The notion of an interval alphabet will be useful in representing timed languages symbolically. Let Σ be a finite alphabet. Then an interval alphabet based on Σ is a finite subset of Σ × Iℝ.

Given an interval alphabet Γ over Σ and a word σ̂ ∈ Γ^{∞}, σ̂ naturally induces a set of timed words over Σ which we will denote tw(σ̂). It is defined as follows. Let σ ∈ T Σ^{∞}. Then σ ∈ tw(σ̂) iff

1. |σ| = |σ̂|.

2. For each prefix τ(a, t) of σ, and for each prefix τ̂(b, I) of σ̂ such that |τ| = |τ̂|, we have a = b and t − time(τ) ∈ I.

q_{0}  q_{1} ⟹ (a, [1, 1])  (a, (0, ∞)) (b, [1, 2])

Figure 2.1: An interval automaton over {a, b}.

For L ⊆ Γ^{∞} we set

tw(L) = ⋃_{σ̂∈L} tw(σ̂).

Definition 2.6 An interval automaton over Σ is simply a Büchi automaton over an interval alphabet based on Σ.

Thus an interval automaton A over Σ has edges of the form q ⟶^{(a,I)} q′, where a is a Σ-action and I is an interval. Viewed as a Büchi automaton over an interval alphabet Γ, A accepts the symbolic language L_{sym}(A) ⊆ Γ^{∞}. What is more interesting to us however, is the timed language accepted by A, denoted L(A), which we define as

L(A) = tw(L_{sym}(A)).

We will say a timed language L ⊆ T Σ^{∞} is a regular interval language if L = L(A) for some interval automaton A over Σ.

Example 2.7 Figure 2.1 shows an interval automaton A over the alphabet Σ = {a, b}. Here we have A = ({q_{0}, q_{1}}, ⟶, {q_{0}}, {q_{1}}, {q_{1}}). In the figure we use the convention that the initial states are indicated with incoming double arrows, while final states are indicated by two concentric circles. The automaton accepts all timed words σ ∈ T Σ^{∞} which begin with a (possibly empty) sequence of a actions, unit times apart, followed by a b action at some time between 1 and 2 units from the last action, and finally a sequence of a’s again, without any time restrictions. □

We can also define the notion of a run of an interval automaton directly over a timed word. Let A = (Q, ⟶, Q_{in}, F, G) be an interval automaton over Σ, and let σ ∈ T Σ^{∞}. Then a run of A on σ is map ρ : prf (σ) → Q such that

1. ρ(ϵ) ∈ Q_{in} 2. For each τ(a, t) ∈ prf (σ), there exists I, such that ρ(τ) ⟶^{(a,I)} ρ(τ(a, t))

and (t − time(τ)) ∈ I.

As usual, the run ρ will be termed accepting if either σ is finite and ρ(σ) ∈ F, or, σ is infinite and ρ(τ) ∈ G for infinitely many τ ∈ prf (σ).

It is not difficult to see that this is an equivalent way of defining the timed language of A—in the sense that σ ∈ tw(L_{sym}(A)) iff there exists an accepting run of A on σ, in the sense defined above.

2.3 Checking emptiness

The problem of checking whether the timed language accepted by an interval automaton A is empty or not, can be easily solved. We can do this by simply checking whether L_{sym}(A) is empty or not. This follows from the following proposition:

Proposition 2.8 Let Γ be an interval alphabet based on Σ such that Γ does not mention the interval [0, 0]. Let σ̂ ∈ Γ^{∞}. Then tw(σ̂) ≠ ∅.

Proof We use the fact that each I ∈ Iℝ is a non-empty subset of ℝ^{>0} provided I ≠ [0, 0]. Let voc(Γ) denote the set of intervals mentioned in Γ. Then, with each I ∈ voc(Γ) we can associate a t_{I} ∈ ℝ^{>0} such that t_{I} ∈ I. Now we can define a timed word σ ∈ T Σ^{∞} such that σ ∈ tw(σ̂). We define σ by defining its set of prefixes as follows. With every prefix of σ̂ we inductively associate a prefix of σ. With the empty prefix we associate the empty word itself. Let τ̂(a, I) be a prefix of σ̂. Then with τ̂(a, I) we associate the word τ(a, t) where τ is the prefix we have associated with τ̂, and t = time(τ) + t_{I}. We need to check that σ is progressive. So suppose σ is infinite and let t ∈ ℝ^{>0}. Let t_{0} be the minimum of the set {t_{I} | I ∈ voc(Γ)}. (Note that the set is finite and hence we can speak of the minimum.) Let τ be the prefix of σ such that |τ| > t/t_{0}. (Such a τ exists by the Archimedian property of ℝ.) Then it is clear that time(τ) > t. Thus σ ∈ T Σ^{∞} and, by construction, σ ∈ tw(σ̂). □

Now, a symbolic word σ̂ which contains a letter of the form (a, [0, 0]) cannot give rise to a timed word and we have tw(σ̂) = ∅. Thus, if A uses the interval [0, 0], we can simply drop all the edges in A labelled by this interval, without affecting the timed language accepted by A. Thus, we can assume without loss of generality that A is over an interval alphabet Γ which does not make use of the interval [0, 0]. Checking emptiness of L(A) is then reduced to checking emptiness of L_{sym}(A). This can be done in linear time in the size of A.

Before we close this section we show that interval automata are a subclass of Alur-Dill timed automata [AD94]. In fact they correspond to the class of timed automata which have a single clock which is reset along every edge in the automaton.

Proposition 2.9 Let L ⊆ T Σ^{∞}. Then the following statements are equivalent.

1. There exists an interval automaton A over Σ such that L = L(A).

2. There exists a TBA B over Σ with a single clock which is reset along every edge, such that L = L(B).

Proof 1 ⇒ 2: Let A = (Q, ⟶, Q_{in}, F, G) be an interval automaton over the interval alphabet Γ based on Σ. Consider the TBA B = (Q, ⟶′ , {x}, Q_{in}, F, G) where ⟶′ is given by:

q ⟶′_{{x}}^{a, (x∈I)} q′ iff q ⟶^{(a,I)} q′.

It is routine to verify that L(B) = L(A).

2 ⇒ 1: Let B = (Q, ⟶′, C, Q_{in}, F, G) be a TBA with C = {x} and with

⟶′ of the form q ⟶′_{{x}}^{a, g} q′ for some a ∈ Σ and g ∈ G_{C}. Since a conjunction

of atomic guards over a single clock can always be written as a single atomic guard, we can further assume that each clock constraint g is of the form x ∈ I. Let A be the interval automaton defined as A = (Q, ⟶, Q_{in}, F, G) where ⟶ is given by

q ⟶^{(a,I)} q′ iff q ⟶′_{{x}}^{a, (x∈I)} q′.

It is again easy to check that L(A) = L(B). □

We give here an example of a language which cannot be accepted by an interval automaton.

Lemma 2.10 Let Σ be the alphabet {a, b}. Then the timed language L over Σ given by

L = {(b, t)(a, t′)(b, t′′) ∈ T Σ^{∞} | t′′ − t > 1}

is not a regular interval language over Σ.

Proof To see this, assume that there exists an interval alphabet Γ based on Σ and L̂ ⊆ Γ^{∞} such that L = tw(L̂). Let n be the least common multiple of the denominators of the rational bounds mentioned in Γ. Then for every interval bound r ≠ ∞ mentioned in Γ, we have r = \frac{k}{n} for some non-negative integer k. Now consider the timed word σ given by:

σ = (b, 1)(a, 1 + \frac{1}{2n})(b, 2 + \frac{1}{4n}).

Clearly σ ∈ L. Hence L = tw(L̂) would imply that there exists σ̂ = (b, I)(a, I′)(b, I′′) in L̂ such that σ ∈ tw(σ̂). We now see that \frac{1}{2n} ∈ I′. Further, 1 − \frac{1}{4n} ∈ I′′ because (2 + \frac{1}{4n}) − (1 + \frac{1}{2n}) = 1 − \frac{1}{4n}.

Let I′ = ⟨l, r⟩. Since \frac{1}{2n} ∈ ⟨l, r⟩, we know that l ≤ \frac{1}{2n} and hence it must be the case that l = 0. This lets us conclude that \frac{1}{4n} ∈ I′. Now consider the timed word σ′ given by:

σ′ = (b, 1)(a, 1 + \frac{1}{4n})(b, 2).

We claim that σ′ ∈ tw(σ̂). To see this we just have to verify that 2−(1+ \frac{1}{4n}) = 1 − \frac{1}{4n} ∈ I′′ and we already know that \frac{1}{4n} ∈ I′. But then σ′ ∉ L and this is a contradiction. □

2.4 Closure under boolean operations

We now show that the class of regular interval languages is closed under boolean operations.

Closure under union is straightforward. Let L and M be two regular interval languages over Σ. Then we know there exist two interval alphabets Γ_{1} and Γ_{2} based on Σ, and regular subsets L̂ of Γ_{1}^{∞}, and M̂ of Γ_{2}^{∞}, such that L = tw(L̂) and M = tw(M̂). Now consider the alphabet Γ = Γ_{1} ∪Γ_{2} and the subset L̂ ∪ M̂ of Γ^{∞}. By classical automata theory, we know that L̂ ∪ M̂ is a regular subset of Γ^{∞}. Further, by definition of the tw map, it follows that tw(L̂ ∪ M̂) = tw(L̂) ∪ tw(M̂). Thus L ∪ M = tw(L̂) ∪ tw(M̂) is a regular interval language.

For closure under complementation the notion of a proper interval set will prove useful. This notion will also play an important role in subsequent sections.

We say a set of intervals I ⊆ Iℝ is proper if it forms a finite partition of ℝ^{≥0}. Thus, if I is a proper interval set, then for each t ∈ ℝ^{≥0} there exists an I ∈ I such that t ∈ I, and for each I, I′ ∈ I, I ∩ I′ ≠ ∅ implies I = I′. An interval alphabet Γ will be termed proper if for each a ∈ Σ the set Γ_{a} = {I | (a, I) ∈ Γ} is a proper interval set. We say an interval set I covers an interval set I′ if every interval in I′ is the union of some subset of intervals in I. Finally, an interval alphabet Γ covers the interval alphabet Γ′ if Γ_{a} covers Γ′_{a} for each a ∈ Σ.

Each interval alphabet Γ induces, in a canonical way, a proper interval alphabet, denoted prop(Γ), with the property that it covers Γ. It is given by

prop(Γ) = {(a, I) | a ∈ Σ, I ∈ prop(Γ_{a})}

where for each a, the set prop(Γ_{a}) is obtained from Γ_{a} by the procedure outlined below.

Let I be a non-empty finite set of intervals (if it is empty, we simply set prop(I) = {[0, ∞)}). Let V = {0, v_{1}, v_{2}, …, v_{n}, ∞} where for 1 ≤ i ≤ n, v_{i} ∈ V iff there exists I ∈ I with v_{i} as the left or right end of I. Without loss of generality, we assume that n ≥ 1 and 0 < v_{1} < v_{2} ⋯ < v_{n} ≠ ∞. Now define prop(I) via:

prop(I) = {[v_{j}, v_{j}], (v_{j}, v_{j+1}) | 0 ≤ j ≤ n}

where we set v_{0} = 0 and v_{n+1} = ∞. It is easy to verify that prop(I) is a proper interval set which covers I.

The following is an important property of proper interval alphabets.

Lemma 2.11 Let Γ be a proper interval alphabet based on Σ. Then for each σ ∈ T Σ^{∞} there exists a unique word σ̂ ∈ Γ^{∞} such that σ ∈ tw(σ̂).

Proof Let σ ∈ T Σ^{∞}. Since Γ is proper we know that for each a ∈ Σ and t ∈ ℝ^{>0} there exists a unique I ∈ Γ_{a} such that t ∈ I. Consider the word σ̂ ∈ Γ^{∞} given by its set of prefixes which we define as follows. For each prefix τ of σ we define a corresponding prefix τ̂ of σ̂. The prefix corresponding to ϵ is ϵ itself. The prefix corresponding to the non-empty prefix τ(a, t) of σ is τ̂(a, I) where I is the unique interval in Γ_{a} such that (t − time(τ)) ∈ I. It is easy to verify that σ ∈ tw(σ̂).

For uniqueness of σ̂ suppose σ ∈ tw(σ̂_{1}) and σ ∈ tw(σ̂_{2}) for some σ̂_{1}, σ̂_{2} ∈ Γ^{∞}. If σ̂_{1} ≠ σ̂_{2} then there must exist prefixes τ̂_{1}(a, I) of σ̂_{1} and τ̂_{2}(a, I′) of σ̂_{2}, such that |τ̂_{1}| = |τ̂_{2}| and I ≠ I′. Let τ(a, t) be a prefix of σ such that |τ| = |τ̂_{1}|. Then we know (t − time(τ)) belongs to both I and I′. Since Γ_{a} is proper, this would mean I = I′ which contradicts our assumption. Thus we must have σ̂_{1} = σ̂_{2}. □

We next observe that proper interval alphabets suffice to capture regular interval languages.

Lemma 2.12 Let Γ be an interval alphabet based on Σ and let L̂ be a regular subset of Γ^{∞}. Let Γ′ be a proper interval alphabet which covers Γ (note that prop(Γ) is at least one such alphabet). Then there exists a regular subset L̂′ of (Γ′)^{∞} such that tw(L̂′) = tw(L̂).

Proof Since L̂ is a regular subset of Γ^{∞} there exists a Büchi automaton A over Γ such that L_{sym}(A) = L̂. Let A = (Q, ⟶, Q_{in}, F, G). Consider the automaton B = (Q, ⟶′, Q_{in}, F, G) over Γ′ where ⟶′ is given by

q ⟶′^{(a,I′)} q′ iff ∃q ⟶^{(a,I)} q′ with I′ ⊆ I.

Let L̂′ = L_{sym}(B). Then it is routine to argue that tw(L̂′) = tw(L̂). □

Using properties of proper alphabets we can now show closure under complementation. Let L be an regular interval language over Σ. Without loss of generality (using Lemma 2.12), we can assume that there exists a proper interval alphabet Γ based on Σ and a regular subset L̂ of Γ^{∞} such that L = tw(L̂). We now claim that T Σ^{∞} − L = tw(Γ^{∞} − L̂). We can prove this easily using Lemma 2.11 as follows. Let σ ∈ T Σ^{∞} − L. By Lemma 2.11 we know there is a unique σ̂ ∈ Γ^{∞} such that σ ∈ tw(σ̂). Now σ̂ cannot belong to L̂, as then we would have σ ∈ tw(L̂). So σ̂ ∈ Γ^{∞} − L̂ and hence σ ∈ tw(Γ^{∞} − L̂). Conversely, let σ ∈ tw(Γ^{∞} − L̂). Then σ ∈ tw(σ̂) for some σ̂ ∉ L̂. But this would mean that σ ∉ L for otherwise the uniqueness of σ̂ would be violated. This completes the proof of the claim above.

Now since regular languages are closed under complement, we know that Γ^{∞} − L̂ is regular, and hence T Σ^{∞} − L is a regular interval language.

Closure under union and complementation tell us that regular interval languages are closed under intersection too. It will be helpful, however, to see an explicit construction of this. Let L_{1} and L_{2} be regular interval languages over Σ. So there exist interval alphabets Γ_{1} and Γ_{2}, and regular sets L̂_{1} ⊆ Γ_{1}^{∞} and L̂_{2} ⊆ Γ_{2}^{∞} such that L_{1} = tw(L̂_{1}) and L_{2} = tw(L̂_{2}). Now, let Γ = prop(Γ_{1} ∪ Γ_{2}). Applying Lemma 2.12 we know that there exist regular subsets M̂_{1} and M̂_{2} of Γ^{∞} such that L_{1} = tw(L̂_{1}) = tw(M̂_{1}) and L_{2} = tw(L̂_{2}) = tw(M̂_{2}). We now claim that L_{1} ∩ L_{2} = tw(M̂_{1} ∩ M̂_{2}). This is again easy to verify using Lemma 2.11 and an argument similar to the complementation case above. Since M̂_{1} ∩ M̂_{2} is regular, we conclude that L_{1} ∩ L_{2} is a regular interval language.

The results above are summarised in the following theorem:

Theorem 2.13 The class of regular interval languages over an alphabet Σ is closed under the boolean operations of union, intersection and complementation. □

2.5 A logical characterisation

In this section we introduce a monadic second order logic interpreted over timed words, which characterises the class of regular interval languages. This logic is called TMSO(Σ) and is parameterised by the alphabet Σ.

Here and in the logics to follow, we assume a supply of individual variables x, y, …, and set-variables X, Y, . . .. These variables will range over prefixes (respectively sets of prefixes) of the timed word in question. We will make use of the predicates Q_{a}(x) (one for each a ∈ Σ) and Δ(x, I), where x is an individual variable and I is an element of Iℝ. The syntax of TMSO(Σ) is given by:

φ ::= (x ∈ X) | (x < y) | Q_{a}(x) | Δ(x, I) | ¬φ | (φ ∨ φ) | ∃xφ | ∃Xφ.

A structure for a formula of the logic will be a pair (σ, 𝕀) where σ ∈ T Σ^{∞} and 𝕀 is an interpretation which assigns to each individual variables a prefix of σ, and to each set variable a set of prefixes of σ. We depart slightly from classical monadic logics by using prefixes instead of natural numbers to play the role of positions in a word. Once again, this is more convenient for us given that we are dealing with both finite and infinite words. Correspondingly, < will be interpreted as the the strict prefix relation ≺ on finite words.

The satisfaction relation σ ⊧_{𝕀} φ for atomic formulas φ is given as follows:

σ ⊧_{𝕀} (x ∈ X) iff 𝕀(x) ∈ 𝕀(X)
σ ⊧_{𝕀} (x < y) iff 𝕀(x) ≺ 𝕀(y)
σ ⊧_{𝕀} Q_{a}(x) iff action(𝕀(x)) = a
σ ⊧_{𝕀} Δ(x, I) iff 𝕀(x) is of the form τ(a, t) and (t − time(τ)) ∈ I.

The operators ¬, ∨, and the existential quantifiers ∃x and ∃X are interpreted in the usual manner, as described below. Let 𝕀 be an interpretation for variables with respect to σ. Let τ be a prefix of σ. We will use the notation 𝕀[τ/x] to denote the interpretation which maps x to τ and agrees with 𝕀 on all other individual and set variables. Similarly, for a set of prefixes S of σ, the notation 𝕀[S/X] will denote the interpretation which sends X to S, and agrees with 𝕀 on all other variables.

σ ⊧_{𝕀} ¬φ  iff σ |̸=_{𝕀} φ
σ ⊧_{𝕀} (φ ∨ φ′) iff σ ⊧_{𝕀} φ or σ ⊧_{𝕀} φ′
σ ⊧_{𝕀} ∃xφ  iff there exists τ ⪯ σ such that σ ⊧_{𝕀[τ/x]} φ
σ ⊧_{𝕀} ∃Xφ  iff there exists S ⊆ prf (σ) such that σ ⊧_{𝕀[S/X]} φ.

Given a sentence φ in TMSO(Σ) we define L(φ) = {σ ∈ T Σ^{∞} | σ ⊧ φ}.

Example 2.14 Let Σ = {a, b}. Then the following TMSO(Σ)-sentence describes the language accepted by the automaton A in Example 2.7.

φ_{1} = ∃x(Q_{b}(x) ∧ Δ(x, [1, 2]) ∧
∀y((y < x) ⇒ (Q_{a}(y) ∧ Δ(y, [1, 1]))) ∧
∀y((x < y) ⇒ Q_{a}(y))).
□

Theorem 2.15 Let L ⊆ T Σ^{∞}. Then L is a regular interval language iff L = L(φ) for some sentence φ in TMSO(Σ).

We will devote the rest of this section to the proof of this theorem. We begin with Büchi’s monadic second order logic characterisation of regular languages, which we will make use of crucially. We recall that for an alphabet A, Büchi’s monadic second order logic (denoted here by MSO(A)) is given as follows:

φ ::= (x ∈ X) | (x < y) | Q_{a}(x) | ¬φ | (φ ∨ φ) | ∃xφ | ∃Xφ.

A structure for this logic is a pair of the form (σ, 𝕀) where σ ∈ A^{∞} and 𝕀 assigns to individual and set variables, non-empty prefixes and sets of non-empty prefixes of σ respectively. The semantics of the logic is given in a similar manner to that of TMSO(Σ). In particular, the atomic formula Q_{a}(x)—here a is required to be in A—is interpreted as follows:

σ ⊧_{𝕀} Q_{a}(x) iff 𝕀(x) = τa for some τ ⪯ σ.

As usual, for a sentence φ in MSO(A) we set

L(φ) = {σ ∈ A^{∞} | σ ⊧ φ}.

Büchi’s result states that a language L ⊆ A^{∞} is accepted by a Büchi automaton over the alphabet A iff L = L(φ) for some sentence φ in MSO(A).

Now, given a formula φ ∈ TMSO(Σ) we show how to translate it to a formula t-s(φ) ∈ MSO(Γ), for a suitably defined interval alphabet Γ. The translation will preserve—in a sense to be made precise—the timed models of φ. (The name t-s is a mnemonic for “timed-to-symbolic”.) Let Γ be any proper interval alphabet over Σ such that for each a ∈ Σ, Γ_{a} covers

voc(φ) = {I | φ has a subformula of the form Δ(x, I)}.

Note that Σ × prop(voc(φ)) is at least one such Γ. Then t-s(φ) (w.r.t. Γ) is obtained from φ by replacing sub-formulas of the form Q_{a}(x) by the formula

⋁_{(b,I)∈Γ, b=a} Q_{(b,I)}(x),

and sub-formulas of the form Δ(x, I) by the formula

⋁_{(a,I′)∈Γ, I′⊆I} Q_{(a,I′)}(x).

Lemma 2.16 Let φ ∈ TMSO(Σ) and let Γ be a proper interval alphabet based on Σ with the property that for each a ∈ Σ, Γ_{a} covers voc(φ). Let σ̂ ∈ Γ^{∞} and σ ∈ T Σ^{∞} be such that σ ∈ tw(σ̂). Suppose further that 𝕀 is an interpretation for variables with respect to σ, and 𝕀̂ is the corresponding interpretation for variables w.r.t. σ̂, given by 𝕀̂(x) = τ̂ where τ̂ ⪯ σ̂ such that |τ̂| = |𝕀(x)|, and 𝕀̂(X) = {𝕀̂(x) | x ∈ X}. Then

1. σ ⊧_{𝕀} φ iff σ̂ ⊧𝕀̂ t-s(φ).

2. If φ is a sentence, then L(φ) = tw(L(t-s(φ)).

Proof

1. We prove the statement by induction on the structure of φ. We begin with the atomic formulas as base cases.

Case φ = (x ∈ X): We know σ ⊧_{𝕀} (x ∈ X) iff 𝕀(x) ∈ 𝕀(X). This in turn is true iff 𝕀̂(x) ∈ 𝕀̂(X), which is true iff σ̂ ⊧𝕀̂ (x ∈ X).

Case φ = (x < y): We know σ ⊧_{𝕀} (x < y) iff 𝕀(x) ≺ 𝕀(y). But this is true iff 𝕀̂(x) ≺ 𝕀̂(y), which is true iff σ̂ ⊧𝕀̂ (x < y).

Case φ = Q_{a}(x): We know σ ⊧_{𝕀} Q_{a}(x) iff action(𝕀(x)) = a. But since σ ∈ tw(σ̂), we know that this holds iff 𝕀̂(x) = τ̂(a, I) for some τ̂ and I such that (a, I) ∈ Γ. This in turn holds iff σ̂ ⊧𝕀̂ ⋁_{(b,I)∈Γ, b=a} Q_{(b,I)}(x).

Case φ = Δ(x, I): Let σ ⊧_{𝕀} Δ(x, I). Then we know that 𝕀(x) = τ(a, t) for some τ, a, t such that (t − time(τ)) ∈ I. Further, since σ ∈ tw(σ̂), we know that 𝕀̂(x) = τ̂(a, I′) for some I′ such that (a, I′) ∈ Γ, and (t − time(τ)) ∈ I′. Using the fact that Γ is proper and covers voc(φ), and (t − time(τ)) ∈ I ∩ I′, it must be the case that I′ ⊆ I. Hence

σ̂ ⊧𝕀̂ ⋁_{(a,I′)∈Γ, I′⊆I} Q_{(a,I′)}(x).

Conversely, let

σ̂ ⊧𝕀̂ ⋁_{(a,I′)∈Γ, I′⊆I} Q_{(a,I′)}(x).

Then 𝕀̂(x) = τ̂(a, I′) for some (a, I′) ∈ Γ with I′ ⊆ I. Since σ ∈ tw(σ̂) it must be the case that 𝕀(x) = τ(a, t) such that (t − time(τ)) ∈ I′. Thus (t − time(τ)) ∈ I, and it follows that σ ⊧_{𝕀} Δ(x, I).

For the induction step, assume the statement holds for formulas φ′ and φ′′.

Case ¬φ′: σ ⊧_{𝕀} ¬φ′ iff σ |̸=_{𝕀} φ′. By the induction hypothesis, this holds iff σ̂ |̸=𝕀̂ t-s(φ′). Since ¬t-s(φ′) = t-s(¬φ′), this holds iff σ̂ ⊧𝕀̂ t-s(¬φ′).

Case (φ′ ∨ φ′′): σ ⊧_{𝕀} (φ′ ∨ φ′′) iff σ ⊧_{𝕀} φ′ or σ ⊧_{𝕀} φ′′. By the induction hypothesis, this holds iff σ̂ ⊧𝕀̂ t-s(φ′) or σ̂ ⊧𝕀̂ t-s(φ′′). Since t-s(φ′ ∨ φ′′) = (t-s(φ′) ∨ t-s(φ′′)), this holds iff σ̂ ⊧𝕀̂ t-s(φ′ ∨ φ′′).

Case ∃xφ′: σ ⊧_{𝕀} ∃xφ′ iff there exists a prefix τ of σ such that σ ⊧_{𝕀[τ/x]} φ′. Let τ̂ be the prefix of σ̂ such that |τ̂| = |τ|. By the induction hypothesis, it follows that σ̂ ⊧_{𝕀̂[τ̂/x]} t-s(φ′). Once again, since t-s(∃xφ′) = ∃x(t-s(φ′)), this holds iff σ̂ ⊧𝕀̂ t-s(∃xφ′).

Case ∃Xφ′: σ ⊧_{𝕀} ∃Xφ′ iff there exists a set of prefixes S of σ such that σ ⊧_{𝕀[S/X]} φ′. Let Ŝ be the set of prefixes of σ̂ given by {τ̂ | τ ∈ S, |τ̂| = |τ|}. By the induction hypothesis, it follows that σ̂ ⊧_{𝕀̂[Ŝ/X]} t-s(φ′). Once again, since t-s(∃Xφ′) = ∃X(t-s(φ′)), this holds iff σ̂ ⊧𝕀̂ t-s(∃Xφ′).

2. This is easy to see once we have (1) above. Let σ ⊧ φ. Then, again using properties of proper alphabets, there exists a σ̂ ∈ Γ^{∞} such that σ ∈ tw(σ̂). Using (1) above, we have σ̂ ∈ L(t-s(φ)) and hence σ ∈ tw(L(t-s(φ))). Conversely, if σ ∈ tw(σ̂) and σ̂ ⊧ t-s(φ), then by (1) again we have that σ ⊧ φ, and hence σ ∈ L(φ).

□

We now show how we can associate a formula s-t(φ̂) ∈ TMSO(Σ) with a formula φ̂ ∈ MSO(Γ), such that the translated formula preserves timed models. The formula s-t(φ̂) is obtained by replacing atomic sub-formulas in φ̂ of the form Q_{(a,I)}(x) by the formula

Q_{a}(x) ∧ Δ(x, I).

We show the following result:

Lemma 2.17 Let Γ be a proper interval alphabet based on Σ and let φ̂ ∈ MSO(Γ). Let σ̂ ∈ Γ^{∞} and σ ∈ T Σ^{∞} such that σ ∈ tw(σ̂). Suppose further that 𝕀̂ is an interpretation for variables w.r.t. σ̂ and let 𝕀 be the corresponding interpretation w.r.t. σ—i.e. 𝕀(x) = τ, where τ ⪯ σ such that |τ| = |𝕀̂(x)|, and similarly for set variables. Then

1. σ ⊧_{𝕀} s-t(φ̂) iff σ̂ ⊧𝕀̂ φ̂.

2. If φ is a sentence, then we have L(s-t(φ̂)) = tw(L(φ̂)).

Proof

1. We proceed by induction on the structure of φ̂.

Case φ̂ = Q_{(a,I)}(x): Thus s-t(φ̂) = Q_{a}(x) ∧ Δ(x, I). Let σ ⊧_{𝕀} Q_{a}(x) ∧ Δ(x, I). Then action(𝕀(x)) = a and 𝕀(x) is of the form τ(a, t) with (t − time(τ)) ∈ I. But this would imply that 𝕀̂(x) = τ(a, I′) for some I′ such that (t − time(τ)) ∈ I′. Since Γ is proper, this would mean I = I′. Hence σ̂ ⊧𝕀̂ Q_{(a,I)}(x).

Conversely if σ̂ ⊧𝕀̂ Q_{(a,I)}(x) then we know that 𝕀̂(x) = τ̂(a, I) for some τ̂. But since σ ∈ tw(σ̂) we must have 𝕀(x) = τ(a, t) for some τ, t such that (t − time(τ)) ∈ I. This means that σ ⊧_{𝕀} Q_{a}(x) ∧ Δ(x, I).

The remaining cases are routine.

2. For a sentence φ̂ to prove that L(s-t(φ̂)) = tw(L(φ̂)), let σ ⊧ s-t(φ̂). Then, since Γ is a proper alphabet, there exists a σ̂ ∈ Γ^{∞} such that σ ∈ tw(σ̂). By (1) above, we know that σ̂ ⊧ φ̂. Thus σ̂ ∈ L(φ̂) and σ ∈ tw(L(φ̂)).

Conversely, suppose σ ∈ tw(L(φ̂)). Then σ ∈ tw(σ̂) for some σ̂ ∈ Γ^{∞} such that σ̂ ⊧ φ̂. By (1) again, we know that σ ⊧ s-t(φ̂), and hence σ ∈ L(s-t(φ̂)).

□

We are now in a position to provide a proof of Theorem 2.15. Let L be a regular interval language over Σ. Using Lemma 2.12 we know that there exists a proper interval alphabet Γ based on Σ and a regular subset L̂ of Γ^{∞} such that L = tw(L̂). Büchi’s theorem tells us that there exists an MSO(Γ)- sentence φ̂ such that L(φ̂) = L̂. Hence L = tw(L(φ̂)). Thus, by Lemma 2.17, we have a TMSO(Σ)-sentence, namely φ = s-t(φ̂), such that L = L(φ).

Conversely, let φ be a TMSO(Σ)-sentence. Then, using Lemma 2.16, we know that there exists a proper interval alphabet Γ and a formula φ̂ = t-s(φ) in MSO(Γ), such that L(φ) = tw(L(φ̂)). Using Büchi’s theorem once more, we are assured of an interval automaton A over Γ such that L_{sym}(A) = L(φ̂). Thus A is such that

L(A) = tw(L_{sym}(A)) = tw(L(φ̂)) = L(φ).

This completes the proof of the theorem.

Product interval automata

As seen in the last chapter, the class of interval automata are a rather restricted class of timed automata which can be captured by timed automata with a single clock which is reset along every transition. Here we increase the expressiveness of interval automata by considering networks of such automata. We have an alphabet of actions which is distributed over locations. Each location runs an interval automaton over its local alphabet. Communication takes place between these automata by enforcing that locations synchronize on common actions. In terms of timed automata, product interval automata will correspond to multi-clock automata, but where the reading and resetting of clocks is controlled by the topology of the network. It is through the distribution of actions that we gain the added expressive power. As we demonstrate in Chapter 5, product interval automata are indeed capable of modelling some non-trivial timed systems.

In Sections 3.5 and 3.6 we will show that product interval automata are closed under boolean operations, and admit a logical characterisation as well.

3.1 Preliminaries

Let P = {1, 2, …, k} be a finite set of agents, or locations. 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 Σ̃. In general, for a P-distributed alphabet Δ̃ we will follow the convention that Δ = ⋃_{i∈P} Δ_{i}. The set of agents that participate in each occurrence of the action a will be denoted by loc(a) and is given by: loc(a) = {i ∈ P | a ∈ Σ_{i}}.

Through the rest of this chapter we fix such a set of agents P and a P-distributed alphabet Σ̃.

We will be considering timed languages in a distributed setting. Towards this end we must re-define the notion of a timed word over a distributed alphabet. This is mainly to allow us to model the simultaneous occurrence of independent actions. Actions a and b are said to be independent if loc(a)∩ loc(b) = ∅.

Definition 3.1 A timed word σ over Σ̃ is an element of (Σ × ℝ^{>0})^{∞} such that:

(i) if τ(a, t)(b, t′) is a prefix of σ then t ≤ t′ (non-decreasing).

(ii) if τ(a, t)τ′(b, t′) is a prefix of σ with t = t′, then loc(a) ∩ loc(b) = ∅ (simultaneous actions must be independent).

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

We let T Σ̃^{∗} and T Σ̃^{ω} denote the set of finite and infinite timed words over Σ̃ respectively, and set T Σ̃^{∞} = T Σ̃^{∗} ∪ T Σ̃^{ω}.

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 does indeed belong to T Σ_{i}^{∞}.

For a finite timed word τ, we will use time_{i}(τ) to denote the time of occurrence of the last i-action in τ. More formally:

Definition 3.2 Let τ ∈ T Σ̃^{∗}. Then time_{i}(τ) is given inductively by:

• time_{i}(ϵ) = 0.

• time_{i}(τ(a, t)) = t if a ∈ Σ_{i}, and equals time_{i}(τ) otherwise.

3.2 Product interval automata

Definition 3.3 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}) where

• Q_{i} is a finite set of states

• ⟶_{i} is a finite subset of Q_{i} × (Σ_{i} × Iℝ) × Q_{i}

• 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 initial states.

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

1. ρ(ϵ) ∈ Q_{in}

2. for each prefix τ(a, t) of σ we have

(a) for each i ∈ loc(a), there exists a transition ρ(τ)[i] ⟶_{i}^{(a,I)} ρ(τ(a, t))[i] with (t − time_{i}(τ)) ∈ I.

(b) for each i ∉ loc(a) we have ρ(τ)[i] = ρ(τ(a, t))[i].

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

(i) σ ↾i is finite and ρ(τ)[i] ∈ F_{i} for any prefix τ of σ such that τ ↾i = σ ↾i, or

(ii) σ ↾i is infinite and ρ(τ)[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).

Notice that the components A_{i} of A are interval automata over Σ_{i}, except that they have no start states. The global initial states determine which combination of states the component automata can start in. Thus, if A_{i} are interval automata over Σ_{i} respectively, with each A_{i} = (Q_{i}, ⟶_{i}, Q_{in}^{i}, F_{i}, G_{i}), and Q_{in} ⊆ Q_{1} × ⋯ × Q_{k}, then we will often use ({A_{i}}_{i∈P}, Q_{in}) to denote the product interval automaton ({B_{i}}_{i∈P}, Q_{in}), where B_{i} = (Q_{i}, ⟶_{i}, F_{i}, G_{i}).

Example 3.4 Consider the language L over Σ = {a, b} given in Lemma 2.10. We saw that L is not a regular interval language over Σ. However we can easily give a product interval automaton A over the distributed alphabet Σ̃ = {{a, b}, {b}} such that L(A) = L. Such an automaton is given in Figure 3.1. □

3.3 Checking emptiness

Unlike interval automata, product interval automata cannot be checked for emptiness by simply examining the symbolic language they accept. We can however use the region construction method of [AD94]. Rather than do this construction explicitly, we will show how to simulate a product interval automaton using a timed Büchi automaton. This will then give us a way of checking emptiness for our automata.

⇓ ⇓ (b, (0, ∞)) (a, (0, ∞)) (b, (0, ∞))  (b, (1, ∞)) (b, (0, ∞))

Figure 3.1: A product interval automaton over Σ̃ = {{a, b}, {b}}.

Due to the fact that our automata accept “non-decreasing” timed words, as opposed to the strictly increasing time sequences of [AD94], we will need to make use of a more generous semantics for timed automata. We enlarge the universe of timed words to include timed sequences over Σ which may be non-decreasing. Thus, we say σ ∈ Σ × ℝ^{>0} is a non-decreasing timed word if it satisfies the following conditions:

(i) if τ(a, t)(b, t′) is a prefix of σ then t ≤ t′ (non-decreasing).

(ii) if σ is infinite, then for each t ∈ ℝ^{>0} there exists a prefix τ(a, t′) of σ such that t < t′ (progressiveness).

Let T_{nd}Σ^{∞} denote the set of non-decreasing timed words over Σ.

We also extend the definition of a run of a timed automaton (Section 2.1) to such words too. Let L_{nd}(B) denote the set of non-decreasing timed words accepted by a timed automaton B.

The region automaton R(B) must be modified slightly to accept untime(L_{nd}(B)). This can be done by allowing every region to be a time successor of itself.

Now let A = ({A_{i}}_{i∈P}, Q_{in}) be a product interval automaton, with each A_{i} = (Q_{i}, ⟶_{i}, F_{i}, G_{i}). We assume here each local finitary final state is “terminal” in the sense that there are no outgoing edges from them. This does not involve any loss of generality.

As a first step we define a TBA B with the property that L_{nd}(B)∩T Σ̃^{∞} = L(A). We define B = (S, ⟶, S_{in}, C, F, G) where:

• The set of states is S = (∏_{i=1}^{k} Q_{i}) × {0, …, k}.

• The set of clocks is C = {x_{i} | i ∈ P}.

• Its transition relation is given as follows. We have (q, l) ⟶_{X}^{a, g} (q′, m) iff the following conditions hold:

1. X = {x_{i} | i ∈ loc(a)},

2. for each i ∈ loc(a) there exists transitions q[i] ⟶_{i}^{(a,I_{i})} q′[i] such that g = ⋀_{i∈loc(a)}(x_{i} ∈ I_{i}).

3. for each i ∉ loc(a), q[i] = q′[i].

4. m = (l + 1) mod (k + 1) if q′[l] ∈ F_{l} ∪ G_{l} or l = 0; otherwise m = l.

• The initial states are given by S_{in} = Q_{in} × {0}.

• The finitary final states F are given by F = (∏_{i=1}^{k} F_{i}) × {0, …, k}.

• The infinitary final states are given by G = {(q, l) ∈ S | l = 0}.

It is not difficult to argue that L_{nd}(B) ∩ T Σ̃^{∞} = L(A).

Next we get rid of words in L_{nd}(B) which are not in T Σ̃^{∞}. To do this we intersect B with a TBA B′ which accepts precisely the language T Σ̃^{∞}. B′ will have a single clock, and its set of states will be {0, 1}^{k}. The clock is used to check whether an action is a zero-time one, while the bits in the state keep track of the components which have already taken part in the last stretch of zero-time actions.

Formally, we define B′ = (S′, ⟶′, C′, S′_{in}, F′, G′) where S′ = {0, 1}^{k}, and C′ = {x}, S′_{in} = {0} where 0 = (0, …, 0). The transitions are one of two forms:

• v ⟶′_{{x}}^{a, (x∈(0,∞))} 0, or,

• v ⟶′_{{x}}^{a, (x∈[0,0])} v′ where v and v′ are such that each of the following are

satisfied:

– v[i] = 0 for each i ∈ loc(a).

– v′[i] = 1 if i ∈ loc(a); v′[i] = v[i] otherwise.

The final states are given by F′ = G′ = S′.

Let B′′ be the TBA obtained by intersecting B and B′. Then B′′ is the TBA promised above, with L_{nd}(B′′) = L(A).

Using the check for emptiness of the language accepted by TBA’s outlined in Section 2.1, we can check if L(A) is empty or not.

We now analyse the time complexity of checking the emptiness of A via this route. The number of states and edges in B′′ can be seen to be at most 2^{O(k)} times the number of global states and edges of A. Thus the number of states in B′′ is at most

2^{O(k)} · |Q|

and the number of edges is at most

2^{O(k)} · |E|

where |Q| = ∏_{i=1}^{k} |Q_{i}| and |E| = ∏_{i=1}^{k} |E_{i}|, with Q_{i}, E_{i} being the state and edge set of the i-th component of A. Further, the constants used in the clock constraints are the same as in A, and the number of clocks is k + 1.

Thus, using the time bound obtained in Section 2.1, the emptiness check for A takes time

|Σ| · O(|Q| + |E|) · 2^{O(k)} · k! · ∏_{i=1}^{k}(c_{i} + 1).

(The factor of |Σ| comes in as we need to examine the distribution of Σ while generating the global transition relation of A.) A loose upper bound for the above expression can be seen to be |Σ| · 2^{O(|A|^{2})}.

3.4 Product interval languages

In this section we give an alternate characterisation of languages accepted by product interval automata in terms of a timed version of the parallel composition operator ⊗. For convenience, we will continue to use the same symbol ⊗ to denote the timed version also. The characterisation we obtain will play an important role in the subsequent sections.

Let L_{i} ⊆ T Σ_{i}^{∞} for each i ∈ P. Then the direct product of L_{1}, …, L_{k}, written ⊗(L_{1}, …, L_{k}), is defined as:

⊗(L_{1}, …, L_{k}) = {σ ∈ T Σ̃^{∞} | σ ↾i ∈ L_{i} for each i ∈ P}.

L ⊆ T Σ̃^{∞} is a regular direct product interval language over Σ̃ if L = ⊗(L_{1}, …, L_{k}) for some regular interval languages L_{i} over Σ_{i}. Finally, we say L ⊆ T Σ̃^{∞} is a regular product interval language over Σ̃ if L is the finite union of regular direct product interval languages over Σ̃.

The aim of this section is to establish the following result:

Theorem 3.5 Let L ⊆ T Σ̃^{∞}. Then L is a regular product interval language over Σ̃ iff L is accepted by a product interval automaton over Σ̃.

We first prove a couple of results that will be helpful in proving the theorem.

Lemma 3.6 Let A = ({A_{i}}_{i∈P}, Q_{in}) be a product interval automaton over Σ̃. Let Q_{in} = {q_{1}, …, q_{m}} for some m ≥ 1. For j ∈ {1, …, m} let A^{j} denote the product interval automaton ({A_{i}}_{i∈P}, {q_{j}}). Then

L(A) = ⋃_{j∈{1,...,m}} L(A^{j}).

Proof Follows easily from the definition of the language accepted by a product interval automaton. □

Lemma 3.7 For each i ∈ P let A_{i} = (Q_{i}, ⟶_{i}, Q_{in}^{i}, F_{i}, G_{i}) be an interval automaton over Σ_{i}. Let A be the product interval automaton

({A_{i}}_{i∈P}, Q_{in}^{1} × ⋯ × Q_{in}^{k}).

Then

L(A) = ⊗(L(A_{1}), …, L(A_{k})).

Proof We first show that L(A) ⊆ ⊗(L(A_{1}), …, L(A_{k})). Let σ ∈ L(A). Then we know that there exists an accepting run ρ of A on σ. We can use ρ to define, for each i ∈ P, a run ρ_{i} of the interval automaton A_{i} on σ ↾i. We do this by setting, for each prefix τ_{i} of σ ↾ i, ρ_{i}(τ_{i}) = ρ(τ′)[i] where τ′ is any prefix of σ such that τ′ ↾ i = τ_{i}. It is easy to check that if τ′ and τ′′ are two prefixes of σ such that τ′ ↾ i = τ′′ ↾ i then ρ(τ′)[i] = ρ(τ′′)[i], and hence ρ_{i} is a well-defined map from prf (σ ↾i) to Q_{i}. To check that ρ_{i} is indeed a run of A_{i} on σ ↾i we must verify that

1. ρ_{i}(ϵ) ∈ Q_{in}^{i}.

This is true since ρ(ϵ) ∈ Q_{in}^{1} × ⋯ × Q_{in}^{k}.

2. For each prefix τ_{i}(a, t) of σ ↾ i, ρ_{i}(τ_{i}) ⟶_{i}^{(a,I)} ρ_{i}(τ_{i}(a, t)) for some I such that t − time(τ_{i}) ∈ I.

To verify this, let τ_{i}(a, t) be a prefix of σ ↾ i. Then there must exist a prefix τ of σ such that τ(a, t) is a prefix of σ and τ ↾ i = τ_{i}. Using the fact that ρ is a run of A on σ we have that there exists an I such that ρ(τ)[i] ⟶_{i}^{(a,I)} ρ(τ(a, t))[i] and t − time_{i}(τ) ∈ I. But it is easy to see that time_{i}(τ) = time(τ_{i}). Hence we have the required property.

Further, each ρ_{i} is an accepting run of A_{i} on σ ↾ i. This is again easy to verify given that ρ is accepting. Thus σ ↾ i ∈ L(A_{i}) for each i, and hence σ ∈ ⊗(L(A_{1}), …, L(A_{k})).

Conversely, suppose σ ∈ ⊗(L(A_{1}), …, L(A_{k})). So there exist accepting runs ρ_{i} of A_{i} on σ ↾ i for each i ∈ P. Using these ρ_{i}’s we can piece together a run ρ of A on σ, given by: ρ(τ)[i] = ρ_{i}(τ ↾i). Again, it is routine to check that ρ is indeed a run of A on σ, and is accepting. □

Returning to the proof of Theorem 3.5, suppose now that L is a regular product interval language over Σ̃. Then there exist L_{i}^{j} ⊆ T Σ_{i}^{∞} for i ∈ P and j ∈ {1, …, m} (m ≥ 1) such that each L_{i}^{j} is a regular interval language over Σ_{i} and

L = ⋃_{j∈{1,...,m}} ⊗(L_{1}^{j}, …, L_{k}^{j}).

Since each L_{i}^{j} is a regular interval language over Σ_{i}, there exist interval automata A_{i}^{j} over Σ_{i} such that L(A_{i}^{j}) = L_{i}^{j}. Let each A_{i}^{j} be of the form (Q_{i}^{j}, ⟶_{i}^{j}, (Q_{in})_{i}^{j}, F_{i}^{j}, G_{i}^{j}). Now let B_{i} denote the disjoint union of the automata A_{i}^{1}, …, A_{i}^{m} (viewed as labelled graphs). Let us use (B_{i}, (Q_{in})_{i}^{j}) to denote the interval automaton with the underlying structure of B_{i} and (Q_{in})_{i}^{j} as the set of initial states. Then it is easy to see that L(B_{i}, (Q_{in})_{i}^{j}) = L(A_{i}^{j}). Thus we have

L = ⋃_{j∈{1,...,m}} ⊗(L_{1}^{j}, …, L_{k}^{j})
= ⋃_{j∈{1,...,m}} ⊗(L(B_{1}, (Q_{in})_{1}^{j}), …, L(B_{k}, (Q_{in})_{k}^{j}))
= ⋃_{j∈{1,...,m}} L({B_{i}}_{i∈P}, (Q_{in})_{1}^{j} × ⋯ × (Q_{in})_{k}^{j}) (using Lemma 3.7)
= L({B_{i}}_{i∈P}, Q_{in}))

where Q_{in} = ⋃_{j∈{1,...,m}}(Q_{in})_{1}^{j} × ⋯ × Q_{in})_{k}^{j}. This last step follows from Lemma 3.6. Thus L is accepted by a product interval automaton.

The converse direction follows in a similar manner. Let A = ({A_{i}}_{i∈P}, Q_{in}) be a product interval automaton over Σ̃, with each A_{i} = (Q_{i}, ⟶_{i}, F_{i}, G_{i}). Let L = L(A). We will show that L is a regular product interval language over Σ̃. Let Q_{in} = {q_{1}, …, q_{m}} (m ≥ 1). Then, by Lemma 3.6, we know

L(A) = ⋃_{j=1}^{m} L({A_{i}}_{i∈P}, {q_{j}}).

Let B_{i}^{j} be the interval automaton over Σ_{i} given by

B_{i}^{j} = (Q_{i}, ⟶_{i}, {q_{j}[i]}, F_{i}, G_{i}),

for i ∈ P, j ∈ {1, …, m}. Then, by Lemma 3.7, we have

L = ⋃_{j=1}^{m} ⊗(L(B_{1}^{j}), …, L(B_{k}^{j})).

Since for each i and j, L(B_{i}^{j}) is a regular interval language over Σ_{i}, we conclude that L is a regular product interval language over Σ̃.

3.5 Closure under boolean operations

The fact that regular product interval languages are closed under union follows directly from the definition of regular product interval languages as finite unions of regular direct product interval languages.

To show closure under intersection and complementation, it is sufficient to show that these operations on regular direct product interval languages do not take us out of the class of regular product interval languages.

Let L = ⊗(L_{1}, …, L_{k}) and M = ⊗(M_{1}, …, M_{k}) with each L_{i} and M_{i} regular interval languages over Σ_{i}, respectively. Then it is easy to verify that L ∩ M = ⊗((L_{1} ∩ M_{1}), …, (L_{k} ∩ M_{k})). This is once again a regular direct product interval language since regular interval languages are closed under intersection.

To show that \overline{L} = T Σ̃^{∞} − L is a regular product interval language, note that we can write \overline{L} as

\overline{L} = ⋃_{j∈P} ⊗(W_{1}^{j}, …, W_{k}^{j})

where for each i, j ∈ P,

W_{i}^{j} = \{ \begin{matrix}T Σ_{i}^{∞} − L_{i} & if i = j \\ T Σ_{i}^{∞} & otherwise. \end{matrix}

Since each W_{i}^{j} is a regular interval language, we can conclude that \overline{L} is a regular product interval language.

Thus, we have

Theorem 3.8 The class of regular product interval languages over Σ̃ is closed under the boolean operations of union, intersection, and complementation. □

3.6 A logical characterisation

We present here the logic TMSO^{⊗}(Σ̃) which captures the class of regular product interval languages over Σ̃.

The formulas in this logic will comprise boolean combinations of TMSO assertions (cf. Section 2.5) about individual components. The formulas in the logic will be interpreted over timed words over Σ̃. An assertion about the actions of component i will be interpreted as a TMSO(Σ_{i}) sentence over the projection of the word to Σ_{i}.

The formulas of TMSO^{⊗}(Σ̃) are given by the following syntax:

φ ::= (α)(i) | ¬φ | (φ ∨ φ) | (φ ∧ φ)

where for each formula (α)(i) we require α to be a sentence in TMSO(Σ_{i}). The notation (α)(i) is meant to indicate that the sentence α comes from the logic TMSO(Σ_{i}). We introduce the operator ∧ as a first class operator in the logic as a matter of convenience.

We note that the formulas in this logic are all sentences—i.e. they have no free variables.

A model for a TMSO^{⊗}(Σ̃) sentence is a timed word in T Σ̃^{∞}. For a word σ ∈ T Σ̃^{∞} and a sentence φ ∈ TMSO^{⊗}(Σ̃), the satisfaction relation σ ⊧ φ is given inductively as follows.

σ ⊧ (α)(i)  iff σ ↾i ⊧ α (as a TMSO(Σ_{i}) formula)
σ ⊧ ¬α  iff σ |̸= α
σ ⊧ (φ ∨ φ′) iff σ ⊧ φ or σ ⊧ φ′
σ ⊧ (φ ∧ φ′) iff σ ⊧ φ and σ ⊧ φ′

For a sentence φ ∈ TMSO^{⊗}(Σ̃) we set L(φ) = {σ ∈ T Σ̃^{∞} | σ ⊧ φ}.

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

To prove this theorem we will make use of the fact that regular interval languages are characterised by the logic TMSO.

We first observe a straightforward consequence of the semantics of TMSO^{⊗}(Σ̃).

Proposition 3.10 For each i in P, let φ_{i} be a sentence in TMSO(Σ_{i}). Consider the TMSO^{⊗}(Σ̃) formula ((φ_{1})(1) ∧ ⋯ ∧ (φ_{k})(k)). Then

L((φ_{1})(1) ∧ ⋯ ∧ (φ_{k})(k)) = ⊗(L(φ_{1}), …, L(φ_{k})).

Proof Let σ ∈ T Σ̃^{∞} and let σ ⊧ ((φ_{1})(1) ∧ ⋯ ∧ (φ_{k})(k)). Then, we know that σ ⊧ (φ_{i})(i) for each i ∈ P. Hence, for each i ∈ P, σ ↾ i ⊧ φ_{i} and consequently, σ ↾i ∈ L(φ_{i}). Thus, σ ∈ ⊗(L(φ_{1}), …, L(φ_{k})).

Conversely, let σ ∈ ⊗(L(φ_{1}), …, L(φ_{k})). Then σ ↾ i ∈ L(φ_{i}) for each i ∈ P. That is, σ ↾ i ⊧ φ_{i} for each i ∈ P. This means that σ ⊧ ((φ_{1})(1) ∧ ⋯ ∧ (φ_{k})(k)). □

Now given a regular direct product interval language L = ⊗(L_{1}, …, L_{k}) we know from Theorem 2.15 that there exist sentences φ_{i} ∈ TMSO(Σ_{i}) such that L(φ_{i}) = L_{i}. Using Proposition 3.10, we have L((φ_{1})(1)∧⋯∧(φ_{k})(k)) = L. Thus regular direct product interval languages can be captured in our logic. Regular product interval languages are finite unions of regular direct product interval languages, and hence can be captured using the ∨ operator in our logic.

Conversely, given a sentence φ in TMSO^{⊗}(Σ̃), we can write φ in disjunctive normal form by first driving in negation symbols (note that ¬((α)(i)) ≡ (¬α)(i)) and then distributing ∧ over ∨:

φ ≡ ⋁_{j=1}^{m}(⋀_{i=1}^{l_{j}} γ_{i}^{j}).

Here each γ_{i}^{j} is of the form (α_{i}^{j})(p), with α_{i}^{j} ∈ TMSO(Σ_{p}) for some p ∈ P. Further, for j = 1, …, m and i = 1, …, k, let X_{i}^{j} be the set of TMSO(Σ_{i}) sentences which occur in α_{1}^{j}, …, α_{l_{j}}^{j}. Let β_{i}^{j} be the conjunction of formulas in X_{i}^{j}, with the convention that ⋀ ∅ = ⊤. It is easy to verify that

φ ≡ ⋁_{j=1}^{m}(⋀_{i=1}^{k} β_{i}^{j}).

From the semantics of ∨ it follows that

L(φ) = ⋃_{j=1}^{m}(L(⋀_{i=1}^{k} β_{i}^{j})).

Once again, using Proposition 3.10 we have:

L(φ) = ⋃_{j=1}^{m}(⊗(L(β_{1}^{j}), ⋯, L(β_{k}^{j}))).

Since for each i ∈ P, β_{i}^{j} is a TMSO(Σ_{i}) sentence, we know that L(β_{i}^{j}) is a regular interval language over Σ_{i}. Thus, it follows that L(φ) is a regular product interval language. This completes the proof of Theorem 3.9.

Timed product-LTL

The Propositional Linear Time Temporal Logic (LTL) proposed by Pnueli [P77] is a specification logic which is well-suited for reasoning about safety and liveness properties of a wide class of reactive systems. Some of the advantages of LTL as a specification language are that it is a fairly natural logic to use, and it has an elementary decision procedure, in contrast to the logic MSO which has a non-elementary decision procedure. Further, LTL is known to be expressively complete: it is expressively equivalent to the first-order fragment of MSO [K68, GP+80].

In this chapter we attempt to lift these advantages to the timed setting. We formulate a timed version of LTL called timed product-LTL and denoted TLTL^{⊗}. An important motivation for studying this logic is that it is expressively complete, being expressively equivalent to the first-order fragment of the logic TMSO^{⊗} introduced in Chapter 3.

TLTL^{⊗} formulas will comprise boolean combinations of assertions over individual components in a timed logic called TLTL. The structure and semantics of TLTL^{⊗} are based on the logic product-LTL proposed by Thiagarajan in the untimed setting [Thi95]. In [Thi95], the author’s main motivation was to examine a subset of LTL in which one can make trace-consistent assertions about concurrent systems. Such assertions have the property that their truth is invariant across interleaved runs of a partially ordered computation, and hence constitute a class of properties which are amenable to partial-order based verification methods [V92]. The motivation in our case however, as mentioned earlier, is that TLTL^{⊗} is a natural temporal logic to study in the framework of product interval automata. In fact, in our setting, product timed LTL turns out to be more expressive than timed LTL over a single global alphabet.

In the next section we introduce the logic TLTL and study its satisfiability problem. We will make use of this in Section 4.2 where we study the satisfiability and model checking problems for the logic TLTL^{⊗}.

Finally, in Section 4.3 we prove the expressive completeness of TLTL^{⊗}.

4.1 TLTL over a single component

We begin with our version of timed action-based LTL, denoted TLTL. Let Σ be an alphabet of actions. Then the formulas of TLTL(Σ) (parameterised by the alphabet Σ) are given by:

φ ::= ⊤ | ¬φ | (φ ∨ φ) | ⟨a, I⟩φ | Oφ | (φUφ).

Here we require a ∈ Σ and I ∈ Iℝ.

The semantics of TLTL(Σ) is given as follows, with the models being timed words over Σ. In what follows, σ ∈ T Σ^{∞}, and τ ∈ T Σ^{∗} with τ ∈ prf (σ).

σ, τ ⊧ ⊤

σ, τ ⊧ ¬α  iff σ, τ |̸= α
σ, τ ⊧ α ∨ β iff σ, τ ⊧ α or σ, τ ⊧ β
σ, τ ⊧ ⟨a, I⟩α iff ∃t : τ(a, t) ⪯ σ and t − time(τ) ∈ I, and σ, τ(a, t) ⊧ α
σ, τ ⊧ Oα  iff ∃τ(a, t) ⪯ σ with σ, τ(a, t) ⊧ α
σ, τ ⊧ αUβ iff ∃δ ∈ prf (σ) with τ ⪯ δ, such that σ, δ ⊧ β and
∀γ : τ ⪯ γ ≺ δ, σ, γ ⊧ α.

We say σ ⊧ φ iff σ, ϵ ⊧ φ. Define L(φ) = {σ ∈ T Σ^{∞} | σ ⊧ φ}.

We mention here some of the standard abbreviations used in temporal logic. The formula ◇α (read as “future α” or “eventually α”) is defined as ◇α = ⊤Uα. □α (“globally α”) is defined as □α = ¬◇¬α.

We now give a construction of an interval automaton which accepts the set of models of a given TLTL(Σ) formula. The construction follows the classical construction of [VWS83]. The manner in which the results are phrased is motivated by their application in the construction of a similar automaton for TLTL^{⊗}.

Before we proceed, we would like to note here that a simpler route to follow would be to translate a given formula of TLTL(Σ) into an equivalent formula which mentions only intervals taken from a proper interval set. We can then use the classical construction to associate an appropriate interval automaton with the given formula. However, this method could lead to an exponential blow-up in the size of the translated formula. This blow-up is avoided in the method we adopt below.

Theorem 4.1 Let X be a non-empty set of formulas of TLTL(Σ). Then we can construct a structure A_{X} = (Q, ⟶, F, G) (an interval automaton without start states) such that for each non-empty subset Y of X there exists (Q_{in})_{Y}^{X} ⊆ Q such that

1. L(⋀ Y) = L(A_{X}, (Q_{in})_{Y}^{X}) where by (A_{X}, (Q_{in})_{Y}^{X}) we mean the interval automaton (Q, ⟶, (Q_{in})_{Y}^{X}, F, G). Thus, by suitably choosing start states for A_{X} we can accept exactly the models of the conjunction of a subset of formulas in X.

2. The number of states in A_{X} is at most 2^{O(∑_{φ∈X} |φ|)}.

3. The largest bound mentioned in A_{X} is at most the largest bound mentioned in the formulas in X.

Proof Let I be the set of intervals mentioned in the formulas in X. Let I′ be a proper interval set covering I. Using a method similar to the one outlined in section 2.4 we can construct I′ such that the size of I′ is at most 2 · |I|, and the largest integer constant mentioned in I′ is the largest integer constant mentioned in I.

For a TLTL formula φ we will denote the subformula closure of φ by sfc(φ). Formally, sfc(φ) is defined inductively as follows:

• sfc(⊤) = {⊤}

• sfc(¬α) = {¬α} ∪ sfc(α).

• sfc((α ∨ β)) = {(α ∨ β)} ∪ sfc(α) ∪ sfc(β).

• sfc(⟨a, I⟩α) = {⟨a, I⟩α} ∪ sfc(α).

• sfc(Oα) = {Oα} ∪ sfc(α).

• sfc((αUβ)) = {(αUβ)} ∪ sfc(α) ∪ sfc(β).

For a set of formulas X we write sfc(X) to denote the set ⋃_{α∈X} sfc(α). We define CL(X), the Fisher-Ladner closure of a set of formulas X, to be

CL(X) = S ∪ {¬α | α ∈ S} ∪ {O(αUβ) | αUβ ∈ S},

where S = sfc(X).

It is easy to verify that |CL(X)| ≤ 3 · ∑_{α∈X} |α|.

An atom of X is a maximal “propositionally” consistent subset of CL(X). Formally, a subset A of CL(X) is an atom of X iff 1. If ⊤ ∈ CL(X) then ⊤ ∈ A.

2. ∀α ∈ CL(X), ¬α ∈ A iff α ∉ A. (Here we identify ¬¬α with α.)

3. ∀(α ∨ β) ∈ CL(X), (α ∨ β) ∈ A iff α ∈ A or β ∈ A.

4. ∀(αUβ) ∈ CL(X), (αUβ) ∈ A iff β ∈ A, or, both α, O(αUβ) ∈ A.

We can now define the automaton A_{X}. Take Q to be the set of atoms of X. The transition relation ⟶ is given by the following rule. We have A ⟶^{(a,I′)} B iff each of the following is satisfied:

1. I′ ∈ I′

2. if ⟨b, I⟩α ∈ A then

(i) b = a

(ii) I ∩ I′ ≠ ∅

(iii) α ∈ B.

3. if ⟨a, I⟩α ∈ CL(X) with I ∩ I′ ≠ ∅ and α ∈ B, then ⟨a, I⟩α ∈ A.

4. For all Oα ∈ CL(X), Oα ∈ A iff α ∈ B.

The set of finitary final states F consists of atoms which have no “nextstate” formulas—i.e. formulas of the form ⟨a, I⟩α or Oα.

For the infinitary final states we have a generalized Büchi condition G = {G_{1}, …, G_{m}} where m ≥ 0 is the number of until formulas in CL(X). Let {α_{1}Uβ_{1} , …, α_{m}Uβ_{m} } be the set of until formulas in CL(X). Then for each i ∈ {1, …, m} we define G_{i} = {A | α_{i}Uβ_{i} ∉ A or β_{i} ∈ A}.

Now let Y be a non-empty subset of X, φ = ⋀ Y, and (Q_{in})_{Y}^{X} = {A | Y ⊆ A}. We will show that L(φ) = L((A_{X}, (Q_{in})_{Y}^{X})).

We first show that L(φ) ⊆ L((A_{X}, (Q_{in})_{Y}^{X})). Let σ be a model for φ. Let ρ : prf (σ) → Q be given by ρ(τ) = {α ∈ CL(X) | σ, τ ⊧ α}. It is easy to verify that for each τ ∈ prf (σ), ρ(τ) is an atom. Further, for

each τ(a, t) ∈ prf (σ) we have ρ(τ) ⟶^{(a,I′)} ρ(τ(a, t)) where I′ ∈ I′ such that t−time(τ) ∈ I′. This too can be readily verified, keeping in mind that we are working with a proper interval set I′. Also, we can see that ρ(ϵ) ∈ (Q_{in})_{Y}^{X}, since σ, ϵ ⊧ φ and hence σ, ϵ ⊧ α for each α ∈ Y, and hence Y ⊆ ρ(ϵ). We have verified so far that ρ is indeed a run of (A_{X}, (Q_{in})_{Y}^{X}) on σ. To argue that ρ is accepting, we first consider the case when σ is finite. Clearly ρ(σ) cannot contain any formula of the form ⟨a, I⟩α or Oα. For the case when σ is infinite, we need to show that ρ meets each of the acceptance conditions G_{i}.

Suppose to the contrary that there exists an i for which G_{i} is not satisfied. Thus there exists a prefix τ of σ such that for all δ ∈ prf (σ) such that τ ⪯ δ we have σ, δ ⊧ α_{i}Uβ_{i} and σ, δ |̸= β_{i}. From the semantics of U this is clearly not possible. Thus ρ is an accepting run of (A_{X}, (Q_{in})_{Y}^{X}) on σ, and hence σ ∈ L((A_{X}, (Q_{in})_{Y}^{X})).

Conversely, to argue that L((A_{X}, (Q_{in})_{Y}^{X})) ⊆ L(φ), we first show the following:

Claim 4.2 Let σ ∈ T Σ^{∞} and let ρ be an accepting run of (A_{X}, (Q_{in})_{Y}^{X}) on σ. Let α ∈ CL(X). Then for each τ ∈ prf (σ) we have σ, τ ⊧ α iff α ∈ ρ(τ).

We can prove the claim by induction on the structure of α. For α = ⊤, we know ⊤ ∈ ρ(τ) for all τ ∈ prf (σ).

For α = ¬β, by the induction hypothesis, we know that σ, τ ⊧ ¬β iff σ, τ |̸= β iff β ∉ ρ(τ) iff ¬β ∈ ρ(τ).

For α = ⟨a, I⟩β, let σ, τ ⊧ ⟨a, I⟩β. Then τ(a, t) ∈ prf (σ) with t − time(τ) ∈ I, and σ, τ(a, t) ⊧ β. Thus, by induction hypothesis, β ∈ ρ(τ(a, t)). From clause 3 of the definition of the transition relation ⟶, we must have ⟨a, I⟩β ∈ ρ(τ). Conversely, let ⟨a, I⟩β ∈ ρ(τ). Let τ(b, t) ∈ prf (σ).

Then, since ρ is a run on σ, there exists I′ ∈ I′ such that ρ(τ) ⟶^{(b,I′)} ρ(τ(a, t)), and t − time(τ) ∈ I′. But since ⟨a, I⟩β ∈ ρ(τ), by the definition of the transition relation ⟶, it must be the case that a = b and I ∩ I′ ≠ ∅. Since I′ is proper, it must be the case that I′ ⊆ I, and hence t − time(τ) ∈ I′ implies t − time(τ) ∈ I. This tells us that σ, τ ⊧ ⟨a, I⟩β.

The arguments for the ∨, U and O connectives are similar to the classical case and are omitted here.

We have used a generalized Büchi condition above. We can go over to a standard Büchi condition as shown in Section 2.1 with an O(m) blow-up in the number of states. Since m ≤ ∑_{φ∈X} |φ|, the number of states is still 2^{O(∑_{φ∈X} |φ|)} as claimed in the statement of the theorem. □

Given φ ∈ TLTL(Σ) we know that φ is satisfiable iff the language accepted by A_{{φ}} is non-empty. Using the results from section 2.3 we see that A_{{φ}} can be checked for emptiness in 2^{O(|φ|)} time. Thus we have:

Corollary 4.3 The satisfiability of a formula φ in TLTL can be checked in 2^{O(|φ|)} time.

4.2 Product TLTL

We now give the syntax and semantics of TLTL^{⊗}. Let Σ̃ = {Σ_{i}} be a distributed alphabet. The syntax of the logic TLTL^{⊗}(Σ̃) is given by:

φ ::= (φ)(i) | ¬φ | (φ ∧ φ′) | (φ ∨ φ′)

where, as in section 3.6, we require of (φ)(i) that i ∈ P and φ ∈ TLTL(Σ_{i}). Thus (φ)(i) is an arbitrary i-type formula φ, tagged with the index i. Once again we introduce ∧ as a first class operator in the logic for convenience in working out proofs. The expressiveness of the logic is unaffected even if we drop the ∧ operator from the syntax.

Models for TLTL^{⊗}(Σ̃) formulas are timed words in T Σ̃^{∞}. Let φ ∈ TLTL^{⊗}(Σ̃) and let σ ∈ T Σ̃^{∞}. The satisfaction relation σ ⊧ φ is defined inductively as follows:

σ ⊧ (φ)(i) iff σ ↾i ⊧ φ (as a TLTL(Σ_{i}) formula).
σ ⊧ ¬φ  iff σ |̸= φ
σ ⊧ (φ ∧ φ′) iff σ ⊧ φ and σ ⊧ φ′.
σ ⊧ (φ ∨ φ′) iff σ ⊧ φ or σ ⊧ φ′.

Once again, we let L(φ) denote the set {σ ∈ T Σ̃^{∞} | σ ⊧ φ}.

Example 4.4 The following formula over the distributed alphabet Σ̃ = ({a, b}, {b}) recognises the language L of Lemma 2.10.

(⟨b, (0, ∞)⟩⟨a, (0, ∞)⟩⟨b, (0, ∞)⟩⊤)(1) ∧ (⟨b, (0, ∞)⟩⟨b, (1, ∞)⟩⊤)(2).

□

From the semantics of TLTL^{⊗}(Σ̃) the following lemma is immediate:

Lemma 4.5 Let φ_{1}, …, φ_{k} be formulas in TLTL(Σ_{1}), …, TLTL(Σ_{k}) respectively. Then,

L((φ_{1})(1) ∧ ⋯ ∧ (φ_{k})(k)) = ⊗(L(φ_{1}), …, L(φ_{k})).

Next we show how we can associate with a given TLTL^{⊗}(Σ̃) formula a product interval automaton which recognizes exactly the models of the formula. Let φ ∈ TLTL^{⊗}(Σ̃). As done for TMSO^{⊗}(Σ̃) in Theorem 3.9, we can write φ as

φ ≡ ⋁_{j=1}^{m}(⋀_{i=1}^{l_{j}} α_{i}^{j}).

with each α_{i}^{j} a TLTL(Σ_{p})-formula for some p ∈ P. Further, for j = 1, …, m and i = 1, …, k, let X_{i}^{j} be the set of i-type formulas which occur in α_{1}^{j}, …, α_{l_{j}}^{j}. Let β_{i}^{j} be the conjunction of formulas in X_{i}^{j}, with the convention that ⋀ ∅ = ⊤. It follows that

φ ≡ ⋁_{j=1}^{m}(⋀_{i=1}^{k} β_{i}^{j}).

From the semantics of ∨ it follows that

L(φ) = ⋃_{j=1}^{m}(L(⋀_{i=1}^{k} β_{i}^{j})).

From Lemma 4.5 we have:

L(φ) = ⋃_{j=1}^{m}(⊗(L(β_{1}^{j}), ⋯, L(β_{k}^{j}))).

Now using theorem 4.1 we can construct for each i = 1, …, k an interval automaton A_{X_{i}} (where X_{i} = ⋃_{j=1}^{m} X_{i}^{j}), such that for each j = 1, …, m the interval automaton (A_{X_{i}}, (Q_{in})_{X_{i}^{j}}^{X_{i}}) accepts L(β_{i}^{j}). Using Lemma 3.7 it follows that

L(φ) = ⋃_{j=1}^{m} L(({A_{X_{i}}}_{i=1}^{k}, ((Q_{in})_{X_{1}^{j}}^{X_{1}} × ⋯ × (Q_{in})_{X_{k}^{j}}^{X_{k}}))).

Now note that the product interval automata

({A_{X_{i}}}_{i=1}^{k}, ((Q_{in})_{X_{1}^{j}}^{X_{1}} × ⋯ × (Q_{in})_{X_{k}^{j}}^{X_{k}})) for j = 1, …, m

are the same except for the start states. It then follows easily that

L(φ) = L(A_{φ})

where

A_{φ} = ({A_{X_{i}}}_{i=1}^{k}, ⋃_{j=1}^{m}((Q_{in})_{X_{1}^{j}}^{X_{1}} × ⋯ × (Q_{in})_{X_{k}^{j}}^{X_{k}})).

Thus the satisfiability problem for TLTL^{⊗} can be solved as follows. Given a formula φ ∈ TLTL^{⊗}(Σ̃) we can generate the product interval automaton A_{φ} and then check the emptiness of A_{φ} as outlined in section 3.3.

To analyse the time complexity of checking satisfiability of φ, note that each component A_{X_{i}} of A_{φ} can be generated in time 2^{O(∑_{α∈X_{i}} |α|)} using Theorem 4.1. Further, it is not difficult to see that ∏_{i=1}^{k} 2^{O(∑_{α∈X_{i}} |α|)} = 2^{O(|φ|)}.

Thus, if Q_{i} and E_{i} are the set of states and edges respectively of the component A_{X_{i}}, we have:

∏_{i=1}^{k} |Q_{i}| = 2^{O(|φ|)} and ∏_{i=1}^{k} |E_{i}| = 2^{O(|φ|)}.

The global initial states can be generated in time

2^{O(|φ|)} · ∏_{i=1}^{k} |Q_{i}| = 2^{O(|φ|)}.

Finally note that ∏_{i=1}^{k} c_{i} is also at most 2^{O(|φ|)}, where c_{i} for i ∈ {1, …, k} is the largest interval bound appearing in an i-type formula. Now using these values in the time bounds obtained in section 3.3 for checking emptiness of product interval automata, we see that the satisfiability of φ can be decided in time

|Σ| · 2^{O(|φ|)} · 2^{O(k)} · k!.

As regards the space complexity of satisfiability we have the following result:

Theorem 4.6 Given Σ̃ and a formula φ ∈ TLTL^{⊗}(Σ̃), the problem of checking whether φ is satisfiable is PSPACE-complete.

Proof The satisfiability problem for LTL is known to be PSPACE-complete [SC85]. PSPACE-hardness for TLTL^{⊗} follows easily by reducing the satisfiability problem for LTL to the one-component case of TLTL^{⊗}. To show that the satisfiability check can be done in PSPACE, we argue that it can be done non-deterministic PSPACE. This will give us a PSPACE algorithm, since non-deterministic PSPACE is known to be equal to PSPACE.

1. The region graph R(A_{φ}) is an implicitly defined graph whose adjacency relation can be checked in space polynomial in |φ| + |Σ̃|. Note that the description of each state-region pair is at most polynomial in the size of the input. In particular, each region can be described in O(k^{2}) · |φ| space, and time successors of a region can be generated in space linear in the description of the region (see [AD94]).

2. Reachability on an n-node graph can be done in non-deterministic log(n) space. The number of states in R(A_{φ}) can be seen to be

2^{O(|φ|)} · 2^{O(k)} · k!.

Thus, the logarithm of the number of states in R(A) is polynomial in |φ| and |Σ̃|, and hence we can check reachability in R(A_{φ}) nondeterministically in polynomial space in the size of φ and Σ̃.

3. We can check emptiness of R(A_{φ}) using the algorithm for reachability. We guess a start state and a final state to begin with. We then check that the final state is reachable from the start state, and that the final state is reachable from itself.

□

Next suppose we consider a real-time program Pr modeled by a product interval 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 φ.

Theorem 4.7 The model checking problem for TLTL^{⊗}(Σ̃) is PSPACE-comp-lete.

Proof PSPACE-hardness follows from the fact that the satisfiability problem for TLTL^{⊗} can be reduced to the model checking problem. This is because the question of whether φ is satisfiable can be reduced to whether A_{univ} |̸= ¬φ, where A_{univ} is a product interval automaton which recognizes the language T Σ̃^{∞}.

To see that the problem can be solved in PSPACE, we must check the emptiness of the intersection of A_{Pr} and A_{φ} in space polynomial in |A_{Pr}|+|φ|. This is a similar argument to the one we have sketched for Theorem 4.6 above. □

4.3 Expressive completeness of TLTL^{⊗}

In this chapter we show that TLTL^{⊗}(Σ̃) is expressively equivalent to the first-order fragment of TMSO^{⊗}(Σ̃). Once again, the proof of this result will factor through a well known result in the classical setting relating LTL and MSO [K68, GP+80].

Let FO[TMSO(A)] denote the first-order fragment of the logic TMSO(A). FO[TMSO(A)] is obtained from TMSO(A) by disallowing the use of quantification over set variables. Thus the syntax of the logic is given by

φ ::= (x ∈ X) | (x < y) | Q_{a}(x) | Δ(x, I) | ¬φ | (φ ∨ φ) | ∃xφ.

The semantics is the same as that of TMSO(A).

The first-order fragment of TMSO^{⊗}(Σ̃), denoted FO[TMSO^{⊗}(Σ̃)] is obtained by taking boolean combinations of the first-order fragment of TMSO(Σ_{i}) for each i ∈ P. Thus the syntax of FO[TMSO^{⊗}(Σ̃)] is given by

φ ::= (α)(i) | ¬φ | (φ ∨ φ) | (φ ∧ φ)

where in each formula (α)(i), α is a sentence in FO[TMSO(Σ_{i})].

It will be useful to first recall the definition of LTL and the result concerning its expressive completeness.

Let A be an alphabet of actions. Then the formulas of the so-called “action-based” LTL, denoted LTL(A), are given by the syntax:

φ ::= ⊤ | ¬φ | (φ ∨ φ) | ⟨a⟩φ | Oφ | (φUφ).

In the formula ⟨a⟩φ we require a ∈ A.

The semantics of LTL(A) is given as follows, with the models being finite and infinite words over A. In what follows, σ ∈ A^{∞}, and τ ∈ A^{∗} with τ ∈ prf (σ).

σ, τ ⊧ ⊤

σ, τ ⊧ ¬α iff σ, τ |̸= α
σ, τ ⊧ α ∨ β iff σ, τ ⊧ α or σ, τ ⊧ β
σ, τ ⊧ ⟨a⟩α iff τa ⪯ σ and σ, τa ⊧ α
σ, τ ⊧ Oα iff ∃a ∈ A : τa ⪯ σ and σ, τa ⊧ α
σ, τ ⊧ αUβ iff ∃δ ∈ prf (σ) with τ ⪯ δ, such that σ, δ ⊧ β and
∀γ : τ ⪯ γ ≺ δ, σ, γ ⊧ α.

We will say that σ ⊧ φ iff σ, ϵ ⊧ φ. Following the convention in this thesis, we set L_{sym}(φ) = {σ ∈ A^{∞} | σ ⊧ φ}.

Thus, looking back at the syntax of TLTL(Σ) formulas, we see that they are simply LTL(Γ) formulas for some interval alphabet Γ based on Σ. Of course, we must bear in mind that TLTL(Σ) formulas are interpreted over timed words over Σ.

Let FO[MSO(A)] denote the first-order fragment of the logic MSO(A). As before, FO[MSO(A)] is obtained from the logic MSO(A) defined in Section 2.5, by disallowing existential quantification over set variables. Then a well known result due to the work of Kamp, and Gabbay et. al, is:

Theorem 4.8 ([K68, GP+80]) LTL(A) is expressively equivalent to FO[MSO(A)].

Returning to our aim of proving expressive completeness for TLTL^{⊗}(Σ̃), we first show that TLTL(A), for an arbitrary alphabet A, corresponds to the first-order fragment of TMSO(A).

The following lemma will play a pivotal role in this.

Lemma 4.9 1. Let Γ be a proper interval alphabet based on A. Let φ̂ be a formula in LTL(Γ). Thus φ̂ is also a formula in TLTL(A); let us call it φ. Then

L(φ) = tw(L_{sym}(φ̂)).

2. Given a formula φ in TLTL(A), there exists a proper interval alphabet Γ based on A and a formula φ′ in TLTL(A) such that L(φ) = L(φ′) and φ′ is also a formula in LTL(Γ).

Proof

1. The proof of this is very similar to our earlier arguments which make use of the properties of proper interval sets.

Let σ ∈ T A^{∞} and let σ̂ ∈ Γ^{∞} such that σ ∈ tw(σ̂). Further, let τ, τ̂ be prefixes of σ and σ̂ respectively, such that |τ| = |τ̂|. Then we claim that σ, τ ⊧ φ iff σ̂, τ̂ ⊧ φ̂.

To prove the claim, we proceed by induction on the structure of φ. For the base case of φ = ⊤, it is true that σ, τ ⊧ ⊤ iff σ̂, τ̂ ⊧ ⊤.

Now suppose φ = ⟨a, I⟩α. Let σ, τ ⊧ ⟨a, I⟩α. Then there exists t ∈ ℝ^{>0} such that τ(a, t) ⪯ σ, and t − time(τ) ∈ I, and σ, τ(a, t) ⊧ α. Since σ ∈ tw(σ̂) we know that there exists I′ ∈ Γ_{a} such that τ̂(a, I′) ⪯ σ̂ and t − time(τ) ∈ I′. Since Γ is a proper interval alphabet, and both I, I′ ∈ Γ_{a}, we must have I = I′. Further, by the induction hypothesis, we know that σ̂, τ̂(a, I) ⊧ α. This proves that σ̂, τ̂ ⊧ ⟨a, I⟩α. Conversely, suppose σ̂, τ̂ ⊧ ⟨a, I⟩α. Then by the semantics of LTL(Γ) we must have τ̂(a, I) ⪯ σ̂ and σ̂, τ̂(a, I) ⊧ α. Since σ ∈ tw(σ̂) we know that there exists t ∈ ℝ^{>0} such that τ(a, t) ⪯ σ and t−time(τ) ∈ I. Also, by the induction hypothesis, we know that σ, τ(a, t) ⊧ α. Thus, we have that σ, τ ⊧ ⟨a, I⟩α.

The remaining cases are easily taken care of and we omit the details here.

Now using the above claim, we can prove part 1 of the theorem. Let σ ∈ L(φ). So σ, ϵ ⊧ φ. Since Γ is a proper interval alphabet, by Lemma 2.11, there exists a σ̂ ∈ Γ^{∞} such that σ ∈ tw(σ̂). By the claim, we now have that σ̂, ϵ ⊧ φ̂. Hence σ̂ ∈ L_{sym}(φ̂) and σ ∈ tw(L_{sym}(φ̂)).

Conversely, suppose σ ∈ tw(σ̂) and σ̂ ∈ L_{sym}(φ̂). Thus σ̂, ϵ ⊧ φ̂. Using the claim again, we can conclude that σ, ϵ ⊧ φ. Thus σ ∈ L(φ). This completes the proof of part 1 of the theorem.

2. Let φ ∈ TLTL(A) and let Γ be a proper interval alphabet based on A, such that for each a ∈ A, Γ_{a} covers voc_{a}(φ). Then, to obtain φ′ we simply replace formulas of the form ⟨a, I⟩α in φ by the formula

⋁_{b=a, I′⊆I, (b,I′)∈Γ}⟨b, I′⟩α′

where, inductively, α′ is obtained from α in a similar manner. It is easy to verify that L(φ) = L(φ′).

□

Theorem 4.10 TLTL(A) is expressively equivalent to the the first-order fragment of TMSO(A).

Proof Let φ_{0} ∈ TLTL(A). Then from Lemma 4.9 part 2, we know that there exists a TLTL(A) formula φ_{1} and a proper interval alphabet Γ such that L(φ_{0}) = L(φ_{1}) and φ_{1} is also a LTL(Γ) formula. Let us refer to φ_{1} as φ̂_{1} when we consider it as a LTL(Γ) formula. Then, by part 1 of the same lemma, we have L(φ_{1}) = tw(L_{sym}(φ̂_{1})). Now, by Theorem 4.8, we know that there exists a sentence φ̂_{2} in FO[MSO(Γ)] such that L(φ̂_{2}) = L_{sym}(φ̂_{1}). Now consider the sentence φ_{3} = s-t(φ̂_{2}) (cf. Section 2.5). Since φ̂_{2} uses only first order quantification, the translated formula φ_{3} is a FO[TMSO(A)] sentence. Further, Γ is a proper interval alphabet, and hence by Lemma 2.17 we know that L(φ_{3}) = tw(L(φ̂_{2})). Thus φ_{3} is the required TMSO(A) sentence with L(φ_{0}) = L(φ_{3}).

Conversely, let φ_{0} be a sentence in FO[TMSO(A)]. Then there exists a proper interval alphabet Γ based on A such that Γ_{a} covers voc(φ_{0}) for each a ∈ A. Consider the MSO(Γ) sentence φ̂_{0} = t-s(φ_{0}) with respect to the interval alphabet Γ (cf. Section 2.5). By Lemma 2.16 L(φ_{0}) = tw(L(φ̂_{0})). Further, by the nature of the translation, φ̂_{0} is a sentence in FO[MSO(Γ)]. Now, again appealing to Theorem 4.8, we know that there exists an LTL(Γ) formula φ̂_{1} such that L_{sym}(φ̂_{1}) = L(φ̂_{0}). But by Lemma 4.9 part 1, we know that φ̂_{1} is also an LTL(A) formula (call it φ_{1}) such that L(φ_{1}) = tw(L_{sym}(φ̂_{1})). Thus φ_{1} is the required formula in TLTL(A) such that L(φ_{1}) = L(φ_{0}). □

Using the above theorem, we can now prove:

Theorem 4.11 TLTL^{⊗}(Σ̃) is expressively equivalent to FO[TMSO^{⊗}(Σ̃)].

Proof Let φ ∈ TLTL^{⊗}(Σ̃). We define a sentence l-m(φ) in TMSO^{⊗}(Σ̃) such that L(φ) = L(l-m(φ)). The sentence l-m(φ) is obtained by replacing each subformula of the form (α)(i) in φ by the sentence (α′)(i) where α′ is a sentence in TMSO(Σ_{i}) which is equivalent to the TLTL(Σ_{i}) formula α. Note that the existence of such an α′ is guaranteed by Theorem 4.10. The fact that L(φ) = L(l-m(φ)) now follows easily by inductive argument on the structure of φ.

Conversely, for a sentence φ ∈ TMSO^{⊗}(Σ̃), we define a formula m-l(φ) in TLTL^{⊗}(Σ̃) such that L(φ) = L(m-l(φ)). The formula m-l(φ) is obtained by replacing each subformula of the form (α)(i) in φ by the formula (α′)(i) where α′ is a formula in TLTL(Σ_{i}) which is equivalent to the TMSO(Σ_{i}) formula α. Once again the existence such an α′ is guaranteed by Theorem 4.10. The fact that L(φ) = L(m-l(φ)) now follows easily by inductive argument on the structure of φ. □

Modelling asynchronous circuits

The aim of this chapter is to show that product interval automata are expressive enough to model an important class of timed behaviours, namely that of asynchronous digital circuits. In [MP95] Maler and Pnueli model the timing behaviour of circuits using a network of timed automata that communicate via shared variables. Their model is based on the non-deterministic inertial delay model for gates [BS94]. With this model as our starting point, we describe the behaviour of a circuit using timed words (in contrast to the signals used in [MP95]). We then show that for a given circuit, we can define a product interval automaton which recognizes the language of timed words generated by the circuit.

We conclude the chapter with some examples of properties we can verify using this model. The properties will be expressed in the logic TLTL^{⊗}.

5.1 The non-deterministic delay model

A k-wire circuit (see Fig. 5.1) is modelled as a tuple

χ = (X, F, D, b_{0})

where X = {x_{1}, …, x_{k}} is a set of wires, F = {f_{1}, …, f_{k}} is a set of gates modeled as functions from {0, 1}^{k} to {0, 1}, and D = {(l_{1}, u_{1}), …, (l_{k}, u_{k})} is set of pairs of positive integers (u_{i} could be ∞ as a special case) with l_{i} ≤ u_{i} for each i. The pair (l_{i}, u_{i}) is meant to model the delay and the latency of the gate f_{i}. For simplicity the delay and the latency are assumed to be modeled by the same pair of values. Roughly speaking, a change in the input signal must hold for at least l_{i} units of time for it to be reflected

f_{1}  f_{2}  f_{3} [l_{1}, u_{1}]  [l_{2}, u_{2}]  [l_{3}, u_{3}]

Figure 5.1: A 3-wire circuit

in the output signal of the gate, and if a change holds for u_{i} units of time, it must be reflected in the output of the gate. This models the latency of the gate. Further, the amount of delay in reflecting a change in the input signal must again lie in the interval [l_{i}, u_{i}]. These notions will be formalised below. b_{0} here is an element of {0, 1}^{k} and will represent the initial values on the wires of the circuit.

Some simplifying assumptions have been made in this model. All gates are assumed to be of fan-in k and all wires are fed into a gate as input. Further, inputs to the circuit need to be modelled using the initial state b_{0} of the circuit, or as not-gates within the circuit, with suitable delay values.

In [MP95] Maler and Pnueli used infinite “signals” to describe the behaviour of a circuit. A signal is a piece-wise constant, right-continuous map from ℝ^{≥0} to the alphabet set, with countably many boundary points (or discontinuities). In our framework, we will use finite and infinite timed words over the alphabet Σ = {0, 1}^{k}. A signal with finitely many discontinuities can be represented as a finite timed word (these are the so called “stable” signals). If they have infinitely many discontinuities, they can be represented as infinite timed words.

We now proceed to give the behaviour of a circuit in terms of timed words. We fix a k-wire circuit χ as above. Recall that we use the alphabet Σ = {0, 1}^{k}.

We will need the following notions:

• Let τ ∈ T Σ^{∗}. We define action(τ) (w.r.t. χ) to be a if τ = τ′(a, t) for some τ′ and t, and we set action(ϵ) = b_{0}. This is the analogue of the time function used earlier in the thesis.

• Let s ∈ {0, 1}^{k}. The “hidden” value vector of s will be denoted by h(s) and is given by h(s)(i) = f_{i}(s). For each i, h(s)(i) will represent the value computed by gate i, which may or may not be propagated to the output of the gate.

• Let s ∈ {0, 1}^{k}. Then excited(s) is a subset of {1, …, k} given by i ∈ excited(s) iff s(i) ≠ h(s)(i). We will say that s is i-excited if i ∈ excited(s), and we will say that s is excited if excited(s) ≠ ∅, Finally, we will say τ ∈ T Σ^{∗} is excited (i-excited) if action(τ) is excited (i-excited).

• Let s, s′ ∈ {0, 1}^{k}. Then we define

switches(s, s′) = {i ∈ {1, …, k} | s′(i) ≠ s(i)}.

These are the gates which have switched in going from s to s′.

• For s, s′ ∈ {0, 1}^{k} we define qtoe(s, s′) ⊆ {1, …, k} given by i ∈ qtoe(s, s′) iff s′ is i-excited and s is not i-excited. qtoe is a mnemonic for “quiescent to excited.”

Similarly, i ∈ etoq(s, s′) iff s is i-excited and s′ is not i-excited.

• Let τ ∈ T Σ^{∗} and i be such that τ is i-excited. Let τ′ be the smallest prefix of τ such that

1. τ′ is i-excited, and,

2. For each τ′′ such that τ′ ⪯ τ′′ ⪯ τ we have that τ′′ is i-excited and further that action(τ′′)(i) = action(τ)(i).

Then we define etime_{i}(τ) = time(τ′). Thus etime_{i}(τ) is defined when gate-i is excited in τ, and it is the time at which gate-i last became excited, without having switched in between.

We define when a finite timed word τ ∈ T Σ^{∗} is valid (w.r.t. χ), inductively on the length of τ. The empty word ϵ is valid. A word of the form τ(a, t) is valid iff the following conditions hold. Let action(τ) = b. Then

1. τ must be valid.

2. For each i ∈ {1, …, k}, if i ∈ switches(b, a) then we must have i ∈ excited(b). Thus, for a gate to switch, it must be in an excited state.

3. For each i ∈ switches(b, a) we must have (t − etime_{i}(τ)) ∈ [l_{i}, u_{i}].

4. Suppose i ∈ excited(b) and i ∉ switches(b, a). Then

(a) if i ∉ excited(a) (i.e. gate i becomes quiescent) then we must have (t − etime_{i}(τ)) < u_{i}.

(b) if i ∈ excited(a) (i.e. gate i remains excited) then also we must have (t − etime_{i}(τ)) < u_{i}.

We say an infinite timed word in T Σ^{ω} is valid iff every finite prefix of it is valid.

We now define L(χ), the behaviour of the circuit χ. For a finite word τ in T Σ^{∗} we have τ ∈ L(χ) iff τ is valid w.r.t χ and τ is not excited. For an infinite word σ ∈ T Σ^{ω}, we have σ ∈ L(χ) iff it is valid w.r.t. to χ.

5.2 Modelling a circuit as a PIA

We now show how we can model the circuit χ as a product interval automaton A_{χ} over the distributed alphabet Σ̃′ with Σ′ ⊆ Σ × Σ. This automaton will have the property that L(A_{χ}) = L(χ), modulo a (geometric) projection applied to the alphabet. Thus we will have L(χ) = ς(L(A_{χ})) where ς is a substitution which maps actions of the form (s, s′) to s′.

We define our distributed alphabet Σ̃′ as follows. The set of actions Σ′ is the set of all (s, s′) ∈ Σ × Σ which satisfy:

1. switches(s, s′) ≠ ∅

2. i ∈ switches(s, s′) implies i ∈ excited(s).

We will have k + 1 locations and the distribution of Σ′ over the locations is given by:

loc((s, s′)) = {k + 1} ∪ switches(s, s′) ∪ etoq(s, s′) ∪ qtoe(s, s′).

(Note that we have no independent actions here as k + 1 ∈ loc(a) for all a ∈ Σ′. Hence T Σ̃′^{∞} = T Σ^{′∞}.)

The components A_{i}, for i = 1, …, k, will correspond to the ith gate. The (k + 1)-th component, A_{k+1}, will be free of any timing constraints and will keep track of the current vector of output values of the circuit.

We define A_{χ} = ({A_{i}}_{i=1}^{k+1}, Q_{in}) with each A_{i} = (Q_{i}, ⟶_{i}, F_{i}, G_{i}) given as follows:

• For i ∈ {1, …, k} we have:

– Q_{i} = {e, q}

– ⟶_{i} is given by:

∗ e ⟶_{i}^{((s,s′),[l_{i},u_{i}])} e provided i ∈ switches(s, s′) and i ∈ excited(s′).

∗ e ⟶_{i}^{((s,s′),[l_{i},u_{i}])} q provided i ∈ switches(s, s′) and i ∉ excited(s′).

∗ e ⟶_{i}^{((s,s′),(0,u_{i}))} q provided i ∉ switches(s, s′) and i ∈ etoq(s, s′).

∗ q ⟶_{i}^{((s,s′),(0,∞))} e provided i ∈ qtoe(s, s′).

– F_{i} = {q}

– G_{i} = {e, q}

• For A_{k+1} we have:

– Q_{k+1} = {0, 1}^{k}

– ⟶_{k+1} is given by:

s ⟶_{k+1}^{((t,t′),I)} s′ iff s = t, s′ = t′, and I = (0, ∞).

– F_{k+1} = {s ∈ Q_{k+1} | excited(s) = ∅}.
– G_{k+1} = Q_{k+1}.

Finally, the set of initial states Q_{in} will be a singleton {q_{in}} with q_{in} = {(d_{1}, …, d_{k}, b_{0})} where for each i ∈ {1, …, k} d_{i} = e, if b_{0} is i-excited, and q otherwise.

5.3 Proof of correctness

In this section we prove the claim that ς(L(A_{χ})) = L(χ). It will be more convenient for us to follow a slightly different route and re-define the behaviour of χ in terms of timed words over Σ′. We do this by mapping each Σ-timed word σ to a Σ′-timed word ς′(σ) in a natural way. We will then show that ς′(L(χ)) = L(A_{χ}).

Let σ ∈ T Σ^{∞}. Then we define ς(σ) by defining for each prefix τ of σ a corresponding prefix τ̂ of ς(σ). For τ = ϵ we define τ̂ = ϵ. For a nonempty prefix τ = τ′(a, t) we define τ̂ = τ̂′((b, a), t) where b = action(τ).

We extend the notions introduced earlier (like validity) in the natural way for these Σ′-timed words as well. In what follows, we will use L(χ) to mean ς′(L(χ)),

Theorem 5.1 L(χ) = L(A_{χ})

Proof We first show that L(χ) is contained in L(A_{χ}).

First note that if σ is a valid Σ′ timed word, and τ is a prefix of σ such that τ is i-excited, then time_{i}(τ) = etime_{i}(τ). This is easy to see by induction on the length of τ.

Now let σ ∈ L(χ). Consider the map ρ : prf (σ) → Q, where Q = Π_{i=1}^{k+1}Q_{i}, given by:

• ρ(ϵ) = q_{in}

• and for each prefix τ(a, t) of σ, with a = (s, s′), ρ(τ(a, t)) is given by ρ(τ(a, t))(k + 1) = s′, and for i ∈ {1, …, k}, ρ(τ(a, t))(i) = e if i ∈ excited(s′) and q otherwise.

We claim that ρ is a run of A_{χ} on σ. Let τ((s, s′), t) be a prefix of σ, and let i ∈ loc((s, s′)). Then we can show that there exists an interval I such that

• ρ(τ)(i) ⟶_{i}^{((s,s′),I)} ρ(τ((s, s′), t))(i)

• t − time_{i}(τ) ∈ I.

For example, if i ∈ switches(s, s′) and i ∉ excited(s′) then ρ(τ)(i) = e and

ρ(τ((s, s′), t))(i) = q and we know that e ⟶_{i}^{((s,s′),[l_{i},u_{i}])} q. Further, using the preceding observation, we know that t − time_{i}(τ) = t − etime_{i}(τ) which in turn lies in the interval [l_{i}, u_{i}] by the validity of σ. The other cases can be argued similarly.

Further, it is easy to verify that for i ∉ loc((s, s′)) we have ρ(τ)(i) = ρ(τ((s, s′), t))(i). Thus ρ is a run on σ.

We now argue that ρ is accepting. If σ is finite, then by definition of L(χ), σ is not i-excited for any i, and hence ρ(σ)(i) = q for all i ∈ {1, …, k}, and ρ is accepting. If σ is infinite, then assume that ρ is not accepting. Then, by the nature of the acceptance conditions, there must exist an i ∈ {1, …, k} such that A_{i} participates only finitely often in σ, say up to τ, and ρ(τ)(i) = e. By the definition of ρ this means that τ′′ is i-excited for all prefixes τ′′ of σ such that τ ⪯ τ′′. But σ is progressive, and hence there exists a prefix τ′ of σ such that time(τ′)−time(τ) > u_{i}, which in turn implies time(τ′)−etime_{i}(τ′) > u_{i}. This contradicts the validity of σ. Thus ρ must be an accepting run.

Conversely, to argue that L(A_{χ}) ⊆ L(χ), we first argue that if ρ is a run of A_{χ} on a word σ, then σ is weakly valid. We say that a word σ ∈ T Σ^{∗} is weakly valid if it satisfies all the clauses of the definition of validity, except possibly clause 4b. As before, an infinite word will be termed weakly valid iff every finite prefix of it is weakly valid.

Let σ ∈ T Σ^{′∞} and let ρ be a run of A_{χ} on σ. We show that for each τ prefix of σ

• if τ is i-excited, then etime_{i}(τ) = time_{i}(τ).

• For i ∈ {1, …, k} ρ(τ)(i) = e iff τ is i-excited.

We prove the claim by induction on |τ|. The claim clearly holds for τ = ϵ. Now let τ = τ′(a, t) be a prefix of σ with a = (s, s′). The following cases arise:

• τ′ is i-excited, i ∈ switches(s, s′), and i ∈ excited(s′). By the induction hypothesis we know that ρ(τ)(i) = e. Further, i ∈ loc((s, s′)) and the

only applicable i transition is e ⟶_{i}^{((s,s′),[l_{i},u_{i}])} e. Thus ρ(τ(a, t))(i) = e. Further, etime_{i}(τ(a, t)) = t = time_{i}(τ(a, t)).

• τ′ is i-excited, i ∈ switches(s, s′), and i ∉ excited(s′). Once again, by the induction hypothesis we know that ρ(τ′)(i) = e. Further, i ∈

loc((s, s′)) and the only applicable i transition is e ⟶_{i}^{((s,s′),[l_{i},u_{i}])} q. Thus ρ(τ′(a, t))(i) = q. Since τ is not i-excited, we are done.

• τ′ is i-excited and i ∉ switches(s, s′). By the induction hypothesis we know that ρ(τ′)(i) = e and since i ∉ loc(a) we have ρ(τ)(i) = e. Further, by the induction hypothesis, etime_{i}(τ′) = time_{i}(τ′), and since etime_{i}(τ′(a, t)) = etime_{i}(τ′), we have etime_{i}(τ′(a, t)) = time_{i}(τ′(a, t)).

• τ′ is not i-excited. then i ∈ qtoe(s, s′) and i ∈ loc(a). Further, by the induction hypothesis, ρ(τ′)(i) = q. The only applicable i-transition is

q ⟶_{i}^{((s,s′),(0,∞))} e. Thus ρ(τ′(a, t))(i) = e. Further, etime_{i}(τ′(a, t)) = t =

time_{i}(τ′(a, t)).

Using the claim proved above, it is easy to verify that such a σ is weakly valid.

We now argue that if A_{χ} has an accepting run ρ on σ, then σ must be valid. Suppose to the contrary that σ is not valid. Thus, using the first part above, σ is weakly-valid, but not valid. It follows that there must exist an i ∈ {1, …, k} and a prefix τ of σ, such that τ is i-excited and i ∉ loc(a) for all prefixes τ′(a, t) of σ such that τ ⪯ τ′. Thus σ ↾i is finite, and equals τ ↾i. Since ρ(τ)(i) = e, ρ(τ)(i) ∉ F_{i}, and ρ cannot be accepting. Thus σ must be valid.

Finally, if σ is finite then, since ρ is accepting, ρ(σ)(i) = q. Using the claim above, we have that σ is not i-excited for any i.

This completes the proof that σ ∈ L(χ). □

5.4 Properties expressed in TLTL^{⊗}

We list below some properties of circuits that we can specify in our logic TLTL^{⊗}Σ′. We can then check whether a given circuit satisfies these properties using the method for model-checking TLTL^{⊗} formulas given in Chapter 4.

• The formula φ below specifies that every possible behaviour of a circuit is eventually stable.

φ = ( ⋁_{excited(s′)=∅} ◇⟨(s, s′), (0, ∞)⟩⊤) (k + 1).

• This formula asserts that every behaviour of a circuit is unstable:

(□ ⋁_{a∈Σ′}⟨a, (0, ∞)⟩⊤) (k + 1).

• For a circuit in which the initial value b_{0} is such that b_{0}(i) = 0 the

formula

(¬◇( ⋁_{i∈switches(s,s′)}⟨(s, s′), (0, ∞)⟩⊤)) (i)

specifies that gate i is stuck at 0. If b_{0}(i) = 1 the same property is specified by the formula

(◇ ⋁_{s′(i)=0}⟨(s, s′), (0, ∞)⟩(¬◇ ⋁_{i∈switches(s,s′)}⟨(s, s′), (0, ∞)⟩⊤)) (i).

• We can specify that gate i always switches within d time units of becoming excited. This is specified by the formula

(□(φ_{1} ⇒ φ_{2}))(i)

if i ∉ excited(b_{0}), and by the formula

(□(φ_{1} ⇒ φ_{2}))(i) ∧ (φ_{3})(i)

if i ∈ excited(b_{0}), where

φ_{1} = ⋁_{i∈excited(s′)}⟨(s, s′), (0, ∞)⟩⊤
φ_{2} = ⋁_{a∈Σ′}⟨a, (0, ∞)⟩(⋁_{i∈switches(t,t′)}⟨(t, t′), (0, d]⟩⊤) (i)
φ_{3} = ⋁_{i∈switches(s,s′)}⟨(s, s′), (0, d]⟩⊤.

Distributed interval automata

Our goal here is to enlarge the class of product interval languages introduced in Chapter 3. The synchronisation of actions in product interval automata is “locally” specified. It is possible to specify the synchronisations in a global manner as done in the asynchronous automata of Zielonka [Z87]. Here we will prefer to use the term distributed automata instead of asynchronous automata.

It is well known in classical trace theory that synchronized products of automata are strictly less expressive than distributed automata. Expectedly, we gain in expressive power by considering the distributed version of product interval automata. We call these automata distributed interval automata.

As in the case of product interval automata, distributed interval automata also admit a logical characterisation and enjoy the desired closure properties.

The proof of these results will make use of several well-known results in classical trace theory. We begin by introducing these results along with the necessary background material.

6.1 Preliminaries

In this chapter and the next we will confine ourselves to infinite behaviours. This is purely for the sake of convenience, as we can then avoid dealing with multiple acceptance conditions in our automata.

For the rest of this section, we fix a P-distributed alphabet Δ̃, with P = {1, …, k}.

Recall that a Mazurkiewicz trace alphabet is a pair (A, I) where A is a finite alphabet and I is an irreflexive and symmetric relation on A. I is called an independence relation on A. A distributed alphabet Δ̃ induces in a natural manner a Mazurkiewicz trace alphabet (Δ, IΔ̃) where IΔ̃ ⊆ Δ × Δ is the independence relation induced by Δ̃, given by

a IΔ̃ b iff loc(a) ∩ loc(b) = ∅.

We will use DΔ̃ to denote the dependence relation (Δ × Δ) − IΔ̃.

Δ̃ induces an equivalence relation ≈Δ̃ on Δ^{ω} given by σ ≈Δ̃ σ′ iff for each i ∈ P, σ ↾ i = σ′ ↾ i. As usual, σ ↾ i is obtained by erasing from σ all occurrences of letters a such that a ∉ Δ_{i}.

We say L ⊆ Δ^{ω} is ≈Δ̃-consistent iff for all σ, σ′ ∈ Δ^{ω}, whenever σ ≈Δ̃ σ′ then σ ∈ L iff σ′ ∈ L. L ⊆ Δ^{ω} is then an ω-regular consistent language over Δ̃ iff L is an ω-regular subset of Δ^{ω} and L is ≈Δ̃-consistent. (We say a subset L of Δ^{ω} is ω-regular iff it is accepted by a Büchi automaton over Δ.) We denote the class of ω-regular consistent languages over a distributed alphabet Δ̃ by RCL(Δ̃).

Next we introduce distributed automata. We will need some notation to begin with. Let Δ̃ be a P-distributed alphabet. For convenience, we will denote a P-family of sets {X_{i}}_{i∈P} by {X_{i}}. Let {S_{i}} be a P-family of local state sets. Suppose P is a non-empty subset of P. Then a P -state (relative to the family {S_{i}}) is a map s : P → ⋃_{i∈P} S_{i} such that s(i) ∈ S_{i} for each i ∈ P. We let S_{P} stand for the set of P -states. We will refer to P-states as global states. An a-state is just a loc(a)-state. We let S_{a} denote the set of a-states.

Definition 6.1 A distributed (Büchi) automaton over Δ̃ is structure A = ({S_{i}}, {⟶_{a}}_{a∈Δ}, S_{in}, {F_{i}}, {G_{i}}) which satisfies:

• Each S_{i} is a finite set of i-local states.

• ⟶_{a}⊆ S_{a} × S_{a} for each a.

• S_{in} ⊆ S_{P} is a set of global initial states.

• F_{i}, G_{i} are subsets of S_{i} for each i.

It will be convenient to first define a global transition relation ⟶_{A} for A. ⟶_{A} is a subset of S_{P} × Δ × S_{P} given by: s ⟶_{A}^{a} s′ iff there exists an a-transition s_{a} ⟶_{a} s′_{a} such that s(i) = s_{a}(i) and s′(i) = s′_{a}(i) for every i ∈ loc(a). Further, s(i) = s′(i) for every i ∉ loc(a).

A run of A on a word σ̂ ∈ Δ^{ω} is a map ρ : prf (σ̂) → S_{P} such that:

• ρ(ϵ) ∈ S_{in}

• for each prefix τ̂a of σ̂ we have ρ(τ̂) ⟶_{A}^{a} ρ(τ̂a).

Further, ρ is said to be accepting iff for each i ∈ P either

(i) σ̂↾i is finite and ρ(τ̂)(i) ∈ F_{i} for some prefix τ̂ of σ̂ such that τ̂↾i = σ̂↾i, or

(ii) σ̂↾i is infinite and ρ(τ̂)(i) ∈ G_{i} for infinitely many τ̂ ∈ prf (σ̂).

As usual we will say a word σ̂ is accepted by A iff there exists an accepting run of A on σ̂. We set L_{sym}(A) to be the subset Δ^{ω} accepted by A.

In the setting of finite words, Zielonka [Z87] has shown that distributed automata accept precisely the class of regular consistent languages. Gastin and Petit [GP92] later extended this result to languages of infinite words as well.

Thus the result due to Gastin and Petit [GP92] specialised to our setting is:

Theorem 6.2 ([GP92]) Let L ⊆ Δ^{ω}. Then L is an ω-regular consistent language over Δ̃ iff L is accepted by a distributed automaton over Δ̃.

In fact, Gastin and Petit use a slightly different acceptance condition for distributed automata. Their condition can however be seen to be equivalent to the one we use here. The reader is referred to [MT96] for a discussion on this.

Next, we introduce traces which are compact ways of representing ≈Δ̃ equivalence classes of words.

Definition 6.3 Let Δ̃ be a distributed alphabet. An (infinite) trace T over Δ̃ is a triple (E, ≤, λ) where

• (E, ≤) is a countably infinite, finitary partial order. By finitary we mean that for every e ∈ E the set {f ∈ E | f < e} is finite.

• λ : E → Δ is a labelling function which satisfies:

– e⋖e′ ⇒ λ(e) DΔ̃ λ(e′). (We say e⋖e′ iff e < e′ and for all f ∈ E, e ≤ f ≤ e′ implies either f = e or f = e′.)

– λ(e) DΔ̃ λ(e′) ⇒ e ≤ e′ or e′ ≤ e.

Let Tr(Δ̃) denote the set of traces over Δ̃. We wish to point out here that for convenience we will not be distinguishing between isomorphic traces. Thus we will say (E, ≤, λ) = (E′, ≤′, λ′) if (E, ≤) is isomorphic to (E′, ≤′) via a map ϕ : E → E′ and λ(e) = λ′(ϕ(e)) for all e ∈ E.

Traces over Δ̃ and ≈Δ̃ equivalence classes represent each other via the maps w-t and t-w which we now define.

The map (“words to traces”) w-t : Δ^{ω} → Tr(Δ̃) associates a trace with a word σ ∈ Δ^{ω}, as follows:

w-t(σ) = (E, ≤, λ)

where

• E = prf (σ) − {ϵ}.

• ≤ is the least partial order contained in E × E satisfying: if τa ⪯ τ′b with a DΔ̃ b, then τa ≤ τ′b.

• λ(τa) = a.

The map t-w : Tr(Δ̃) → 2^{(Δ^{ω})} is defined as:

t-w((E, ≤, λ)) = {λ(δ) | δ is a linearization of (E, ≤)}.

(We denote the canonical extension of λ to words in Δ^{ω} by λ itself.)

We extend the maps w-t and t-w to act naturally on subsets of Δ^{ω} and Tr(Δ̃) respectively. In particular, for L ⊆ Tr(Δ̃) we have

t-w(L) = ⋃_{T ∈L} t-w(T).

Let RTrL(Δ̃) denote the class of trace languages which are images, under the map w-t, of ω-regular consistent languages over Δ̃. That is,

RTrL(Δ̃) = {w-t(L) | L ∈ RCL(Δ̃)}.

Then the classes RCL(Δ̃) and RTrL(Δ̃) represent each other via the maps w-t and t-w in the following sense

Proposition 6.4 (see [Thi95]) 1. For any L in RCL(Δ̃), t-w(w-t(L)) = L, and

2. For any L in RTrL(Δ̃), w-t(t-w(L)) = L.

We now recall some results on the logical definability of ω-regular consistent languages. In [Tho89] Thomas shows that regular consistent languages (over finite words) can be characterised by a monadic second order logic in which the ‘≤’ is interpreted as the partial ordering of action occurrences along a word (and not the prefix ordering that we have used till now). Ebinger and Muscholl [EM96] later extended this result to the setting of infinite words.

The formulas of MSOTr(Δ̃), the monadic second order logic of traces over Δ̃, are given by the following syntax:

φ ::= (x ≤ y) | Q_{a}(x) | (x ∈ X) | (φ ∨ φ) |¬φ | ∃xφ | ∃Xφ.

Here a is required to be in Δ, and as usual, x and X are individual and set variables respectively.

The formulas of MSOTr(Δ̃) are interpreted over traces in Tr(Δ̃). Given a trace T = (E, ≤, λ) over Δ̃, and an interpretation 𝕀 which assigns elements of E to the first-order variables {x, y, …} and subsets of E to the second-order variables {X, Y, …}, the atomic formulas are interpreted as follows:

T ⊧_{𝕀} (x ≤ y) iff 𝕀(x) ≤ 𝕀(y) in the partial order (E, ≤)
T ⊧_{𝕀} Q_{a}(x)  iff λ(𝕀(x)) = a
T ⊧_{𝕀} (x ∈ X) iff 𝕀(x) ∈ 𝕀(X)

The logical connectives ¬, ∨, and ∃ (for both first-order and second-order variables) are interpreted in the usual manner.

For a sentence φ ∈ MSOTr(Δ̃), let L(φ) denote the set of traces which satisfy φ. That is

L(φ) = {T ∈ Tr(Δ̃) | T ⊧ φ}.

Theorem 6.5 ([EM96]) L ∈ RTrL(Δ̃) iff L = L(φ) for some sentence φ ∈ MSOTr(Δ̃).

6.2 Distributed interval automata

Once again we fix a P-distributed alphabet Σ̃ = {Σ_{p}}_{p∈P} with P = {1, 2, …, k}. Let a ∈ Σ.

An a-event of Σ̃ is a pair (a, J) with J : loc(a) → Iℝ. The set of events of Σ̃, denoted E(Σ̃), is defined to be:

E(Σ̃) = {(a, J) | a ∈ Σ, and (a, J) is an a-event}.

A distributed interval alphabet based on Σ̃ is a distributed alphabet Γ̃ = (Γ_{1}, …, Γ_{k}) such that

1. Γ is a finite subset of E(Σ̃) (following the earlier convention, we set Γ = ⋃_{i∈P} Γ_{i}).

2. loc((a, J)) = loc(a) for all (a, J) ∈ Γ. That is, the distribution of a-events in Γ̃ respects the distribution of letters in Σ̃.

Let Γ̃ be a distributed interval alphabet based on Σ̃. Once again we can associate a set of timed words with a symbolic word σ̂ ∈ Γ^{∞}.

Definition 6.6 We define tw(σ̂) to be set of all σ ∈ T Σ̃^{∞} such that

1. |σ| = |σ̂|.

2. for each τ(a, t) ⪯ σ and τ̂(b, J) ⪯ σ̂ such that |τ| = |τ̂|, we have a = b, and for each i ∈ loc(a), (t − time_{i}(τ)) ∈ J(i).

As before, for L ⊆ Γ^{∞} we set

tw(L) = ⋃_{σ̂∈L} tw(σ̂).

Definition 6.7 A distributed interval automaton over Σ̃ is just a distributed automaton over a distributed interval alphabet Γ̃ based on Σ̃.

A distributed interval automaton A accepts a timed language L(A) ⊆ T Σ̃^{ω} given by L(A) = tw(L_{sym}(A)). We will term such languages ω-regular distributed interval languages over Σ̃, and denote this class DIL(Σ̃).

As in the case of interval automata and product interval automata, we can define the notion of a run of A directly on a timed word in T Σ̃^{ω}. The timed language accepted in this manner can be seen to coincide with the one given above using the tw map.

We remark here that in the the light of Theorem 6.2 an alternate way of arriving at the class DIL(Σ̃) is by applying the map tw to languages in RCL(Γ̃), for some distributed interval alphabet Γ̃ based on Σ̃.

Example 6.8 Fig 6.1 shows a distributed interval automaton A over the distributed alphabet Σ̃ = ({a, a′, d}, {b, b′, d}). The distributed interval alphabet we have in mind is

Γ̃ = ({(a, ⟨I⟩), (a′, ⟨I⟩), (d, ⟨I, I⟩)}, {(b, ⟨I⟩), (b′, ⟨I⟩), (d, ⟨I, I⟩)}),

where I is the interval [1, 1]. We have written the second components of the a-events as ordered tuples instead of functions. Thus (d, ⟨I, I⟩) represents the d-event (d, J) where J(1) = J(2) = I.

A is defined as

A = ({S_{i}}, {⟶â}_{â∈Γ}, S_{in}, {F_{i}}, {G_{i}})

s t u t  s v  t  s v′ u′ u v  u′ v′ (d, ⟨I, I⟩)  (d, ⟨I, I⟩) (a, ⟨I⟩)  (b, ⟨I⟩) (a′, ⟨I⟩)  (b′, ⟨I⟩) (b, ⟨I⟩)  (a, ⟨I⟩)  (b′, ⟨I⟩)  (a′, ⟨I⟩)

Figure 6.1: A distributed interval automaton over Σ̃ = ({a, a′, d}, {b, b′, d}).

where S_{1} = {s, u, u′} and S_{2} = {t, v, v′}, S_{in} = {(s, t)}, F_{i} = ∅ and G_{i} = S_{i} for i ∈ P = {1, 2}. The transition relation can be inferred from the figure. For example, ⟶_{(a,⟨I⟩)}= {(s, u)} and ⟶_{(d,⟨I,I⟩)}= {((u, v), (s, t)), ((u′, v′), (s, t))}.

It is not difficult to see that

L_{sym}(A) = (([(a, I)(b, I)] + [(a′, I)(b′, I)])(d, I))^{ω}.

Here we use [x] to denote the ≈Γ̃-equivalence class of x, and the symbol ‘+’ to denote the union operation of regular expressions. L^{ω} denotes the infinite concatenation L · L · · ·.

L(A)—the language of timed words accepted by A—can be seen to be the set of all words in T Σ̃^{ω} of the form

(x_{1}, 1)(y_{1}, 1)(d, 2)(x_{2}, 3)(y_{2}, 3)(d, 4)(x_{3}, 5)(y_{3}, 5)(d, 6) ⋯

where for each i ∈ ℕ − {0}, x_{i} ∈ {a, a′}, y_{i} ∈ {b, b′}, and x_{i} = a iff y_{i} = b. □

We now wish to argue that ω-regular product interval languages are strictly weaker than ω-regular distributed interval languages.

Proposition 6.9 The class of ω-regular product interval languages over Σ̃ is strictly contained in the class of ω-regular distributed interval languages over Σ̃.

Proof Let L ⊆ T Σ̃^{ω} be an ω-regular product interval language. So there exits a product interval automaton A over Σ̃ with L(A) = L. Let A = ({A_{i}}_{i∈P}, Q_{in}), with each A_{i} = (Q_{i}, ⟶_{i}, F_{i}, G_{i}). We define a distributed interval automaton B over Σ̃ such that L(B) = L(A). Let Γ̃ be the distributed interval alphabet based on Σ̃ given by

Γ = {(a, J) ∈ E(Σ̃) | ∀i ∈ loc(a) ∃q ⟶_{i}^{(a,I)} q′ with I = J(i)}.

We define B to be the distributed automaton over Γ̃ given by:

B = ({Q_{i}}, {⟶â}_{â∈Γ}, Q_{in}, {F_{i}}, {G_{i}})

where the transition relation is defined as follows. Let (a, J) ∈ Γ, and let s,

s′ be (a, J)-states. Then s ⟶_{(a,J)} s′ iff for each i ∈ loc(a), s(i) ⟶_{i}^{(a,J(i))} s′(i). It is not difficult to verify that L(B) = L(A).

To show the strict inclusion, we argue below that the language L of Example 6.8 is not a regular product interval language over Σ̃ = ({a, a′, d}, {b, b′, d}).

Suppose L were a regular product interval language. Then there exist regular direct product interval languages L_{1}, …, L_{m} (m ≥ 1) over Σ̃, such that L = ⋃_{i=1}^{m} L_{i}. It is easy to see that there must exist some L_{i}, and timed words σ, σ′ in L_{i} such that σ ↾ 1 ≠ σ′ ↾ 1. Since we can interchange adjacent x_{i}’s and y_{i}’s and still remain within L_{i}, without loss of generality we can write σ and σ′ as: σ = τ(a, t)(b, t)(d, t + 1)δ and σ′ = τ(a′, t)(b′, t)(d, t + 1)δ′, where τ ∈ T Σ̃^{∗} and δ, δ′ ∈ T Σ̃^{ω}.

Further, we can construct a δ′′ ∈ T Σ̃^{ω} such that δ′′ ↾ 1 = δ′ ↾ 1 and δ′′ ↾2 = δ ↾2.

Now consider the word σ′′ = τ(a′, t)(b, t)(d, t + 1)δ′′. σ′′ must belong to L_{i}, since σ′′ ↾ 1 = σ′ ↾ 1 and σ′′ ↾ 2 = σ ↾ 2. But this is a contradiction, since σ′′ ∉ L.

This proves that L cannot be a regular product interval language over Σ̃. □

6.3 Checking emptiness

To check the emptiness of the timed language accepted by a distributed interval automaton we follow a similar route to the one adopted for product interval automaton in Section 3.3.

Let

A = ({S_{i}}, {⟶â}_{â∈Γ}, S_{in}, {F_{i}}, {G_{i}})

be a distributed interval automaton over Γ̃ based on Σ̃. (Once again we assume that each local finitary final state is terminal.) We define a TBA B with the property that L_{nd}(B)∩T Σ̃^{∞} = L(A). Let B = (Q, ⟶, Q_{in}, C, F, G) where:

• The set of states is Q = (∏_{i=1}^{k} S_{i}) × {0, …, k}.

• The set of clocks is C = {x_{i} | i ∈ P}.

• Its transition relation is given as follows. We have (q, l) ⟶_{X}^{a, g} (q′, m) iff the following conditions hold:

1. X = {x_{i} | i ∈ loc(a)},

2. there exists (a, J) ∈ Γ and (a, J)-states s, s′ such that s ⟶_{(a,J)} s′, q[i] = s(i) and q′[i] = s′(i) for each i ∈ loc(a), and for each i ∉ loc(a) q[i] = q′[i]. Further, g = ⋀_{i∈loc(a)}(x_{i} ∈ J(i)).

3. m = (l +1) mod (k +1) if q′(l) ∈ F_{l} ∪G_{l} or l = 0; otherwise m = l.

• The initial states are given by Q_{in} = S_{in} × {0}.

• F = ∅

• The infinitary final states are given by G = {(q, l) ∈ Q | l = 0}.

It is not difficult to argue that L_{nd}(B) ∩ T Σ̃^{∞} = L(A).

Finally, we intersect B with the automaton B′ of Section 3.3 to get the automaton B′′ with the property that L_{nd}(B′′) = L(A).

The emptiness check via this route can be seen to take time

O(|S| + |E|) · 2^{O(k)} · k! · ∏_{i=1}^{k}(c_{i} + 1)

where S and E are the sets of global states and transitions of A respectively, and c_{i} is the largest (normalised) i-type interval bound appearing in A.

Before we close this section we prove a property of distributed interval languages (this applies to product interval languages as well) which allows us a mild saving in the emptiness check for the corresponding automata.

A non-progressive timed word over Σ̃ is an element of (Σ × ℝ^{>0})^{ω} such that:

(i) if τ(a, t)(b, t′) is a prefix of σ then t ≤ t′ (non-decreasing).

(ii) if τ(a, t)τ′(b, t′) is a prefix of σ with t = t′, then loc(a) ∩ loc(b) = ∅ (simultaneous actions must be independent).

Thus a non-progressive timed word need not satisfy the progressiveness condition (iii) of Definition 3.1. Let T_{np}Σ̃^{ω} denote the set of non-progressive timed words over Σ̃.

We extend the definition of the tw map to non-progressive timed words as well. Let Γ̃ be a distributed interval alphabet based on Σ̃. For a word σ̂ in Γ^{ω} let tw_{np}(σ̂) denote the set of non-progressive timed words in T_{np}Σ̃^{ω} which satisfy Definition 6.6.

Proposition 6.10 Let Γ̃ be a distributed interval alphabet based on Σ̃ and let σ̂ ∈ Γ^{∞}. Then untime(tw_{np}(σ̂)) = untime(tw(σ̂)).

Proof We assume for convenience that the rational interval bounds which occur in Γ are integers. It is easy to adapt the proof to the case of non-integral bounds. The proof we give here is based on a similar argument in [AD94] to show that the progressiveness condition added to the region automaton is enough to ensure the existence of progressive timed word along any run which accepts a non-progressive timed word.

Let σ = (α, η) be a non-progressive timed word in tw_{np}(σ̂). If σ itself is progressive, we have nothing to prove. Suppose σ is not progressive. We construct a timed word σ′ which is progressive and belongs to tw(σ̂).

Now since σ is not progressive, its sequence of time stamps η is monotonically increasing and bounded, which means that it must converge to a value l ∈ ℝ^{>0}. This would further imply that there exists a natural number l_{0} such that for all n ≥ l_{0} we have η(n) − η(l_{0}) < 0.5. Also, let X ⊆ P be the set of components which participate infinitely often in σ; then we can assume without loss of generality that for each n ≥ l_{0}, loc(α(n)) ∈ X. Since the agents in X participate infinitely often in σ, there exists an infinite sequence of natural numbers l_{1}, l_{2}, … such that l_{0} < l_{1} < l_{2} < ⋯ and for each n ≥ 0 and i ∈ X there exists m with l_{n} < m < l_{n+1} and α(m) ∈ Σ_{i}.

Now define σ′ as (α, η′) where η′ is given as follows. Let n ∈ ℕ − {0}. Then

η′(n) = \{ \begin{matrix}η′(n − 1) + (η(n) − η(n − 1)) & if & n ∉ \{l_{1}, l_{2}, …\} \\ η′(n − 1) + (η(n) − η(n − 1)) + 0.5 & if & n ∈ \{l_{1}, l_{2}, …\} \end{matrix}

where we set η′(0) = 0.

σ′ is clearly progressive since its time stamps increase by at least 0.5 time units at infinitely many points along the word. Further, untime(σ′) = untime(σ) = α. Thus we need only verify that σ′ ∈ tw(σ̂).

We first observe an immediate property of our construction. Let τ, τ′ be prefixes of σ and σ′ respectively, such that |τ| = |τ′|. Let i ∈ loc(action(τ)). Then time_{i}(τ′) = time_{i}(τ) + 0.5 if |τ| ∈ {l_{1}, l_{2}, …}, and time_{i}(τ′) = time_{i}(τ) otherwise. Further, if |τ| ∈ {l_{1}, l_{2}, …, } then 0 < time_{i}(τ) < 0.5. Since our interval bounds are assumed to be integral, it follows that time_{i}(τ′) ∈ I iff time_{i}(τ) ∈ I for any interval I mentioned in Γ. Since σ ∈ tw_{np}(σ̂) it follows that σ′ ∈ tw(σ̂).

It now follows immediately that untime(tw_{np}(σ̂)) = untime(tw(σ̂)) □

As a consequence of this proposition, while checking the emptiness of the TBA B′′ above, we need not add the extra state information in the region automaton R(B′′) to ensure progressive runs.

6.4 Closure under Boolean Operations

Here we wish to show that class of distributed interval languages are closed under boolean operations. To be precise, we fix, as usual, a distributed alphabet Σ̃ = {Σ_{p}}_{p∈P} with P = {1, 2, …, k}. Closure under union is straightforward, so here we will concentrate on complementation.

Once more the notion of a proper alphabet will play an important role. We extend the notion of proper interval alphabets introduced in Chapter 2 to distributed interval alphabets too. We say a distributed interval alphabet Γ̃ over Σ̃ is proper if the set

Γ_{a,i} = {I | ∃(a, J) ∈ Γ, with J(i) = I}

is a proper interval set for each a ∈ Σ and i ∈ loc(a). As before, we will say a distributed interval alphabet Γ̃ covers another distributed interval alphabet Δ̃ (with both Γ̃ and Δ̃ based on Σ̃) iff Γ_{a,i} covers Δ_{a,i} for each a ∈ Σ and i ∈ loc(a).

Given a distributed interval alphabet Γ̃ based on Σ̃, we can construct a proper distributed interval alphabet Δ̃ based on Σ̃ such that Δ̃ covers Γ̃. This can be done by defining

Δ_{i} = {(a, J) ∈ E(Σ̃) | a ∈ Σ_{i} and ∀i ∈ loc(a), J(i) ∈ prop(Γ_{a,i})}.

The following proposition shows that proper alphabets suffice to capture the class DIL(Σ̃).

Proposition 6.11 Let Γ̃ be a distributed interval alphabet over Σ̃ and let L̂ ∈ RCL(Γ̃). Let Δ̃ be a proper distributed interval alphabet covering Γ̃. Then there exists a M̂ ∈ RCL(Δ̃) such that tw(M̂) = tw(L̂).

Proof Since L̂ is in RCL(Γ̃), by Theorem 6.2 we know that there exists a distributed automaton A over Γ̃ such that L_{sym}(A) = L̂. Let A = ({S_{i}}, {⟶_{(a,J)}}_{(a,J)∈Γ}, S_{in}, {F_{i}}, {G_{i}}). Consider now the distributed automaton

B = ({S_{i}}, {⟹_{(a,J)}}_{(a,J)∈Δ}, S_{in}, {F_{i}}, {G_{i}})

over Δ̃ given by: s_{a} ⟹_{(a,J′)} s′_{a} iff we have s_{a} ⟶_{(a,J)} s′_{a} with J′(i) ⊆ J(i) for each i ∈ loc(a).

Taking M̂ = L_{sym}(B) it is quite easy to prove that tw(M̂) = tw(L̂). □

Proper distributed interval alphabets also enjoy a property analogous to Lemma 2.11 for interval alphabets:

Proposition 6.12 Let Γ̃ be a proper distributed interval alphabet based on Σ̃ and let σ ∈ T Σ̃^{ω}. Then there exists a unique σ̂ ∈ Γ^{ω} such that σ ∈ tw(σ̂).

Proof Consider the word σ̂ ∈ Γ^{ω} defined as follows. Let i ∈ ℕ − {0}. Let τ(a, t) be the prefix of σ such that |τ| = i − 1. Then we define σ̂(i) = (a, J) where for each j ∈ loc(a), J(j) is the unique interval I in Γ_{a,j} such that (t − time_{j}(τ)) ∈ I. By construction, we have that σ ∈ tw(σ̂).

To argue that σ̂ is the only word in Γ^{ω} for which σ ∈ tw(σ̂), let σ̂′ ∈ Γ^{ω} with σ ∈ tw(σ̂′). We show that for every i ∈ ℕ, σ̂′(i) = σ̂(i). Let i ∈ ℕ and let σ̂(i) = (b, J) and σ̂′(i) = (b′, J′). Let τ(a, t) be the prefix of σ such that |τ| = i − 1. Then clearly b = b′ = a. Further, for each j ∈ loc(a) we have (t − time_{j}(τ)) ∈ J(j) and (t − time_{j}(τ)) ∈ J′(j). But both J(j) and J′(j) belong to Γ_{a,j}. Since Γ_{a,j} is a proper interval set, we must have J(j) = J′(j). This proves that σ̂′ = σ̂. □

Now let L be a distributed interval language over Σ̃. So there exists a proper distributed interval alphabet Γ̃ over Σ̃, and a distributed automaton A over Γ̃, such that L = tw(L_{sym}(A)). By the complementation results established in [KMS95, M94] we know that there exists a distributed interval automaton B over Γ̃ such that L_{sym}(B) = Γ^{ω} − L_{sym}(A).

It now follows using Proposition 6.12 that

L(B) = tw(Γ^{ω} − L_{sym}(A)) = T Σ̃^{ω} − tw(L_{sym}(A)) = T Σ̃^{ω} − L.

This lets us conclude that the class DIL(Σ̃) is closed under complementation.

It is easy to see that the class of distributed interval languages over Σ̃ is closed under union. Closure under union and complementation give us closure under intersection too. Thus, we have the following result:

Theorem 6.13 The class DIL(Σ̃) of ω-regular distributed interval languages over Σ̃ is closed under the boolean operations of union, intersection and complementation.

6.5 Timed trace languages

The aim of this section is to obtain a representation result for distributed interval languages via timed trace languages. This result will be along the lines of the representation of ω-regular consistent languages via ω-regular trace languages stated in Proposition 6.4.

We begin with the notion of a timed trace.

Definition 6.14 A timed trace over Σ̃ is a pair (T, θ) where

• T = (E, ≤, λ) is a trace over Σ̃

• θ : E → ℝ^{>0} satisfying

– e < e′ ⇒ θ(e) <′ θ(e′) where <′ is the usual ordering over reals (we will call this < itself, since the intended ordering will be clear from the context), and

– there exists a linearization δ of (E, ≤), such that δ respects θ (i.e. θ(e) < θ(e′) ⇒ e < e′ in δ) and θ(δ) is progressive—i.e. it forms a divergent sequence of reals.

Let TTr(Σ̃) denote the set of timed traces over Σ̃.

Let (T, θ) be a timed trace over a distributed alphabet Σ̃, with T = (E, ≤ , λ). For each e ∈ E and i ∈ P the set

↓_{i} e = {e′ ∈ E | e′ < e and λ(e′) ∈ Σ_{i}}

is a finite, totally ordered subset of E. When this set is non-empty we define last_{i}((T, θ), e) to be the maximum element of ↓_{i} e, and time_{i}((T, θ)), e) to be θ(last_{i}((T, θ), e)). If the set ↓_{i} e is empty, we define time_{i}((T, θ), e) = 0.

Let Γ̃ be a distributed interval alphabet based on Σ̃. Given a trace T = (E, ≤, λ) over the symbolic alphabet Γ̃ we can associate a set of timed traces tt(T) with T as follows: Let (T′, θ′) be a timed trace over Σ̃, with T′ = (E′, ≤′, λ′). Then (T′, θ′) ∈ tt(T) iff

• (E′, ≤′) = (E, ≤) and for each e ∈ E, λ′(e) = a iff λ(e) = (a, J) for some J. That is, λ′ is the projection of λ to the Σ-component of the alphabet Γ.

• Let e ∈ E with λ(e) = (a, J). Then for each i ∈ loc(a) (θ′(e) − time_{i}((T′, θ′), e)) ∈ J(i).

Next, we observe that the uniqueness property of symbolic traces over a proper distributed interval alphabet holds for traces as well.

Lemma 6.15 Let Γ̃ be a proper distributed interval alphabet based on Σ̃. Let (T′, θ′) be a timed trace over Σ̃. Then there exists a unique trace T ∈ Tr(Γ̃) such that (T′, θ′) ∈ tt(T).

Proof Let T′ = (E′, ≤′, λ′). Define T = (E, ≤, λ) with E = E′, ≤=≤′, and λ given as follows. Let e ∈ E and let λ′(e) = a. Then we define λ(e) = (a, J) where for each i ∈ loc(a), J(i) is the unique interval in Γ_{a,i} such that θ′(e) − time_{i}((T′, θ′), e) ∈ J(i). T is clearly a trace over Γ̃ and, by construction, (T′, θ′) ∈ tt(T).

The uniqueness of T (up to isomorphism) follows easily using the fact that Γ̃ is proper. □

We say a subset M of TTr(Σ̃) is an ω-regular timed trace language over Σ̃ iff there exists a distributed interval alphabet Γ̃ based on Σ̃ and an ω-regular trace language M̂ over Γ̃, with M = tt(M̂). Let RTTrL(Σ̃) denote the class of ω-regular timed trace languages over Σ̃.

We now define maps tt-tw (“timed traces to timed words”) and tw-tt (“timed words to timed traces”) which take us back and forth between distributed interval languages and timed traces languages.

Definition 6.16

1. The map tw-tt : DIL(Σ̃) → RTTrL(Σ̃) is given as follows. Let L ∈ DIL(Σ̃). Then there exists a distributed interval alphabet Γ̃ based on Σ̃ and L̂ ∈ RCL(Γ̃) such that L = tw(L̂). We set tw-tt(L) = tt(w-t(L̂)).

2. The map tt-tw : RTTrL(Σ̃) → DIL(Σ̃) is given as follows. Let M ∈ RTTrL(Σ̃). Then there exists a distributed interval alphabet Γ̃ based on Σ̃ and M̂ ∈ RTrL(Γ̃) such that M = tw(M̂). We set tt-tw(M) = tw(t-w(M̂)).

We need to show that the maps tw-tt and tt-tw are indeed well-defined.

Proposition 6.17 tw-tt and tt-tw are well-defined maps from DIL(Σ̃) to RTTrL(Σ̃) and RTTrL(Σ̃) to DIL(Σ̃) respectively.

Proof We prove that tw-tt is well-defined. The proof that tt-tw is welldefined proceeds in a similar manner.

Let Γ̃_{1} and Γ̃_{2} be distributed interval alphabets based on Σ̃, and let L̂_{1} ∈ RCL(Γ̃_{1}) and L̂_{2} ∈ RCL(Γ̃_{2}) such that tw(L̂_{1}) = tw(L̂_{2}) = L. Let M̂_{1} = w-t(L̂_{1}) and let M̂_{2} = w-t(L̂_{2}). Then we show that tt(M̂_{1}) = tt(M̂_{2}).

We first show that tt(M̂_{1}) ⊆ tt(M̂_{2}).

Let (T, θ) ∈ tt(M̂_{1}) with T = (E, ≤, λ). So there exists T̂_{1} ∈ M̂_{1} with (T, θ) ∈ tt(T̂_{1}). Now T has a linearization δ such that θ(δ) is progressive. Let σ̂_{1} be the corresponding linearization of T̂_{1}. (Since T̂_{1} and T are isomorphic, the isomorphism induces a linearization of T̂_{1} corresponding to δ.) By Proposition 6.4, it follows that σ̂_{1} ∈ L̂_{1}. We also note here that the underlying poset of T is isomorphic to the underlying poset of w-t(σ̂_{1}) and hence we can assume that E is the set of non-empty prefixes of σ̂_{1}.

Consider now the timed word σ = (α, η) where α is the projection of σ̂_{1} to the Σ component—i.e. for each i ∈ ℕ, α(i) = a iff σ̂_{1}(i) = (a, J) for some J; for each non-empty prefix w of α we have η(w) = θ(τ̂) where τ̂ is the prefix of σ̂_{1} such that |τ̂| = |w|. It is not difficult to verify that σ is progressive and hence is a timed word over Σ̃. We now claim that σ ∈ tw(σ̂_{1}). This is easy to infer once we observe that for any prefix τ of σ, and τ̂ of σ̂_{1} such that |τ| = |τ̂|, we have last_{i}(τ) exists iff last_{i}((T, θ), τ̂) exists and |last_{i}(τ)| = |last_{i}((T, θ), τ̂)|. This is easy to verify using the fact that σ̂_{1} is a linearization of T. Thus we conclude that σ ∈ tw(σ̂_{1}).

Now since tw(L̂_{1}) = tw(L̂_{2}), there exists σ̂_{2} ∈ L̂_{2} such that σ ∈ tw(σ̂_{2}). Since σ ∈ tw(σ̂_{1}) and σ ∈ tw(σ̂_{2}), the sequence of Σ-actions in σ̂_{1} and σ̂_{2} are the same. Hence, if T̂_{2} = w-t(σ̂_{2}) then T̂_{1} and T̂_{2} are isomorphic as posets, where the isomorphism matches equal length prefixes of σ̂_{1} and σ̂_{2}. Thus to show that (T, θ) ∈ tt(T̂_{2}) we need only verify the following: Let τ̂_{1} be a prefix of σ̂_{1}, and τ̂_{2} a prefix of σ̂_{2}, such that |τ̂_{1}| = |τ̂_{2}|. Further, let λ(τ̂_{1}) = a and let (a, J) be the label of τ̂_{2} in T̂_{2}. Then we have θ(τ̂_{1})−time_{i}((T, θ), τ̂_{1}) ∈ J(i) for each i ∈ loc(a). This is again easy to verify using the fact that σ ∈ tw(σ̂_{2}). This completes the proof that tt(M̂_{1}) ⊆ tt(M̂_{2}).

By a symmetric argument it follows that tt(M̂_{2}) ⊆ tt(M̂_{1}). Thus tt(M̂_{1}) = tt(M̂_{2}). This proves that tw-tt is a well-defined map. □

Theorem 6.18 The classes DIL(Σ̃) and RTTrL(Σ̃) represent each other via the maps tw-tt and tt-tw in the following sense:

1. Let L ∈ DIL(Σ̃). Then tt-tw(tw-tt(L)) = L.

2. Let M ∈ RTTrL(Σ̃). Then tw-tt(tt-tw(M)) = M.

Proof

1. Let tw-tt(L) = M. So there exists a distributed interval alphabet Γ̃ based on Σ̃, and L̂ ∈ RCL(Γ̃) such that L = tw(L̂), and M = tt(w-t(L̂)). Let M̂ = w-t(L̂). Now, since M̂ ∈ RTrL(Γ̃) and M = tt(M̂), we have tt-tw(M) = tw(t-w(M̂)). By Proposition 6.4, t-w(M̂) = L̂. Thus tt-tw(M) = tw(L̂), and hence tt-tw(M) = L.

2. Let tt-tw(M) = L. Then there exists a distributed interval alphabet Γ̃ based on Σ̃, and M̂ ∈ RTrL(Γ̃) such that M = tt(M̂), and L = tw(t-w(M̂)). Let L̂ = t-w(M̂). Now, since L̂ ∈ RCL(Γ̃) with L = tw(L̂), we have tw-tt(L) = tt(w-t(L̂)) which equals tt(M̂) by Proposition 6.4. Thus tw-tt(L) = M.

□

6.6 A logical characterisation

In this section we provide a logical characterisation for the class of ω-regular timed trace languages over Σ̃. The logic, called TMSOTr(Σ̃), will have the flavour of MSOTr but in a timed setting.

As per the convention used in the earlier logics, we assume a supply of individual variables x, y, … and a supply of set variables X, Y, … which will be interpreted as events and sets of events, respectively, in the partial order of the timed trace under consideration.

Definition 6.19 The formulas of TMSOTr(Σ̃) are given by the following syntax:

φ ::= (x ≤ y) | Q_{a}(x) | Δ_{i}(x, I) | (x ∈ X) | (φ ∨ φ) |¬φ | ∃xφ | ∃Xφ.

In the atomic formula Q_{a}(x) we require a ∈ Σ, and in Δ_{i}(x, I) we require i ∈ P and I ∈ Iℝ.

The formulas of TMSOTr(Σ̃) are interpreted over timed traces over Σ̃ as described below. Let (T, θ) be timed trace over Σ̃. Let T = (E, ≤, λ). Let 𝕀 be an interpretation of variables which maps each individual variable (respectively set variable) to an element in E (respectively, a subset of E). Then the atomic formulas are interpreted as follows:

(T, θ) ⊧_{𝕀} (x ≤ y) iff 𝕀(x) ≤ 𝕀(y) in the partial order (E, ≤)
(T, θ) ⊧_{𝕀} Q_{a}(x)  iff λ(𝕀(x)) = a
(T, θ) ⊧_{𝕀} (x ∈ X) iff 𝕀(x) ∈ 𝕀(X)
(T, θ) ⊧_{𝕀} Δ_{i}(x, I) iff λ(𝕀(x)) ∈ Σ_{i} and θ(𝕀(x)) − time_{i}((T, θ), 𝕀(x)) ∈ I.

The boolean operators ∨ and ¬, and the existential quantifiers ∃x and ∃X are interpreted in the usual way.

For a sentence φ ∈ TMSOTr(Σ̃), let L(φ) denote the set

L(φ) = {(T, θ) ∈ TTr(Σ̃) | (T, θ) ⊧ φ}.

We will show that the class of timed trace languages definable by TMSOTr(Σ̃) sentences is precisely the class of ω-regular timed trace languages over Σ̃. We will do this by translating back and forth between formulas in TMSOTr(Σ̃) and MSOTr(Γ̃), for a suitable Γ̃ based on Σ̃, and then appealing to Theorem 6.5.

Definition 6.20 Let φ ∈ TMSOTr(Σ̃). Let Γ̃ be a proper distributed interval alphabet based on Σ̃ such that for each i ∈ P and a ∈ Σ_{i}, Γ_{a,i} covers the set

voc_{i}(φ) = {I | Δ_{i}(x, I) is a subformula of φ}.

Then the formula t-s(φ) (w.r.t. Γ̃) in MSOTr(Γ̃) is obtained by replacing in φ atomic formulas of the form Q_{a}(x) by

⋁_{(b,J)∈Γ, b=a} Q_{(b,J)}(x)

and atomic formulas of the form Δ_{i}(x, I) by the formula

⋁_{(a,J)∈Γ, a∈Σ_{i}, J(i)⊆I} Q_{(a,J)}(x).

Lemma 6.21 Let φ and Γ̃ be as above. Let 𝕀 be an interpretation for variables. Then we can say the following:

1. Let T ∈ Tr(Γ̃) and let (T′, θ′) ∈ tt(T). Then

(T′, θ′) ⊧_{𝕀} φ iff T ⊧_{𝕀} t-s(φ).

2. If φ is a sentence, then L(φ) = tt(L(t-s(φ))).

Proof

1. We proceed by induction on the structure of φ. Let T = (E, ≤, λ) and T′ = (E, ≤, λ′). We consider the base cases when φ is of the form Q_{a}x and Δ_{i}(x, I). The remaining base cases and induction steps are routine.

(a) Case φ = Q_{a}(x): (T′, θ′) ⊧_{𝕀} Q_{a}(x) iff λ′(𝕀(x)) = a which holds iff λ(𝕀(x)) = (b, J) for some (b, J) ∈ Γ with b = a. This in turn holds iff T ⊧_{𝕀} ⋁_{(b,J)∈Γ, b=a} Q_{(b,J)}(x).

(b) Case φ = Δ_{i}(x, I): Let (T′, θ′) ⊧_{𝕀} Δ_{i}(x, I). Then we know λ′(𝕀(x)) ∈ Σ_{i} and θ′(𝕀(x))−time_{i}((T′, θ′), 𝕀(x)) ∈ I. Let λ(𝕀(x)) = (a, J). So a = λ′(𝕀(x)) ∈ Σ_{i}. Further, since (T′, θ′) ∈ tt(T), we have θ′(𝕀(x)) − time_{i}((T′, θ′), 𝕀(x)) ∈ J(i). It follows that I ∩ J(i) ≠ ∅. Since I ∈ voc_{i}(φ) and Γ_{a,i} covers voc_{i}(φ), we must have J(i) ⊆ I. Since we know that T ⊧_{𝕀} Q_{(a,J)}(x) with a ∈ Σ_{i} and J(i) ⊆ I, we have:

T ⊧_{𝕀} ⋁_{(a,J)∈Γ, a∈Σ_{i}, J(i)⊆I} Q_{(a,J)}(x).

Conversely, let T ⊧_{𝕀} t-s(Δ_{i}(x, I)). i.e.

T ⊧_{𝕀} ⋁_{(a,J)∈Γ a∈Σ_{i}, J(i)⊆I} Q_{(a,J)}(x).

Thus, T ⊧_{𝕀} Q_{(a,J)}(x) for some a ∈ Σ_{i} and (a, J) ∈ Γ such that J(i) ⊆ I. So, λ(𝕀(x)) = (a, J). Further, since (T′, θ′) ∈ tt(T), we have λ′(𝕀(x)) = a ∈ Σ_{i} and

θ′(𝕀(x)) − time_{i}((T′, θ′), 𝕀(x)) ∈ J(i).

Since J(i) ⊆ I, we have

θ′(𝕀(x)) − time_{i}((T′, θ′), 𝕀(x)) ∈ I.

Thus, (T′, θ′) ⊧_{𝕀} Δ_{i}(x, I).

2. Let (T′, θ′) ⊧ φ. Since Γ̃ is a proper distributed interval alphabet, by Lemma 6.15 there is a trace T in Tr(Γ̃) such that (T′, θ′) ∈ tt(T). By part 1 above, we know T ⊧ t-s(φ). Thus (T′, θ′) ∈ tt(L(t-s(φ))).

Conversely, let (T′, θ′) ∈ tt(L(t-s(φ))). So there exists T in Tr(Γ̃) such that T ⊧ t-s(φ)) and (T′, θ′) ∈ tt(T). Again, by part 1 of the lemma, (T′, θ′) ⊧ φ, and (T′, θ′) ∈ L(φ).

□

In a similar manner, we can go from a formula φ in the “symbolic” logic MSOTr(Γ̃) to a formula s-t(φ) in TMSOTr(Σ̃) by replacing subformulas of the form Q_{(a,J)}(x) in φ by the formula

Q_{a}(x) ∧ ⋀_{i∈loc(a)} Δ_{i}(x, J(i)).

Lemma 6.22 Let Γ̃ be a proper distributed interval alphabet based on Σ̃. Let φ be a formula in MSOTr(Γ̃). Let 𝕀 be an interpretation for variables.

1. Let T ∈ Tr(Γ̃) and let (T′, θ′) ∈ tt(T). Then

T ⊧_{𝕀} φ iff (T′, θ′) ⊧_{𝕀} s-t(φ).

2. If φ is a sentence then tt(L(φ)) = L(s-t(φ)).

Proof

1. The proof once again proceeds by induction on the structure of φ. We give the argument for the case when φ is the atomic formula Q_{(a,J)}(x).

Let T ⊧_{𝕀} Q_{(a,J)}(x). Then λ(𝕀(x)) = (a, J). Since (T′, θ′) ∈ tt(T), we know λ′(𝕀)(x) = a and θ′(𝕀(x)) − time_{i}((T′, θ′), 𝕀(x)) ∈ J(i) for all i ∈ loc(a). Hence

(T′, θ′) ⊧_{𝕀} Q_{a}(x) ∧ ⋀_{i∈loc(a)} Δ_{i}(x, J(i)).

Conversely, let

(T′, θ′) ⊧_{𝕀} Q_{a}(x) ∧ ⋀_{i∈loc(a)} Δ_{i}(x, J(i)).

(having fixed an element (a, J) of Γ). Let λ(𝕀(x)) = (b, J′). Since (T′, θ′) ⊧_{𝕀} Q_{a}(x) we have λ′(𝕀(x)) = a, and hence b = a. Further, since

(T′, θ′) ⊧_{𝕀} ⋀_{i∈loc(a)} Δ_{i}(x, J(i))

we have, for each i ∈ loc(a), θ′(𝕀(x)) − time_{i}((T′, θ′), 𝕀(x)) ∈ J(i). Further, using the fact that (T′, θ′) ∈ tt(T) we have for all i ∈ loc(a) θ′(𝕀(x)) − time_{i}((T′, θ′), 𝕀(x)) ∈ J′(i). Thus, for all i ∈ loc(a) we have J′(i) ∩ J(i) ≠ ∅. But Γ̃ is proper alphabet. Hence J(i) = J′(i), and we have

T ⊧_{𝕀} Q_{(a,J)}(x).

2. Let (T′, θ′) ∈ tt(L(φ)). So there exists T in Tr(Γ̃) such that T ⊧ φ and (T′, θ′) ∈ tt(T). By part 1 of the lemma, (T′, θ′) ⊧ s-t(φ), and we have (T′, θ′) ∈ L(s-t(φ)).

Conversely, let (T′, θ′) ⊧ s-t(φ). Since Γ̃ is a proper distributed interval alphabet, by Lemma 6.15 there is a trace T in Tr(Γ̃) such that (T′, θ′) ∈ tt(T). By part 1 above, we know T ⊧ φ. Thus (T′, θ′) ∈ tt(L(φ)).

□

We can now state and prove the main result of this section.

Theorem 6.23 L ⊆ TTr(Σ̃) is a ω-regular timed trace language over Σ̃ iff it is definable in TMSOTr(Σ̃). That is:

L ∈ RTTrL(Σ̃) iff L = L(φ) for some sentence φ ∈ TMSOTr(Σ̃).

Proof Let M ∈ RTTrL(Σ̃). So there exists a distributed interval alphabet Γ̃ based on Σ̃, and a language M̂ ∈ RTrL(Γ̃) such that M = tt(M̂). By the Theorem 6.5, there exists a sentence φ in MSOTr(Γ̃) such that M̂ = L(φ). By Lemma 6.22 we know that

L(s-t(φ)) = tt(M̂) = M.

Conversely, let M = L(φ) for some sentence φ in TMSOTr(Σ̃). Let Γ̃ be a proper distributed interval alphabet based on Σ̃ such that for each i ∈ P and a ∈ Σ_{i}, Γ_{a,i} covers voc_{i}(φ). Then by Lemma 6.21 we know there exists a sentence φ′ = t-s(φ) in MSOTr(Γ̃) such that

tt(L(φ′)) = L(φ) = M.

Again, appealing to Theorem 6.5, we know that L(φ′) belongs to RTrL(Γ̃). Since M = tt(L(φ′)) we have that M ∈ RTTrL(Σ̃). □

Cellular interval automata

In classical trace theory asynchronous cellular automata are known to provide an alternate automata-theoretic characterisation of regular trace languages. Cellular asynchronous automata are again a network of automata based on a distributed alphabet. They have a separate component for each action in the alphabet, in contrast to distributed automata which have a component for each location in the distributed alphabet. Each component in the cellular automaton can read the states of the components of actions dependent on it, but must make a move by changing its own local state only.

In this chapter we consider a timed version of these automata called cellular interval automata. Here we have a component for each action, and a clock for each component. A component can not only read the states of the components of actions dependent on it, but can also make use of timing constraints based on the the values of the clocks of these components. In addition, the clock of the component corresponding to each action a is reset with every occurrence of a.

In contrast to the classical untimed setting, cellular interval automata are more powerful than distributed interval automata. This is due to the fact we now have a clock for each action, rather than one for each component. In fact, as we show in Section 7.4, they have the same expressive power as the event recording automata of Alur, Fix and Henzinger [AFH94].

The class of timed languages accepted by cellular interval automata are closed under boolean operations. In addition they admit a logical characterisation along the lines of that for distributed interval languages.

Finally, making use of the techniques introduced so far, we give a full monadic second order logic characterisation of event recording languages.

7.1 Preliminaries

The underlying symbolic structure of cellular interval automata correspond to quasi asynchronous cellular automata (qACA’s). In this section we introduce these automata, and show that, like distributed automata, they too recognise exactly the class of ω-regular consistent languages. We will use this fact to establish several results about the languages accepted by cellular interval automata.

We will need to extend the notation of the last chapter regarding Pindexed families of sets to other families of sets as well.

Let {S_{x}}_{x∈X} be a family of X-indexed sets of states. Let Y ⊆ X. Then a Y -state (with respect to the family {S_{x}}_{x∈X}) is a map s : Y → ⋃_{x∈Y} S_{x} such that s(x) ∈ S_{x} for each x ∈ Y. Let S_{Y} denote the set of Y -states. For a Y -state s, and Z ⊆ Y, we use s_{Z} to denote the Z-state s′ given by s′(x) = s(x) for each x ∈ Z.

Till further notice, let us fix a P-distributed alphabet Δ̃, and a partition of Δ, C = {C_{x}}_{x∈X}. We will need some notation relating locations of P and blocks of the partition C. Let a ∈ Δ. Then there exists a unique x ∈ X such that a ∈ C_{x}; we set comp(a) = x. For i ∈ P we will use comp(i) to mean the set {comp(a) | a ∈ Δ_{i}}.

For elements of X we can define an analogous notion of “locations” and “dependent” blocks (with respect to Δ̃ and C). For x ∈ X, we define

loc(x) = ⋃_{a∈C_{x}} loc(a).

and the set of blocks dependent on x to be

D(x) = {y ∈ X | loc(x) ∩ loc(y) ≠ ∅}.

Finally, we say C is a valid partition (with respect to Δ̃) iff for each x ∈ X and for each a, b ∈ C_{x}, we have loc(a) = loc(b). Note that if C is a valid partition with respect to Δ̃, then for any a ∈ Δ and x ∈ X such that a ∈ C_{x}, we have loc(a) = loc(x).

Example 7.1 Let Δ̃ be the distributed alphabet ({a, b, e}, {c, d, e}). Then the partition C = ({a, b}, {c}, {d}, {e}) of Δ is a valid with respect to Δ̃.

We are now ready to define a quasi asynchronous cellular automaton (qACA).

Definition 7.2 Let Δ̃ be P-distributed alphabet. Let C = {C_{x}}_{x∈X} be a partition of Δ which is valid with respect to Δ̃. Then a qACA A over (Δ̃, C) is a structure

A = ({Q_{x}}_{x∈X}, {⟶_{a}}_{a∈Δ}, Q_{in}, {F_{x}}_{x∈X}, {G_{x}}_{x∈X}).

where

• For each x ∈ X, Q_{x} is a finite set of x-local states.

• ⟶_{a}⊆ Q_{D(y)} × Q_{y} where y = comp(a).

• Q_{in} ⊆ Q_{X}.

• F_{x}, G_{x} ⊆ Q_{x} are the finitary and infinitary accepting states for component x.

Let A be a qACA as above. Then we can define a global transition relation ⟶_{A} ⊆ Q_{X} × Δ × Q_{X} given by q ⟶_{A}^{a} q′ iff

• q_{D(y)} ⟶_{a} q′(y) where y = comp(a).

• for all x ≠ comp(a), q′(x) = q(x).

A run of A on a word σ ∈ Δ^{ω} is a map ρ : prf (σ) → Q_{X} such that

• ρ(ϵ) ∈ Q_{in} and

• for each prefix τa of σ we have ρ(τ) ⟶_{A}^{a} ρ(τa).

Let σ ↾x denote the projection of the word σ to the subset C_{x} of Δ. Then we say a run ρ on σ is accepting iff for each x ∈ X, either σ ↾x is finite and ρ(τ)(x) ∈ F_{x} for some prefix τ of σ such that τ ↾x = σ ↾x; or σ ↾x is infinite and ρ(τ)(x) ∈ G_{x} for infinitely many prefixes τ of σ.

We set L_{sym}(A) to be the set of words in Δ^{ω} on which A has an accepting run.

Lemma 7.3 Let Δ̃ be a P-distributed alphabet, and let C = {C_{x}}_{x∈X} be a valid partition of Δ with respect to Δ̃. Let L ⊆ Δ^{ω}. Then L ∈ RCL(Δ̃) iff L = L_{sym}(B) for some qACA B over (Δ̃, C).

Proof Let L ∈ RCL(Δ̃). Then we know there exists a distributed automaton A over Δ̃ such that L = L_{sym}(A). Let

A = ({S_{i}}_{i∈P}, {⟶_{a}}_{a∈Δ}, S_{in}, {F_{i}}_{i∈P}, {G_{i}}_{i∈P}).

We will construct a qACA B over (Δ̃, C) which will simulate the behaviour of A.

The idea is that each component x stores the states of each agent in loc(x), as last seen by it. In addition, for each i ∈ loc(x), it also stores information to keep track of the component (among those in comp(i)) with the latest information about agent i. This construction is adapted from a standard construction to show that cellular asynchronous automata can simulate asynchronous automata (see [M94]).

Rather than spell out the construction as a whole, it will be more convenient for the reader if we sketch the construction in a layered fashion. We begin with the underlying structure of B.

The states of B will be given by {Q_{x}}_{x∈X} where for each x ∈ X, Q_{x} = S_{loc(x)} × {0, …, |X| − 1}^{loc(x)}. Thus each Q_{x} state is of the form (s, v) where s is a vector of states comprising an S_{i} state for each i ∈ loc(x). For each i ∈ loc(x), v contains a value between 0 and |X|−1. This value when added to the values in other comp(i) components, will give us the component with the latest information of agent i’s state. (We assume, without loss of generality, that X = {0, 1, …, |X| − 1}.) This is formalised in the transition relation described below.

Let a ∈ Δ and let x = comp(a). Let q ∈ Q_{D(x)}, and let q′ ∈ Q_{x}. For each y ∈ D(x) let q(y) = (r_{y}, v_{y}). Further, let q′ = (r, v). Then we have q ⟶′_{a} q′ iff there exists a transition s ⟶_{a} s′ in A such that for each i ∈ loc(a)

• q(z)(i) = s(i), where z is the component in comp(i) with the most recent information about agent i. That is, z = (∑_{y∈comp(i)} v_{y}(i)) mod |X|.

• r(i) = s′(i).

• v(i) is such that ((∑_{y∈(comp(i)−{x})} v_{y}(i)) + v(i)) mod |X| = x.

The set of initial states Q_{in} of B will be given as follows. Let q ∈ Q_{X}, with q(x) = (r_{x}, v_{x}) for each x ∈ X. Then q ∈ Q_{in} iff

1. there exists a s ∈ S_{in} such that for each i ∈ P and each x ∈ comp(i), r_{x}(i) = s(i).

2. ∑_{x∈comp(i)} v_{x}(i) ∈ comp(i).

To give an appropriate acceptance condition for B we will have to carry additional information in the basic structure defined above.

To begin with, the automaton B guesses the following:

• A subset fin of X which is the set of components of B participating only finitely often in the word.

• For each x ∈ fin, a subset last(x) of loc(x) which is the set of agents in loc(x) for which the last action performed is a C_{x} action.

This guessing is implemented using the non-deterministic choice available through multiple initial states.

Now, each component x ∉ fin maintains, for each agent i ∈ loc(x), a pair (f, W) with f ∈ {0, 1} and W ⊆ comp(i). The pair (f, W) is used to indicate whether agent i has seen a G_{i} state (f = 1) and the components W in comp(i) which have “witnessed” this fact. Initially, f = 0 and W = ∅ for all agents. Suppose component x performs an action in Δ_{i}. Let (f, W) be the pair associated with agent i in the component with the latest information about agent i. Then if W = comp(i), f is set to 0 and W is set to ∅. Else, if agent i moves into a state in G_{i}, f is set to 1 and W to W ∪ {x}. Otherwise, f is set to 0 and W remains unchanged.

The pairs (f, W) in which x = 1 will be used by each component to signal its infinitary final states. As is done for generalised Büchi conditions, each component x signals an infinitary final state only after it checks that for each agent in loc(x), the associated pair (f, W) is such that f = 1.

For the local finitary final states, a component x ∈ fin non-deterministically decides that it has done its last action in the current word and moves into a state which indicates so. For each i ∈ loc(x), the corresponding state is marked “good” if either i ∉ last(x) or agent i has moved into a state in its local finitary final state set F_{i}. Otherwise the corresponding state is marked “bad.” The finitary final states for component x are now all those states in which the corresponding state for each agent in loc(x) is marked “good.”

This completes the description of the qACA B which accepts the same language as A.

Conversely, let B be a qACA over (Δ̃, C). We will show that we can simulate B using a distributed automaton A. This will show that L_{sym}(B) ∈ RCL(Δ̃).

Let B = ({Q_{x}}_{x∈X}, {⟶′_{a}}_{a∈Δ}, Q_{in}, {F_{x}}_{x∈X}, {G_{x}}_{x∈X}). The distributed automaton A will simulate B by keeping track of, for each agent i ∈ P, the state of each of the components in comp(i). In fact after every move of A, the following invariant will be maintained. Suppose x is the component of B which has made the last move. Then for each x ∈ X, each agent in loc(x) will contain the current state of component x.

Thus the states of B will be {S_{i}}_{i∈P} where for each i ∈ P, S_{i} = Q_{comp(i)}. The transition relation ⟶_{a} for A will be given as follows. Let a ∈ Δ

and let a ∈ C_{x}. Let y ∈ D(x). Then we know that there exists an i ∈ P such that C_{x}, C_{y} ⊆ Δ_{i}, and hence x, y ∈ comp(i). Let s, s′ be S_{a} states. Then we define s ⟶_{a} s′ iff there exists a transition in B of the form q ⟶′_{a} q′ such that

1. for each z ∈ D(x), and i ∈ loc(x) such that z ∈ comp(i), we have s(i)(z) = q(z).

2. for each i ∈ loc(a) s′(i)(x) = q′ and s′(i)(x′) = s(i)(x′) for each x′ ≠ x.

The set of initial states S_{in} is the set of states s ∈ S_{P} such that there exists a state q ∈ Q_{in} with s(i)(x) = q(x) for each i ∈ P and each x ∈ comp(i).

For setting up the final states, we will assume that each component x has been modified so that it uses only “terminating” finitary final states—that is, once in a finitary final state, the component never makes a further transition. The finitary final states for agent i will now comprise the states s ∈ S_{i} such that s(x) ∈ F_{x} for each x ∈ comp(i). For the infinitary final states we again use a counter which cycles through each component in comp(i) checking that either it is in a finitary final state, or moves into an infinitary final state in G_{x} at some point. The states with counter value 0 will then be the infinitary final states for each agent.

It is not difficult to verify that L_{sym}(A) = L_{sym}(B). This completes the proof of the lemma. □

7.2 Cellular interval automata

Once again, let us fix a set of agents P = {1, …, k} and a P-distributed alphabet Σ̃. For a ∈ Σ let D(a) denote the set of letters in Σ which are dependent on a. That is, D(a) = {b ∈ Σ | aDΣ̃b}. Then a cellular interval alphabet based on Σ̃ is a finite set of elements of the form (a, K) where a ∈ Σ and K : D(a) → Iℝ.

Let Γ be a cellular interval alphabet based on Σ̃. As before we can define a map tw which associates with each σ̂ ∈ Γ^{∞} a set of timed words tw(σ̂) ⊆ T Σ̃^{∞}. This is done as follows. Let σ ∈ T Σ̃^{∞} and let σ̂ ∈ Γ^{∞}. Then σ ∈ tw(σ̂) iff |σ| = |σ̂| and for each prefix τ(a, t) of σ and τ̂(b, K) of σ̂ with |τ| = |τ̂| we have a = b and for each c ∈ D(a), t − time_{c}(τ) ∈ K(c). Here time_{c}(τ) is the time of occurrence of the latest c action in τ: it is defined inductively as follows. time_{c}(ϵ) = 0 and time_{c}(τ′(a, t)) = t if a = c and time_{c}(τ′) otherwise. We extend the map tw to work on subsets of Γ^{∞} in the natural way.

Before we define a cellular interval automaton, we note that a cellular interval alphabet Γ̃ based on Σ̃ induces in a natural way a valid partition of Γ. This partition is given by CΓ̃ = {C_{a}}_{a∈Σ} with C_{a} = {(b, K) ∈ Γ | b = a}.

Definition 7.4 A cellular interval automaton over Σ̃ is a qACA over (Γ̃, CΓ̃), for some cellular interval alphabet Γ̃ based on Σ̃.

A cellular interval automaton A over Σ̃ accepts a timed language L(A) ⊆ T Σ̃^{ω} given by L(A) = tw(L_{sym}(A)). We will call such languages ω-regular cellular interval languages over Σ̃ and denote the class of such languages by CIL(Σ̃).

Example 7.5 Let Σ̃ = ({a, b}). We assume the ordering a < b and represent functions (over elements of Σ) as as tuples ⟨I, I′⟩, (s, s′) etc. Let Γ̃ be the cellular interval alphabet ({(a, ⟨I, I⟩), (b, ⟨I, I⟩), (b, ⟨I, I′⟩)}) where I = (0, ∞) and I′ = (1, ∞). Here X = Σ = {a, b} and CΓ̃ is the partition of Γ given by C_{a} = {(a, ⟨I, I⟩)} and C_{b} = {(b, ⟨I, I⟩), (b, ⟨I, I′⟩)}. Define

A = ({Q_{x}}_{x∈Σ}, {⟶â}_{â∈Γ}, Q_{in}, {F_{x}}_{x∈Σ}, {G_{x}}_{x∈Σ}) where

• Q_{a} = {s_{1}, s_{2}}, and Q_{b} = {s_{1}, s_{2}, s_{3}}

• The transition relations are given by:

(s_{1}, s_{1}) ⟶_{(b,I,I)} s_{2},
(s_{1}, s_{2}) ⟶_{(a,I,I)} s_{2},
(s_{2}, s_{2}) ⟶_{(b,I,I′)} s_{3},
(s_{2}, s_{3}) ⟶_{(b,I,I)} s_{3}.

• Q_{in} = {(s_{1}, s_{1})}.

• F_{a} = {s_{2}}, F_{b} = ∅, G_{a} = ∅, and G_{b} = {s_{3}}.

L(A) can be seen to be essentially the language L of Lemma 2.10, extended in a trivial way to give us an ω-language. Thus

L(A) = {(b, t)(a, t′)(b, t′′)(b, t_{1})(b, t_{2}) ⋯ ∈ T Σ^{ω} | t′′ − t > 1}
□

Cellular interval automata can be simulated by timed Büchi automata in much the same way as product and distributed interval automata. Here we will need to have a clock for each letter of Σ.

Let B = ({Q_{a}}_{a∈Σ}, {⟶′_{a}}_{a∈Γ}, Q_{in}, {F_{a}}_{a∈Σ}, {G_{a}}_{a∈Σ}) be a cellular interval automaton over Σ, via the cellular interval alphabet Γ̃. The time complexity for checking emptiness of L(B) by this method can be seen to be

O(|S| + |E|) · 2^{O(|Σ|)} · |Σ|! · ∏_{a∈Σ}(c_{a} + 1)

where S and E are the global states and transitions of B respectively. For each a ∈ Σ, c_{a} is the largest (normalised) interval bound in the set

{K(a) | b ∈ D(a) and (b, K) ∈ Γ}.

Cellular interval languages can be seen to be strictly more expressive than distributed interval languages.

Proposition 7.6 The class of ω-regular distributed interval languages over a distributed alphabet Σ̃ is a subclass of the class of ω-regular cellular interval languages over Σ̃.

Proof Let A be a distributed interval automaton over Σ̃. Then A is also a distributed automaton over a distributed interval alphabet Γ̃ based on Σ̃. Consider the partition C of Γ given by C = {C_{a}}_{a∈Σ}, where C_{a} = {(b, J) ∈ Γ | b = a}. Then C is valid with respect to Γ̃. By Lemma 7.3 we can construct a a qACA B over (Γ̃, C) such that L_{sym}(B) = L_{sym}(A).

We now transform B to a qACA B′ over a cellular interval alphabet Γ̃′ based on Σ̃. Let Γ̃′ be the set of all (a, K) with a ∈ Σ and K : D(a) → Iℝ such that K(b) is the intersection of a subset of intervals mentioned in Γ. We define the qACA B′ over (Γ̃′, CΓ̃′) as follows. The automaton B′ is essentially the same as B, except that the transition relation of B′ is obtained by replacing each edge q ⟶_{(a,J)} q′ of A by the edge q ⟶′_{(a,K)} q′, provided for each b ∈ D(a), K(b) = ⋂_{i∈P} J(i), where P ⊆ loc(a) is the set of agents for which q(b) has the latest information.

We are making use of the fact that time_{i}(τ) equals time_{b}(τ) provided b was the last Σ_{i} action to take part in τ. It is not difficult to see that this property ensures that the timed language accepted by B′ is the same as that of A.

To show that (over certain distributed alphabets) cellular interval automata are strictly more powerful than distributed interval automata, consider the timed language L accepted by the cellular interval automaton A of Example 7.5. A is defined over the single-component distributed alphabet Σ̃ = ({a, b}). Suppose that L were accepted by a distributed interval automaton over Σ̃. Since Σ̃ is a single-component distributed alphabet, this would imply that L is also a regular interval language over Σ. But, by essentially the same argument as Lemma 2.10, we know that L is not a regular interval language over Σ, and this is a contradiction. Thus L is not a ωregular distributed interval language over Σ̃. □

7.3 Closure and logical properties

In the light of results proved in the preceding section, particularly Lemma 7.3, cellular interval languages are simply images under the tw map of ω-regular consistent languages over a cellular interval alphabet. Using the notion of a proper cellular interval alphabet—defined in the obvious way—and using the fact that ω-regular consistent languages are closed under boolean operations, we can show that the class of cellular interval languages over a distributed alphabet Σ̃ are also closed under boolean operations.

Theorem 7.7 The class of CIL(Σ̃) of ω-regular cellular interval languages over Σ̃ is closed under the boolean operations of union, intersection and complementation. □

In Section 6.5 we showed that ω-regular distributed interval languages can be represented by ω-regular timed trace languages. In a similar manner we can show that ω-regular cellular interval languages can be represented by ω-regular cellular timed trace languages. These are defined via the map (called tt as well) which is given as follows. Let T = (T, ≤, λ) be a trace over a cellular interval alphabet Γ̃ based on Σ̃. Let (T′, θ′) be a timed trace over Σ̃, with T′ = (E′, ≤′, λ′). For an element e ∈ E′ we define time_{a}((T′, θ′), e) to be the time of the last a-labelled event below e in the timed trace (T′, θ′). Then (T′, θ′) ∈ tt(T) iff

• (E′, ≤′) = (E, ≤) and for each e ∈ E, λ′(e) = a iff λ(e) = (a, K) for some K. That is, λ′ is the projection of λ to the Σ-component of the alphabet Γ.

• Let e ∈ E with λ(e) = (a, K). Then for each b ∈ D(a) (θ′(e) − time_{b}((T′, θ′), e)) ∈ K(b).

As before, we extend tt to act on subsets of Tr(Γ̃) as well.

The class RTCTrL(˜Σ̃) of ω-regular timed cellular trace languages over Σ̃ is defined to be the set of all timed trace languages M ⊆ TTr(Σ̃) such that there exists a cellular interval alphabet Γ̃ based on Σ̃ and M̂ ∈ RTrL(Γ̃) such that M = tt(M̂).

We now give a logical characterisation of ω-regular timed cellular trace languages over Σ̃ in terms of a logic interpreted over timed traces, as done in Section 6.6.

The syntax of this logic, which we call TMSOC(Σ̃), is given by:

φ ::= (x ≤ y) | Q_{a}(x) | Δ_{a}(x, I) | (x ∈ X) | (φ ∨ φ) |¬φ | ∃xφ | ∃Xφ.

In the formula Δ_{a}(x, I) we require a ∈ Σ and I ∈ Iℝ.

The semantics of the logic are similar to that of TMSOTr(Σ̃) given in Section 6.6. The operator Δ_{a}(x, I) is new however, and it is interpreted as follows. Let 𝕀 be an interpretation for variables. Then:

(T, θ ⊧_{𝕀} Δ_{a}(x, I) iff λ(𝕀(x)) ∈ D(a) and θ(𝕀(x)) − time_{a}((T, θ), 𝕀(x)) ∈ I.

Using essentially the same arguments as for TMSOTr(Σ̃) we can show the following result.

Theorem 7.8 Let M ⊆ TTr(Σ̃). Then M ∈ RTCTrL(Σ̃) iff M = L(φ) for some sentence φ ∈ TMSOC(Σ̃). □

7.4 Event recording automata

We conclude this chapter by showing how cellular interval automata are related to the event recording automata of Alur, Fix and Henzinger. In addition we apply the methods introduced earlier in the thesis to establish a logical characterisation of languages accepted by event recording automata.

Event recording automata were proposed in [AFH94] as a determinizable (and hence complementable) subclass of timed automata. They are timed Büchi automata which have a clock x_{a} for each action a, with the restriction that along every transition labelled a, the set of clocks reset is exactly {x_{a}}.

We can define an event recording automaton in the same spirit as the automata introduced thus far. Let Σ be an alphabet of actions. Then an event-recording alphabet based on Σ is a finite subset of Σ × Iℝ^{Σ}. Thus elements of the event-recording alphabet are of the form (a, K), where K : Σ → Iℝ.

Let Γ be an event recording alphabet based on Σ, and let σ̂ ∈ Γ^{∞}. Then, we can associate a set of timed words tw(σ̂) with σ̂ as follows: Let σ ∈ T Σ^{∞}. Then σ ∈ tw(σ̂) iff |σ| = |σ̂| and for τ(a, t) ∈ prf (σ) and τ̂(b, K) ∈ prf (σ̂) such that |τ| = |τ̂| we have a = b, and t − time_{c}(τ) ∈ K(c) for all c ∈ Σ. As before, time_{c}(τ) is the time of occurrence of the latest c action in τ. For a subset L̂ of Γ^{∞}, we set tw(L̂) = ⋃_{σ̂∈L̂} tw(σ̂).

An event recording automaton A over Σ is a Büchi automaton over an event recording alphabet based on Σ. The language of timed words accepted by A is given by L(A) = tw(L_{sym}(A)). We term such languages as event recording languages over Σ.

Event recording automata and cellular interval automata have the same expressive power in the sense of Proposition 7.9 below. As in the case of timed automata, we will need to relax the definition of the timed language accepted by event recording automata to allow them to accept non-decreasing timed words. This is to facilitate a comparison with cellular interval languages in which simultaneous occurrences of independent actions are allowed. As done in Section 3.3 we set L_{nd}(A) to be the language of non-decreasing timed words accepted by an event recording automaton A. Also, for convenience, we will consider only ω-behaviours for these automata.

Proposition 7.9 1. Let A be an event recording automaton over an alphabet Σ. Then we can construct a cellular interval automaton B over the single-component distributed alphabet Σ̃ = (Σ) such that L(B) = L(A).

2. Let B be a cellular interval automaton over a distributed alphabet Σ̃. Then we can construct an event recording automaton A′′ over the alphabet Σ such that L_{nd}(A′′) = L(B).

Proof

1. We know that A is a Büchi automaton over a event recording alphabet Γ based on Σ and L(A) = tw(L_{sym}(A)). Now L_{sym}(A) is an ω-regular consistent language over Γ̃ = (Γ). Thus there exists a qACA B over (Γ̃, CΓ̃) such that L_{sym}(B) = L_{sym}(A) (by Lemma 7.3). Further, Γ̃ is also a cellular interval alphabet over Σ̃. Thus B is a cellular interval automaton over Σ̃. Finally, we observe that the definitions of the tw map for symbolic words over an event recording alphabet and a cellular interval alphabet coincide for a single-component distributed alphabet. It is now easy to see that L(B) = tw(L_{sym}(B)) = tw(L_{sym}(A)) = L(A).

2. Let B be a cellular interval automaton over Σ̃ as in the statement of the proposition. Then B is a qACA over (Γ̃, CΓ̃), for some cellular interval alphabet Γ̃ based on Σ̃. Let B = ({Q_{a}}_{a∈Σ}, {⟶â}_{â∈Γ}, Q_{in}, {F_{a}}_{a∈Σ}, {G_{a}}_{a∈Σ}). We assume here that each local finitary final state in B is terminal. We define an event recording automaton A over Σ with the property that L_{nd}(A) ∩ T Σ̃^{∞} = L(B). Let Γ′ be the event recording alphabet given by

Γ′ = {(a, K′) | ∃(a, K) ∈ Γ : ∀b ∈ Σ, K′(b) = K(b) if b ∈ D(a),

and (0, ∞) otherwise}.

Consider the event recording automaton A = (S, ⟶, S_{in}, F, G) over Γ′, where:

• The set of states is S = Q_{Σ} × {0, …, |Σ|}.

• The transition relation is given as follows. We have

(q, l) ⟶^{(a,K′)} (q′, m)

iff the following conditions hold:

(i) there exists (a, K) ∈ Γ such that q ⟶_{B}^{(a,K)} q′, and K′(b) = K(b) for each b ∈ D(a) and K′(b) = (0, ∞) if b ∉ D(a).

(ii) m = (l + 1) mod (|Σ| + 1) if q′(l) ∈ F_{l} ∪ G_{l} or l = 0; otherwise

m = l.

• The initial states are given by S_{in} = Q_{in} × {0}.

• F = ∅

• The infinitary final states are given by G = {(q, l) ∈ S | l = 0}.

It is easy to verify that L_{nd}(A) ∩ T Σ̃^{∞} = L(B).

Next we define an event recording automaton A′ over Σ which accepts the non-decreasing timed language T Σ̃^{ω}. This is done in a similar manner to the timed automaton B′ of Section 3.3, except that here we must keep track of the last action and replace the transition label (a, x, (x ∈ I)) by (a, K) where for each b ∈ Σ, K(b) = I if b is the last action to have taken place; otherwise K(b) = (0, ∞).

We can now intersect A with the automaton A′ to get the event recording automaton A′′ with the property that L_{nd}(A′′) = L(B).

□

Using the techniques used in the previous chapters we can show the result established in [AFH94] that event recording languages are closed under boolean operations. In addition we can give the following logical characterisation of these languages.

Consider the logic TMSOER(Σ) given by

φ ::= (x ∈ X) | (x < y) | Q_{a}(x) | Δ_{a}(x, I) | (φ ∨ φ) |¬φ | ∃xφ | ∃Xφ.

The logic is interpreted over timed words in T Σ^{ω} and the semantics is similar to that of TMSO(Σ) introduced in Section 2.5. The operator Δ_{a}(x, I) is interpreted as follows:

σ ⊧_{𝕀} Δ_{a}(x, I) iff time(𝕀(x)) − time_{a}(𝕀(x)) ∈ I.

Thus the predicate Δ_{a}(x, I) allows us to check if the time since the last occurrence of a lies in the interval I.

Theorem 7.10 Let Σ be an alphabet of actions and let L ⊆ T Σ^{ω}. Then L is an event recording language over Σ iff there exists a sentence φ ∈ TMSOER(Σ) such that L = L(φ).

Proof The proof proceeds in a very similar manner to the proof of Theorem 2.15, and the details are omitted here. □

Conclusion

In this chapter we summarise the main contents of this thesis. We also point to some areas which merit further study.

8.1 Summary

In this thesis we have proposed some subclasses of Alur-Dill timed automata and developed their theory. A common feature of our automata is that they comprise a network of timed agents in which the use of clocks is determined by the topology of the network.

The simplest of these classes of automata are called product interval automata. They comprise a network of components, each of which is a timed automaton with a single clock. The clock for each component is required to be reset with every action of the component. The classes of distributed interval automata and cellular interval automata are generalisations of product interval automata, based on classical extensions of products of automata. The relative expressive power of these automata is depicted in Fig 8.1.

We show that these classes of automata enjoy several properties which are desirable from both a practical as well as theoretical viewpoint.

Each of these classes is closed under the boolean operations of union, intersection and complementation. In addition they admit logical characterisations via full monadic second order logics.

In terms of the modelling power we show that these automata are powerful enough to model an important class of timed behaviours, namely those of asynchronous digital circuits.

Product interval automata and distributed interval automata have some useful preservation properties in the context of partial order reduction methods for timed systems. Their disciplined use of clocks can be exploited to

Product Interval Automata Distributed Interval Automata Cellular Interval Automata = Event Recording Automata Timed Automata

Figure 8.1: Subclasses of timed automata studied in this thesis

efficiently infer the independence of transitions in the quotiented state space [M99]. We also demonstrate a property of the languages accepted by these automata which leads to a saving in the emptiness check for these automata compared to that of general timed automata.

In the case of product interval languages we study a timed temporal logic called TLTL^{⊗}. This logic is expressively equivalent to the first order fragment of TMSO^{⊗}, the monadic second order logic corresponding to product interval languages. We give automata theoretic solutions to the satisfiability and model checking problems for this logic.

The closure properties of our automata can be attributed to the fact that all clocks are implicit—the action labels on the transitions determine the set of clocks to be reset. In conjunction with this property the use of proper interval alphabets constitutes the main technical idea. Proper alphabets help us to represent timed languages symbolically in a way in which operations on timed languages can factor through corresponding operations at the symbolic level. This allows us to make use of powerful results in classical automata theory and logic.

8.2 Future Work

An issue which needs further examination is whether product interval automata are amenable to a more efficient emptiness check. At the moment our method of checking emptiness is to treat these automata as general timed automata and then apply the region (or zone) construction. As shown in Section 6.3 product interval automata do have a minor advantage over general timed automata in that progressive run conditions can be done away with, leading to a minor saving in the size of the region automaton. However, one needs to explore the possibility that product interval automata may admit a more efficient emptiness check which takes advantage of the the structure of these automata.

Another area which we aim to examine further is the use of our automata in partial order reduction methods for timed systems.

In the untimed setting, the unfolding method of McMillan [M93] constitutes an alternate approach to the partial order based reduction methods of [V92, G96]. Here one constructs a finite prefix of the unfolding of a transition system (given by say a Petri net or product system) from which it is possible to retrieve information about reachability and deadlock in the corresponding global transition system. This often leads to a saving in the work done as retrieving this information from the the finite prefix could be more efficient than working with the global transition system.

We would like to explore the applicability of this method in a timed setting. Using the local time semantics of product interval automata it may be possible to define an appropriate notion of a timed unfolding. We expect such a method to help in the practical verification of asynchronous circuits.

Bibliography

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

[AFH94] 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).

[AFH96] R. Alur, T. Feder, T. A. Henzinger: The benefits of relaxing punctuality, Journal of the ACM, 43, 116–146 (1996).

[AH92] 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).

[AH93] R. Alur, T. A. Henzinger: Real-time logics: complexity and expressiveness, Information and Computation 104, 35–77 (1993).

[B60] J. R. Büchi: Weak second-order arithmetic and finite automata, Zeitschrift für Math. Logik und Grundlagen der Mathematik, 6, 66–92 (1960).

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

[BM83] B. Berthomieu, M. Menasche: An Enumerative Approach for Analyzing Time Petri Nets, Information Processing 83 North Holland (1983).

[BS94] J. A. Brzozowski, C-J. H. Seger: Asynchronous Circuits, Springer-Verlag (1994).

[DH99] D. D’Souza, T. Hune: An on-the-fly Construction for an Event Clock Logic, Manuscript (to appear in BRICS Technical Report Series) (2000).

[DM94] V. Diekert, A. Muscholl: Deterministic asynchronous automata for infinite traces, Acta Informatica 31, 379–397 (1994).

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

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

[DT99] D. D’Souza, P. S. Thiagarajan: Product Interval Automata: A Subclass of Timed Automata, Proc. 19th Foundations of Software Technology and Theoretical Computer Science (FSTTCS), LNCS 1732 (1999).

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

[G96] P. Godefroid: Partial-Order Methods for the Verification of Concurrent Systems, LNCS 1032 (1996).

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

[GP+80] D. Gabbay, A. Pnueli, S. Shelah, J. Stavi: The Temporal Analysis of Fairness, Seventh ACM Symposium on Principles of Programming Languages, 163–173, (1980).

[HRS98] 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).

[K68] K. Kamp: Tense Logic and the Theory of Linear Order, PhD Thesis, University of California (1968).

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

[KP92] S. Katz, D. Peled: Interleaving Set Temporal Logic, Theoretical Computer Science, Vol. 75 (3), 21–43 (1992).

[M93] K. McMillan: Symbolic model checking, Kluwer Academic Publishers (1996).

[M94] A. Muscholl: On the complementation of Büchi asynchronous cellular automata, Theoretical Computer Science, 169, 123–145 (1996).

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

[MF76] P. Merlin, D. J. Farber: Recoverability of Communication Protocols—Implications of a Theoretical Study, IEEE Trans. Commun. Vol 24, No. 9 (1976).

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

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

[P77] A. Pnueli: The Temporal Logic of programs, Proceedings of 18th IEEE Symposium on Foundations of Computer Science, 46–57 (1977).

[RS97] 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).

[SC85] A. P. Sistla, E. M. Clarke: The complexity of propositional linear temporal logic, Journal of the ACM, 32: 733–749 (1985).

[Thi95] P. S. Thiagarajan: A Trace Consistent Subset of PTL, Proc. CON-CUR ’95, LNCS 962, 438–452 (1995).

[Tho89] W. Thomas: On the logical definability of trace languages, in ASMICS Workshop on “Free Partially Commutative Monoids,” Kochel (1989).

[Tho90] 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).

[V92] A. Valmari: A Stubborn Attack on State Explosion, Formal Methods in System Design, 1: 297-322 (1992).

[VW86] M. Y. Vardi, P. Wolper: An automata-theoretic approach to automatic program verification, Proc. IEEE Symposium on Logic in Computer Science (LICS), 332–334 (1986).

[VWS83] M. Y. Vardi, P. Wolper, A. P. Sistla: Reasoning about infinite computation paths, Proc. 24th IEEE Symposium on Foundation of Computer Science, Tuscan, 1983, pages 185–194.

[W94] 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).

[WN94] G. Winskel, M. Nielsen: Models for Concurrency, in S. Abramsky, D. Gabbay (Eds.) Handbook of Logic in Computer Science, Vol. 3, Oxford University Press (1994).

[YJ94] W. Yi, B. Jonsson: Decidability of Timed Language-Inclusion for Networks of Real-Time Communicating Sequential Processes, Proc. FST&TCS 94, LNCS 880 (1994).

[Z87] W. Zielonka: Notes on finite asynchronous automata, R.A.I.R.O.— Inform. Theor. Appl., Vol 21, 99–135 (1987).

List of Publications

1. D. D’Souza and P. S. Thiagarajan: Product Interval Automata: A Subclass of Timed Automata, in Proceedings of 19th Foundations of Software Technology and Theoretical Computer Science (FSTTCS), LNCS 1732 (1999).

2. D. D’Souza and P. S. Thiagarajan: Distributed Interval Automata, Internal Report TCS-98-3, Chennai Mathematical Institute (1998). (Available electronically at www.smi.ernet.in/techreps.)

3. D. D’Souza and P. Madhusudan: On-the-fly verification for Product-LTL, in Proceedings of Seventh National Seminar in Theoretical Computer Science (1997).