Revisiting Reachability in Timed Automata
Logic in Computer Science
2017-04-20 v2
Abstract
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-known reachability analysis of timed automata involving difference bound matrices. Using this new proof, we give an exponential-space procedure for model checking the reachability fragment of the logic parametric TCTL. Finally we show that the latter problem is NEXPTIME-hard.
Cite
@article{arxiv.1702.03450,
title = {Revisiting Reachability in Timed Automata},
author = {Karin Quaas and Mahsa Shirmohammadi and James Worrell},
journal= {arXiv preprint arXiv:1702.03450},
year = {2017}
}