This thesis defines a class of decidable real-time formalisms, intended for automatic synthesis of real-time reactive programs. It defines a temporal logic, a family of automata, and a corresponding classical logic. This temporal logic, as expressive as MITL, is axiomatised.
|Effective start/end date||1/10/95 → 7/06/99|
- decision procedure
- real time
- temporal logic