Hostname: page-component-74656f9884-npj9w Total loading time: 0 Render date: 2026-11-10T11:43:31.814Z Has data issue: false hasContentIssue false
  • English
  • Français

Relating timed and register automata†

Published online by Cambridge University Press:  05 December 2014

DIEGO FIGUEIRA ,
PIOTR HOFMAN  and
SŁAWOMIR LASOTA
DIEGO FIGUEIRA*
Affiliation:
University of Edinburgh, 10 Crichton Street, Edinburgh EH8 9AB, United Kingdom INRIA, ENS Cachan, LSV, 61 avenue du Président Wilson 94235 Cachan, France Institute of Informatics, University of Warsaw, Banacha 2, 02-097 Warszawa, Poland Email: dfigueir@inf.ed.ac.uk, ph209519@mimuw.edu.pl, sl@mimuw.edu.pl
PIOTR HOFMAN
Affiliation:
Institute of Informatics, University of Warsaw, Banacha 2, 02-097 Warszawa, Poland Email: dfigueir@inf.ed.ac.uk, ph209519@mimuw.edu.pl, sl@mimuw.edu.pl
SŁAWOMIR LASOTA
Affiliation:
Institute of Informatics, University of Warsaw, Banacha 2, 02-097 Warszawa, Poland Email: dfigueir@inf.ed.ac.uk, ph209519@mimuw.edu.pl, sl@mimuw.edu.pl
*
‡ Corresponding author.
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the 'Save PDF' action button.

Timed and register automata are well-known models of computation over timed and data words, respectively. The former has clocks that allow to test the lapse of time between two events, whilst the latter includes registers that can store data values for later comparison. Although these two models behave differently in appearance, several decision problems have the same (un)decidability and complexity results for both models. As a prominent example, emptiness is decidable for alternating automata with one clock or register, both with non-primitive recursive complexity. This is not by chance.

This work confirms that there is indeed a tight relationship between the two models. We show that a run of a timed automaton can be simulated by a register automaton over ordered data domain, and conversely that a run of a register automaton can be simulated by a timed automaton. These are exponential time reductions hold both in the finite and infinite words settings. Our results allow to transfer decidability results back and forth between these two kinds of models, as well complexity results modulo an exponential time reduction. We justify the usefulness of these reductions by obtaining new results on register automata.

Information

Type
Paper
Information
Mathematical Structures in Computer Science , Volume 26 , Special Issue 6: Special Issue: Express'10 , September 2016 , pp. 993 - 1021
Copyright
Copyright © Cambridge University Press 2014 

Footnotes

†

An extended abstract of this work appeared as Figueira et al. (2010).

The first author acknowledges the financial support of the Future and Emerging Technologies (FET) programme within the Seventh Framework Programme for Research of the European Commission, under the FET-Open grant agreement FOX, number FP7-ICT-233599. The second and third authors acknowledge the financial support of the Polish Ministry of Science grant nr N N206 567840.

References

Abdulla, P. A., Deneux, J., Ouaknine, J. and Worrell, J. (2005) Decidability and complexity results for timed automata via channel machines. In: ICALP 1089–1101.Google Scholar
Alur, R. and Dill, D. L. (1994) A theory of timed automata. Theoretical Computer Science 126 183–235.Google Scholar
Benedikt, M., Ley, C. and Puppis, G. (2010) What you must remember when processing data words. In: AMW.Google Scholar
Bojańczyk, M. and Lasota, S. (2012) A machine-independent characterization of timed languages. In: Proceedings ICALP'12. Springer Lecture Notes in Computer Science 7392 92–103.Google Scholar
Bojańczyk, M., Klin, B. and Lasota, S. (2011) Automata with group actions. In: Proceedings LICS'11 355–364.Google Scholar
Bouyer, P., Markey, N., Ouaknine, J., Schnoebelen, P. and Worrell, J. (2008) On termination for faulty channel machines. In: STACS 121–132.Google Scholar
Bouyer, P., Petit, A. and Thérien, D. (2003) An algebraic approach to data languages and timed languages. Information and Computation 182 (2) 137–162.Google Scholar
Chambart, P. and Schnoebelen, P. (2008) The ordinal recursive complexity of lossy channel systems. In: LICS, IEEE Computer Society Press 205–216. Available at http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CS-lics08.pdf.Google Scholar
Demri, S. and Lazić, R. (2009) LTL with the freeze quantifier and register automata. ACM Transactions on Computational Logic (TOCL) 10 (3) Article No. 16, ACM.Google Scholar
Figueira, D., Figueira, S., Schmitz, S. and Schnoebelen, P. (2011) Ackermannian and primitive-recursive bounds with Dickson's lemma. In: Proceedings of the 26th Annual IEEE Symposium on Logic in Computer Science (LICS), Toronto, Ontario, Canada 269–278. Available at: http://doi.ieeecomputersociety.org/10.1109/LICS.2011.39.Google Scholar
Figueira, D., Hofman, P., and Lasota, S. (2010) Relating timed and register automata. In: Proceedings 17th International Workshop on Expressiveness in Concurrency, EXPRESS'10, Paris, France 61–75. Available at: http://dx.doi.org/10.4204/EPTCS.41.5.Google Scholar
Figueira, D. and Segoufin, L. (2009) Future-looking logics on data words and trees. In: MFCS 331–343.Google Scholar
Jenkins, M., Ouaknine, J., Rabinovich, A. and Worrell, J. (2010) Alternating timed automata over bounded time. In: LICS, IEEE Computer Society Press.Google Scholar
Kaminski, M and Francez, N. (1994) Finite-memory automata. Theoretical Computer Science 134 (2) 329–363.Google Scholar
Lasota, S. and Walukiewicz, I. (2005) Alternating timed automata. In: FoSSaCS 250–265.Google Scholar
Lasota, S. and Walukiewicz, I. (2008) Alternating timed automata. ACM Transactions on Computational Logic (TOCL) 9 (2) Article No. 10, ACM.Google Scholar
Lazić, R. (2006) Safely freezing LTL. In: FSTTCS 381–392.Google Scholar
Lazić, R. (2008) Safety alternating automata on data words. In: CoRR, ArXiv:0802.4237.Google Scholar
Löb, M. H. and Wainer, S. S. (1970) Hierarchies of number theoretic functions, I. Archiv für Mathematische Logik und Grundlagenforschung 13 39–51.Google Scholar
Neven, F., Schwentick, T. and Vianu, V. (2004) Finite state machines for strings over infinite alphabets. ACM Transactions on Computational Logic 5 (3) 403–435.Google Scholar
Ouaknine, J. and Worrell, J. (2004) On the language inclusion problem for timed automata: Closing a decidability gap. In: LICS, IEEE Computer Society Press 54–63.Google Scholar
Ouaknine, J. and Worrell, J. (2005) On the decidability of metric temporal logic. In: LICS, IEEE Computer Society Press 188–197.Google Scholar
Ouaknine, J. and Worrell, J. (2006) Safety metric temporal logic is fully decidable. In: TACAS 411–425.Google Scholar
Parys, P. and Walukiewicz, I. (2009) Weak alternating timed automata. In: ICALP 273–284.Google Scholar
Parys, P. and Walukiewicz, I. (2011) Personal communication.Google Scholar
Schnoebelen, P. (2010) Revisiting Ackermann-Hardness for lossy counter machines and reset Petri nets. In: MFCS 2010. Springer Lecture Notes in Computer Science 6281 616–628. Available at: http://dx.doi.org/10.1007/978-3-642-15155-2_54.Google Scholar