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, i.e., 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 CosyVerif handles several of them:

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

Some references