License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ICALP.2018.118
URN: urn:nbn:de:0030-drops-91228
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2018/9122/
Go to the corresponding LIPIcs Volume Portal

Clemente, Lorenzo ; Lasota, Slawomir

Binary Reachability of Timed Pushdown Automata via Quantifier Elimination and Cyclic Order Atoms

pdf-format:
LIPIcs-ICALP-2018-118.pdf (0.5 MB)

Abstract

We study an expressive model of timed pushdown automata extended with modular and fractional clock constraints. We show that the binary reachability relation is effectively expressible in hybrid linear arithmetic with a rational and an integer sort. This subsumes analogous expressibility results previously known for finite and pushdown timed automata with untimed stack. As key technical tools, we use quantifier elimination for a fragment of hybrid linear arithmetic and for cyclic order atoms, and a reduction to register pushdown automata over cyclic order atoms.

BibTeX - Entry

@InProceedings{clemente_et_al:LIPIcs:2018:9122,
  author =	{Lorenzo Clemente and Slawomir Lasota},
  title =	{{Binary Reachability of Timed Pushdown Automata via Quantifier Elimination and Cyclic Order Atoms}},
  booktitle =	{45th International Colloquium on Automata, Languages, and  Programming (ICALP 2018)},
  pages =	{118:1--118:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-076-7},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{107},
  editor =	{Ioannis Chatzigiannakis and Christos Kaklamanis and D{\'a}niel Marx and Donald Sannella},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2018/9122},
  URN =		{urn:nbn:de:0030-drops-91228},
  doi =		{10.4230/LIPIcs.ICALP.2018.118},
  annote =	{Keywords: timed automata, reachability relation, timed pushdown automata, linear arithmetic}
}

Keywords: timed automata, reachability relation, timed pushdown automata, linear arithmetic
Collection: 45th International Colloquium on Automata, Languages, and Programming (ICALP 2018)
Issue Date: 2018
Date of publication: 04.07.2018

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI