Effective Definability of the Reachability Relation in Timed Automata
arXiv:1903.09773
Abstract
We give a new proof of the result of Comon and Jurski that the binary reachability relation of a timed automaton is definable in linear arithmetic.
arXiv:1903.09773
We give a new proof of the result of Comon and Jurski that the binary reachability relation of a timed automaton is definable in linear arithmetic.