Timed Automata & Its Applications
Model checking is gaining traction as a useful method for troubleshooting complex reactive systems like embedded controllers and network protocols. Traditional model checking techniques do not allow for explicit time modelling, making them unsuitable for analysing real-time systems whose correctness is dependent on the relative magnitudes of distinct delays. As a result, timed automata were developed as a formal notation for modelling real-time systems’ behaviour.
Let’s consider the below example before fully describing what a timed automaton is.
Consider the language L of timed-words w over the unary alphabet {a}, where the initial time unit contains an {a} and the time between two consecutive an is less than one time unit. A single clock x, which shall never be equal to one, is used by the timed automaton that recognises this language (seen nearby). If no a were emitted at the start of the run, this clock counts the time since the last a was broadcast. This signifies that this clock is reset to zero every time an a is emitted.
A finite automaton that has been augmented with a finite number of real-valued clocks is known as a timed automata. Clock values all grow at the same rate during a run of a timed automaton. Clock values can be compared to integers along the automation’s transitions. These comparisons serve as guards, enabling or disabling transitions and therefore limiting the automation’s possible behaviours. Clocks can also be reset. Timed automata are a type of hybrid automata subclass.
A timed automaton is essentially a finite automaton (a graph with a finite number of nodes or locations and a finite number of labelled edges) with real-valued variables added to it. An automaton like this can be thought of as an abstract model of a timed system. The variables represent the system’s logical clocks, which start at zero when the system is turned on and thereafter increase synchronously at the same rate. Clock restrictions, or edge guards, are used to limit the automaton’s behaviour. When the clock values fulfil the guard labelled on the edge, a transition represented by an edge can be taken. When a transition is made, clocks may be reset to zero.
Figure 2(a) shows an example of a timed automaton. Two clocks are in charge of the automaton’s timing behaviour. The self-loop in the location loop is controlled by the clock. The loop’s single transition may occur when.
The execution of the entire automaton is controlled by the clock. When the interval is between 10 and 20, the automaton can start at any time; when the interval is between 40 and 50, it can go from loop to finish, and so on.
Timed Büchi Automata
With a Timer A guard on an automaton’s edge is merely an enabling condition for the transition represented by the edge; it can’t make the transition happen. For example, the aforementioned automaton could idle in any area indefinitely. The problem is solved in the original work by Alur and Dill by introducing Büchi-acceptance conditions, in which a subset of the locations in the automaton are marked as accepting, and only those executions passing through an accepting location infinitely often are considered valid automaton behaviours. Consider the automata in Fig. 2(a) again, and assume that the end is indicated as accepting.. When the value of is at most 20, the position start must be left; otherwise, the automaton will become trapped in start and will never be able to enter end. Similarly, the automaton must exit the loop when it reaches a maximum of 50 to be allowed to enter the end.
Timed Safety Automata
In timed safety automata, a more intuitive concept of progress is presented. Instead of accepting conditions, locations in timed safety automata might be constrained by location invariants, which are local timing constraints. An automaton can stay in a place as long as the clock values satisfy the location’s invariant requirement. Consider Fig. 2(b), which is a timed safety automaton that corresponds to the Büchi automaton in Fig. 2(a) with the end designated as an accepted location.
The invariant provides a local condition that start and finish must be left when the number is at most 20, and loop must be left when the number is at most 50. This provides a localised perspective of the automaton’s timing behaviour in each area.
Tools for Timed Systems
Several tools implement timed (and hybrid) automata.
• HYTECH
is a linear hybrid automata model checker. Reachability qualities can be tested by doing exact backward and forward computations (but there is of course no guarantee the computation will terminate). Many more operations on polyhedra are possible, such as variable hiding (equivalent to projections), “while” loops, emptiness tests, and so on. HYTECH is a Berkeley-based technology (USA).
• KRONOS
is a timed automata model checker. Backward and forward computations, both exact and abstract, are possible. There is also a backward method for the logic TCTL. The KRONOS tool, which was created in Grenoble (France)
• UPPAAL
is a timed automata model checker that performs forward analysis with extrapolation. With some additional capabilities such as bounded integer variables and broadcast channels, it can validate reachability properties of timed systems. The UPPAAL tool was created in collaboration between Aalborg University in Denmark and Uppsala University in Sweden (Sweden).
Applications.
Automata-theoretic Verification.
The reachability analysis that has been discussed is sufficient for checking the safety properties of real-time systems. We need to evaluate non-terminating, infinite executions to test liveness features such “if a request occurs infinitely often, so does the response.” Using an automata-theoretic method, both safety and liveness qualities may be specified and verified in a uniform and elegant manner. A timed automata, sometimes with acceptance conditions (e.g. B uchi), is considered as a generator of a timed language — a set of sequences in which each symbol is associated with a real-valued time of occurrence.
Verification refers to questions regarding the timed language defined by the system’s timed automata. When a timed automaton accepts unwanted behaviours, the verification challenge is reduced to confirming the intersection’s emptiness, which can be handled in Pspace. In contrast, if the question is given by a timed automaton that accepts all behaviours that satisfy the required property, verification corresponds to verifying the inclusion of the two timed languages, and is in general undecidable.
The language-inclusion problem’s decidability can be ensured by demanding a deterministic specification automaton, such as an event-clock automaton. Various attempts have been made to establish an equivalent theory of timed languages since theory of regular (or ω -regular) languages has many applications, including modelling of discrete systems. The timed variant of S1S, timed regular expressions, and timed temporal logics can all be used to describe timed languages defined by timed automata. In, the complexity of various membership problems for timed automata is investigated. Under union and intersection, but not complementation, timed languages definable by timed automata are closed. This has led to the discovery of subclasses with superior closure qualities, such as event-clock automata.
Equivalence and Refinement Relations. While the undecidability of timed language equivalence for timed automata, stronger equivalences such as timed bisimulation and simulation can be determined. A timed bisimulation is an equivalence relation ∼ on the state-space QA for a timed automaton A such that whenever q1∼ q2, if q1a →q0 for a∈ Σ ∪ IR, then there exists q2 with q2a→ q2 and q1∼ q2. While the maximal timed bisimulation relation has an infinite number of equivalence classes, the problem of determining whether a timed bisimulation exists that connects two specified initial states is surprisingly decidable (the algorithm involves analysing the region automaton of the product space Q(A) × Q(A)).
The same proof technique can be used to develop algorithms for determining whether a timed simulation exists (timed simulation relations are useful for establishing refinement between descriptions at different levels of abstractions). Exptime is the level of difficulty in deciding on a timed (bi)simulation. The number of clocks that an observer must utilise to discriminate between two timed automata can be used to establish a hierarchy of approximations to the timed bisimulation relation. In, the effect of the observer’s clock precision on differentiating ability is investigated.
Linear real-time temporal logics.
Linear temporal logic (Ltl) is a popular formalism for writing requirements regarding computations of reactive systems. A variety of real-time extensions of Ltl have been proposed for writing requirements of real-time systems . In particular, the real-time temporal logic Metric Interval Temporal Logic (Mitl) admits temporal connectives such as always, eventually, and until, subscripted with intervals. A typical bounded-response requirement that “every request p must be followed by a response q within 3 time units” is expressed by the Mitl formula ( p -> ≤3 q). To verify whether a real-time system modeled as a timed automaton A satisfies its specification given as a Mitl formula ϕ, the model checking algorithm constructs a timed automaton A¬ϕ that accepts all timed words that violate ϕ, and checks whether the product of A with A¬ϕ has a nonempty language .
The definition of Mitl requires the subscripting intervals to be nonsingular. In fact, admitting singular intervals as subscripts (e.g. formulas of the form (p→=1 q)) makes translation from Mitl to timed automata impossible, and the satisfiability and model checking problems for the resulting logic are undecidable.. Many tools for symbolic model checking employ the branching-time logic Ctl as a specification language.The real-time logic Timed Computation Tree Logic (Tctl) allows temporal connectives of Ctl to be subscripted with intervals. For instance, the bounded response property that “every request p must be followed by a response q within
3 time units” is expressed by the Tctl formula ∀ ( p→∀ ≤3q). It turns out that two states that are region-equivalent satisfy the same set of Tctl Formulas. Consequently, given a timed automaton A and a Tctl-formula ϕ, the computation the set of states of A that satisfy ϕ, can be performed by a labeling algorithm that labels the vertices of the region automaton R(A) with
subformulas of ϕ starting with innermost subformulas . Alternatively, the symbolic model checking procedure computes the set of states satisfying each subformula by a fixpoint routine that manipulates zone constraints .
Probabilistic models.
Modeling restrictions such as “the delay between the input event a and the output event b is distributed equally between 1 and 2 seconds” are possible using probabilistic extensions of timed automata. The semantics of the verification question alter when probabilities are introduced. Verification refers to showing that the likelihood that the run of the system A generates a word accepted by AS is zero, given a probabilistic timed automata A and a specification automaton AS that accepts the unacceptable behaviours.
This difficulty can be solved by modifying the cycle detection technique on the region automata of the product of A and AS. Tctl characteristics of a probabilistic timed automaton can be verified using a similar way. When explicit probabilities are included in the criteria (for example, event a will occur within time 2 with a probability of at least 0.5), model verification procedures are only known for a discrete model of time.
Hybrid systems.
The timed automata model has been extended to include continuous variables other than clocks, such as temperature and defective clocks. Hybrid automata can be used to simulate discrete controllers that are embedded in a dynamic environment. In general, there is no consensus on how to verify hybrid automata. Analysis is available for the subclass of rectangular automatas by language-preserving translation to timed automatas, and for the subclass of linear hybrid automatas via symbolic fixpoint computing using polyhedra..
Conclusion
The basic model of timed automata has been explained in this blog. The area automaton construction is one of the most essential and fundamental in this domain: it finitely abstracts behaviours of timed automata into behaviours of finite automata, allowing model-checking of many features. We also discussed several extensions of timed automata, with a focus on the decidability of model-checking reachability conditions. There have been so many works devoted to timed systems in general, and timed automata in particular, that presenting the entire theory of timed automata in a single blog is impossible. The current blog discusses several results on timed automata, with an emphasis on the decidability of reachability conditions and some applications based on timed automata
Authors
Vishwakarma Institute of Technology, Pune
- Shabbir Asgar Tankiwala
- Shivansh Rastogi
- Shriraj Sonawane
- Nikhil Sontakke
- Sejal Utekar