Skip to content

T
tiamo

Home

Last edited by Maximilien COLANGE
Page history

TiAMo is designed as a platform for the experimental assessment and comparison of model-checking algorithms for timed weighted automata.

Timed Automata

A timed automaton is a finite automaton together with a finite set of clocks.
Clocks evolve at the same pace in the automaton states (or locations).
Transitions are guarded by conditions (comparisons agains integer constants) on clock values.
Transitions are also allowed to reset clocks to zero.

A location together with a value for every clock forms a configuration of the automaton.

Timed Weighted Automata

A timed weighted automaton is further equipped with weights (or costs) both in locations and on transitions. The weight of location multiplies with the time spent in it, while the the weight of a transitions adds to the weight of the run.

TiAMo

TiAMo is currently focused on the reachability and optimal reachability tasks:

  • reachability: is a given location reachable from the initial state (initial location, all clocks set to zero)?
  • optimal reachability: what is the smallest cost to reach a given location from the initial states?

The main difficulty of model-checking such systems stems from the continuous nature of time. An automaton has uncountably many configurations, each of which has uncountably many successors.