Timed automata

From Wikipedia, the free encyclopedia

Timed automata is mostly the formal modeling and verification of timed and hybrid systems. It was primarily designed by Rajiv Alur.

Contents 1 Introduction 2 Kinds of transitions 3 Formal Syntax 4 Grammer of the constraints 5 Building a model 6 References 7 Category

[edit] Introduction

Timed automata concentrates on working with state machines and dynamic systems together. Most often, for dynamic systems, there is the rate of change of a variable, say x. Consider a hand torch. If the key is clicked twice, it should be brighter. If it is clicked slowly twice, it shuts off. Here the change is modeled in time. If the duration of the second click extends beyond a threshold, the light should be shut off. Mostly a reset is modeled from wherein we consider a change or input. Most transitions have a "guard" , basically a condition check on the timers. For example, in the above case, when the button is clicked once, a clock x is reset. Now, the clock starts. If the button is clicked within 2 seconds, then the light should be brighter. So the guard is
if x<=2 then BRIGHTER
else OFF

[edit] Kinds of transitions

There are 2 kinds of transitions, once where one or many clocks get reset over the transition and the other - if the system waited on the transition for δ period of time, the clocks ( all of them) undergo incrementation by δ.

[edit] Formal Syntax

The formal syntax is, A = < L , L₀ , Σ , X , I , E > , where L is the set of states, L₀ is the set of initial states, Σ is the set of labels, X is the set of clocks, I is the set of Invariants and E is the set of edges.
The edges are further defined by the state its going out from, the state it is going into, the clocks that will be reset, the constraints and the labels.

[edit] Grammer of the constraints

if you assume X to be the clock and K to be a constant, φ : = X >= K | X <= K | X > K | X < K | φ₁ AND φ₂

[edit] Building a model

Building a model mostly consist of identifying key variables and constructing states guarded by time constraints. As a simultaneous functioning of these systems, we can check and verify properties for a real system.

[edit] References

• Rajeev Alur and David L. Dill (1994). "A theory of timed automata". Theoretical Computer Science 126 (2): 183-235. 

[edit] Category

Formal methods