Problem Set H: Zeno Timed Automaton in H1
We have been made aware that the timed automaton given in exercise H1 of Problem Set H is Zeno while we defined Region Graphs only for non-Zeno timed automata. We have uploaded a new version of the Problem Set where we removed the loops in states s1 and s2 in order to make the timed automaton non-Zeno.
If you already constructed the Region Graph for the timed automaton given in rev 1 although it was Zeno, you may hand in this solution. Otherwise, use the timed automaton given in rev 2. Please point out in your solution which timed automaton you used.
We are sorry for the confusion!
Your Verification Team