Effective Definability of the Reachability Relation in Timed Automata

Martin Fränzle; Karin Quaas; Mahsa Shirmohammadi; James Worrell

Effective Definability of the Reachability Relation in Timed Automata

Formal Languages and Automata Theory 2019-03-26 v1

Authors: Martin Fränzle , Karin Quaas , Mahsa Shirmohammadi , James Worrell

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.

Keywords

timed automata reachability relation linear arithmetic definability formal verification

Cite

@article{arxiv.1903.09773,
  title  = {Effective Definability of the Reachability Relation in Timed Automata},
  author = {Martin Fränzle and Karin Quaas and Mahsa Shirmohammadi and James Worrell},
  journal= {arXiv preprint arXiv:1903.09773},
  year   = {2019}
}