Timed Automation :

In automata theory, a timed automaton is a finite automation extended with a finite set of real-valued clocks. During a run of a timed automaton, clock values increase all with the same speed. Along the transitions of the automaton, clock values can be compared to integers. These comparisons form guards that may enable or disable transitions and by doing so constrain the possible behaviours of the automaton. Further, clocks can be reset. Timed automata are a sub-class of a type hybrid automata.
Timed automata can be used to model and analyse the timing behaviour of computer systems, e.g., real-time systems or networks. Methods for checking both safety and liveness properties have been developed and intensively studied over the last 20 years.
It has been shown that the state reachability problem for timed automata is decidable, which makes this an interesting sub-class of hybrid automata. Extensions have been extensively studied, among them stopwatches, real-time tasks, cost functions, and timed games. There exists a variety of tools to input and analyse timed automata and extensions, including the model checkers UPPAAL, Kronos, and the schedulable analyser TIMES. These tools are becoming more and more mature, but are still all academic research tools.

Example :

Before formally defining what a timed automaton is, some examples are given.
Consider the language

{\mathcal L}

of timed-words

w

over the unary alphabet

\{a\}

such that there is an

a

during the first time unit, and there is less than one time unit between two successive

a

. The timed automaton recognizing this language, pictured nearby, use a single clock

x

, which should never be equal to one. This clock counts the time since the start of the run if no

a

were emitted, or from the last

a

emitted otherwise. This means that each time an

a

is emitted, this clock is reset to zero.
Consider the language

{\mathcal L}

of timed-words

w

over the binary alphabet

\{a,b\}

such that each

a

is followed by a

b

in the next time unit. The timed automaton recognizing this language, pictured nearby, recalls whether there was a

a

which was not followed by a

b

or not. If it is not the case, it accepts the run, otherwise it rejects it. Furthermore, when there is such a

a

, it has a clock

x

which recall the time elapsed since the first such

a

was emitted. In this case, a

b

can not be emitted if the clock is at least equal to one, and thus the run fails.

Timed automaton accepting the language a* such that a letter is emitted in each open interval of length one.

Formal Definition :

Timed automaton :

Formally, a timed automaton is a tuple

{\mathcal {A}}=\langle \Sigma ,L,L_{0},C,F,E\rangle

that consists of the following components:

$\Sigma$ is a finite set called the alphabet or actions of ${\mathcal {A}}$ .

$L$ is a finite set. The elements of $L$ are called the locations or states' of ${\mathcal {A}}$ .

$L_{0}\subseteq L$ is the set of start locations.

$C$ is a finite set called the clocks of ${\mathcal {A}}$ .

$F\subseteq L$ is the set of accepting locations.

E\subseteq L\times \Sigma \times {\mathcal {B}}(C)\times {\mathcal {P}}(C)\times L

is a set of edges, called transitions of

{\mathcal {A}}

, where

${\mathcal {B}}(C)$ is the set of clock constraints involving clocks from $C$ , and

${\mathcal {P}}(C)$ is the power of $C$ .

An edge

