Verification Bernd Finkbeiner


Problem Set H: Zeno Timed Automaton in H1

Written: 11.12.2019 15:53 Written By: Noemi Passing

Dear students,

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

Privacy Policy | Legal Notice
If you encounter technical problems, please contact the administrators