Relating Reachability Problems in Timed and Counter Automata

Issue title: Reachability Problems for Infinite State Systems

Guest editors: Parosh Aziz Abdulla, Stéphane Demri, Alain Finkel, Jérôme Leroux and Igor Potapov

Article type: Research Article

Authors: Haase, Christoph^{a; *; †} | Ouaknine, Joël^b | Worrell, James^b

Affiliations: [a] Laboratoire Spécification et Vérification (LSV), CNRS, École Normale Supérieure (ENS) de Cachan, 61, avenue du Président Wilson, 94235 Cachan Cedex, France. [email protected] | [b] Department of Computer Science, University of Oxford, Parks Rd, OX1 3QD, Oxford, United Kingdom. [email protected]; [email protected]

Correspondence: [†] Address for correspondence: Laboratoire Spécification et Vérification (LSV), CNRS, École Normale Supérieure (ENS) de Cachan, 61, avenue du Président Wilson, 94235 CACHAN Cedex, France

Note: [*] Supported by the French Agence Nationale de la Recherche (ANR), ReacHard (grant ANR-11-BS02-001). Parts of this paper appeared in the author’s Ph.D. thesis [1].

Abstract: We establish a relationship between reachability problems in timed automata and space-bounded counter automata. We show that reachability in timed automata with three or more clocks is logarithmic-space inter-reducible with reachability in space-bounded counter automata with two counters. We moreover show the logarithmic-space equivalence of reachability in two-clock timed automata and space-bounded one-counter automata. This last reduction has recently been employed by Fearnley and Jurdziński to settle the computational complexity of reachability in two-clock timed automata.

Keywords: timed automata, counter automata, reachability, infinite-state systems

DOI: 10.3233/FI-2016-1316

Journal: Fundamenta Informaticae, vol. 143, no. 3-4, pp. 317-338, 2016