Next: Connected Automata Up: Timed Automata Previous: Timed CTL: TCTL and Contents
Because we assume for tCTL a discrete structure we can apply all the 'usual' methods of model-checking. Nevertheless one has to adapt the algorithms to the changes leaving aside the next-operator and including numerical bounds for the properties.