Revisiting reachability in timed automata
We revisit a fundamental result in real-time verification, namely that the binary reachability relation between configurations of a given timed automaton is definable in linear arithmetic over the integers and reals. In this paper we give a new and simpler proof of this result, building on the well-...
| Main Authors: | , , |
|---|---|
| Format: | Conference item |
| Published: |
Institute of Electrical and Electronics Engineers
2017
|