Last modified

June 28, 2016

Displayed

Jun 25, 2017

June 28, 2016

Displayed

Jun 25, 2017

The Automata-based Services

A **finite-state automaton** is a

A **Timed Automaton** (TA) is a standard finite state
automaton extended with *clocks*, viz., real-valued variables evolving
uniformly. Such clocks can be compared with integers in guards (constraint
that has to be verified to fire a transition) and invariants (constraint that
has to be verified to remain in a discrete state). Some of the clocks can be
reset when firing transitions. Extensions of the formalism allow clocks to be
compared with other clocks, to be set to arbitrary values (updates), or to be
stopped (stopwatches).

Timed Automata were first defined by Rajev Alur and David Dill in the early 1990s. Since then, much research has been performed to study Timed Automata and their subclasses or variants. Many (but not all) problems related to TAs are decidable, which makes TA a powerful and widely used formalism for specifying and verifying real time systems.

There are numerous classes of Finite-State / Timed Automata and handles several of them:

- Finite State Automata,
- Timed Automata,
- Parametric Timed Automata,
- Timed Automata with Stopwatches,
- Parametric Timed Automata with Stopwatches,
- Linear Hybrid Automata.

The pages in this section present the formalism itself, some illustrating examples, as well as the services for Timed Automata-based Verification available in .

- "Finite State Automata", Wikipedia (last accessed in 2013)