Timed Automata (Alur, '97)

Terminology:
- location
- switch
- invariant
- time constraint
- labels
- clocks

- A := (L, L0, Sigma, X, I, E)
- E := (s, a, phi, s')

The semantics is a transition system with infinite states and transitions
- because of clock increments
- transition can due to taking a switch or increment of clock(s).

Defining an equivalent relation ~ with automata with finite quotients:
- there are three requirements: stable, Lf-sensitive, and finite.
- examples are zone and region automata

Constructing zone automata can be done algorithmically:
- starting from the initial zone (s0, v), where v is a clock zone, or a set of clock constraints.
- we can apply a formula to derive the next clock zone

Solving the reachability problem for the zone automata is the same as the original timed automata
- there are only finite # of zones
- can be structured as BDD problem


two systems are bisimilar if they match each other's moves