MeFoSyLoMa CNRS Iniria
QR Code
Last modified
June 28, 2016

Jun 25, 2017
The Automata-based Services

Finite State Automata

A finite-state automaton is a mathematical model used to design computer programs and digital logic circuits. It is conceived as an abstract machine that can be in one of a finite number of states. The machine is in only one state at a time; the state it is in at any given time is called the current state. It can change from one state to another when initiated by a triggering event or condition, this is called a transition. A particular FSM is defined by a list of the possible transition states from each current state, and the triggering condition for each transition.

Timed Automata

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:

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

Some references