@article{FranzleQuaasShirmohammadiWorrell:IPL:2020,
    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.},
    Author = {Fr{\"a}nzle, Martin and Quaas, Karin and Shirmohammadi, Mahsa and Worrell, James},
    File = {Effective definability of the reachability relation in timed automata - 1-s2.0-S0020019019301541-main - a - a - b.pdf},
    ISSN = {0020-0190},
    Journal = {Information Processing Letters},
    Keywords = {Presburger arithmetic, Region automaton, Semilinear sets, Real-time systems},
    Pages = {105871},
    Title = {Effective definability of the reachability relation in timed automata},
    URL = {http://www.sciencedirect.com/science/article/pii/S0020019019301541},
    Volume = {153},
    Year = {2020},
    bdsk-url-1 = {http://www.sciencedirect.com/science/article/pii/S0020019019301541},
    bdsk-url-2 = {https://doi.org/10.1016/j.ipl.2019.105871},
    date-added = {2019-12-09 16:50:31 +0100},
    date-modified = {2020-01-06 12:07:30 +0100},
    doi = {10.1016/j.ipl.2019.105871}
}

@article{FranzleQuaasShirmohammadiWorrell:IPL:2020, 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.}, Author = {Fr{\"a}nzle, Martin and Quaas, Karin and Shirmohammadi, Mahsa and Worrell, James}, File = {Effective definability of the reachability relation in timed automata - 1-s2.0-S0020019019301541-main - a - a - b.pdf}, ISSN = {0020-0190}, Journal = {Information Processing Letters}, Keywords = {Presburger arithmetic, Region automaton, Semilinear sets, Real-time systems}, Pages = {105871}, Title = {Effective definability of the reachability relation in timed automata}, URL = {http://www.sciencedirect.com/science/article/pii/S0020019019301541}, Volume = {153}, Year = {2020}, bdsk-url-1 = {http://www.sciencedirect.com/science/article/pii/S0020019019301541}, bdsk-url-2 = {https://doi.org/10.1016/j.ipl.2019.105871}, date-added = {2019-12-09 16:50:31 +0100}, date-modified = {2020-01-06 12:07:30 +0100}, doi = {10.1016/j.ipl.2019.105871} }