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-...
| Principais autores: | , , |
|---|---|
| Formato: | Conference item |
| Publicado em: |
Institute of Electrical and Electronics Engineers
2017
|