(\ell ,\sigma ,g,r,\ell ')

from

E

is a transition from locations

\ell

\ell '

with action

\sigma

, guard

g

and clock resets

r

A timed automaton accepting timed words over

\{a,b\}

where each occurrence of

a

is followed less than one time unit later by an occurrence of

b

Extended State :

A pair with a location $\ell$ and a clock valuation $\nu$ is called either an extended state or a state.
Note that the word state is thus ambiguous, since, depending on the author, it may mean either a pair or an element of $L$ . For the sake of the clarity, this article will use the term location for element of $L$ and the term extended location for pairs.
Here lies one of the biggest difference between timed-automata and finite automata. In a finite automaton, at some point of the execution, the state is entirely described by the number of letter read and by a finite number of possible values, which are actually called "states". That means that, given a state and a suffix of the word to read, the remaining of the run is totally determined. Thus, the word "finite" in the name "finite automata". However, as it is explained in the section "run" below, in order to resume clocks are used to determine which transitions can be taken. Thus, in order to know the state of the automaton, you must both know in which location you are, and the clock valuation.

Run :

Given a timed word $w=(\sigma _{1},t_{1}),(\sigma _{2},t_{2}),\dots ,$ with $\sigma _{i}\in \Sigma$ , $(t_{i})_{i}$ an increasing sequence of non-negative number, and a timed-automaton ${\mathcal {A}}$ as above, a run is a sequence of the form $(\ell _{0},\nu _{0}){\xrightarrow[{t_{1}}]{\sigma _{1}}}(\ell _{1},\nu _{1})\dots$ satisfying the following constraint:

(initialization) $\ell _{0}\in L_{0}$

(consecution), for all

i\geq 1

, there exists an edge in

E

of the form

\langle \ell _{i-1},\sigma _{i},g_{i},r_{i},\ell _{i}\rangle

such that:

we assume that $t_{i}-t_{i-1}$ time units passed, and at this time, the guard is satisfied. I.e. $\nu _{i-1}+t_{i}-t_{i-1}$ satisfies $g_{i}$ ,

the new clock valuation $\nu _{i}$ corresponds to $\nu _{i-1}$ , in which $t_{i}-t_{i-1}$ time units passed and in which the clocks of $r_{i}$ where reset. Formally, $\nu _{i}=(\nu _{i-1}+t_{i}-t_{i-1})[r_{i}\rightarrow 0]$ .

The notion of accepting run is defined as in finite automata for finite words and as in Buchi automata for infinite words. That is, if

w

is finite of length

n

, then the run is accepting if

\ell _{n}\in F

. If the word is infinite, then the run is accepting if and only if there exists an infinite number of position

i

such that

\ell _{i}\in F

Deterministic timed automaton :

As in the case of finite and Buchi automaton, a timed-automaton may be deterministic or non-deterministic. Intuitively, being deterministic has the same meaning in each of those case. It means that the set of start locations is a singleton, and that, given a state $s$ , and a letter $a$ , there is only one possible state which can be reached from $s$ by reading $a$ . However, in the case of timed-automaton the formal definition is slightly more complex. Formally, a timed-automaton is deterministic if:

$L_{0}$ is a singleton

for each pair of transitions $(\ell ,\sigma ,g,r,\ell ')$ and $(\ell ,\sigma ,g',r',\ell '')$ , the set of clocks valuations satisfying $g$ is disjoint from the set of clocks valuations satisfying $g'$ .

Closure Property :

The class of languages recognized by non-deterministic timed automata is:

closed under union, indeed, the disjoint union of two timed automata recognize the union of the language recognized by those automata.

closed under intersection.

not closed under complement.

Problems and their complexity :

The computational complexity of some problems related to timed automata are now given.

The emptiness problem for timed automaton can be solved by constructing a region automation and checking whether it accepts the empty language. This problem is PSPACE-complex.

The universality problem of non-deterministic timed automaton is undecidable, and more precisely . However, when the automaton contains a single clock, the property is decidable, however it is not primitive recursive. This problem consists in deciding whether every words are accepted by a timed-automaton.

Alternating timed automaton :

In automata theory, an alternating timed automaton (ATA) is a mix of both timed automation and alternating finite automation. That is, it is a sort of automata which can measure time and in which there exists universal and existential transition.

ATAs are more expressive than timed automaton. one clock alternating timed automaton (OCATA) is the restriction of ATA allowing the use of a single clock. OCATAs allow to express timed languages which can not be expressed using timed-automaton.

Formal definition :

Σ is a finite set called the alphabet or actions of ${\mathcal {A}}$ .

$L$ is a finite set. The elements of $L$ are called the locations or states' of ${\mathcal {A}}$ .

$C$ is a finite set called the clocks of ${\mathcal {A}}$ .

$L_{0}\subseteq L$ is the set of start locations.

$F\subseteq L$ is the set of accepting locations.

$E\subseteq L\times \Sigma \times {\mathcal {B}}(C)\to {\mathcal {B}}^{+}(L\times {\mathcal {P}}(C))$ is the transitions function of ${\mathcal {A}}$ . It is a partial function, defined as explained in the previous section.

Formally, an alternating timed automaton is a tuple ${\mathcal {A}}=\langle \Sigma ,L,L_{0},C,F,E\rangle$ that consists of the following components:

Any Boolean expression can be rewritten into an equivalent expression in disjunctive natural form. In the representation of a ATA, each disjunction is represented by a different arrow. Each conjunct of a disjunction is represented by a set of arrows with the same tail and multiple heads. The tail is labelled by the letter and each head is labelled by the set of clocks it resets.

Closing Thoughts :

Used in Embedded Systems, Mainframe computers etc.

Although the decision to abstract away from quantitative time has had many advantages, it is ultimately Counterproductive when reasoning about systems that must interact with physical processes; the correct functioning of the control system of airplanes and toasters depends crucially upon real-time considerations.

The types of automata we have studied till now do not have any real-time considerations.

In only two decades the theory of timed automata has established itself as an integral part of real-time systems development.

Even Sequential logic can applied through Timed automata in UPPAAL.

Authors :

Vishwakarma Institute of Technology, Pune.
Third-Year Students, Computer Department

Search This Blog

Memory Management in Operating System

Timed Automata and it's Applications

Timed Automation :

Example :

Formal Definition :

Timed automaton :

Extended State :

Run :

Deterministic timed automaton :

Closure Property :

Problems and their complexity :

Alternating timed automaton :

Formal definition :

Closing Thoughts :

Authors :

Kedar Uttarwar.
Danish Tadvi.
Amol Randhir.
Sakshi Shinde

Comments

Post a Comment

Popular posts from this blog

Line coding and their types

Data warehouse modelling with Snowflake Schema

Timed Automata and it's Applications

Timed Automation :

Example :

Formal Definition :

Timed automaton :

Extended State :

Run :

Deterministic timed automaton :

Closure Property :

Problems and their complexity :

Alternating timed automaton :

Formal definition :

Closing Thoughts :

Authors :

Kedar Uttarwar.Danish Tadvi.Amol Randhir.Sakshi Shinde

Comments

Post a Comment

Popular posts from this blog

Line coding and their types

Data warehouse modelling with Snowflake Schema

Kedar Uttarwar.
Danish Tadvi.
Amol Randhir.
Sakshi Shinde