Higher-Dimensional Timed and Hybrid Automata

Authors

Uli Fahrenberg

Journal

Leibniz Transactions on Embedded Systems

Type

article

Projects

AA"AA" is not in the list (Vaucanson, Spot, URBI, Olena, APMC, Tiger, Climb, Speaker ID, Transformers, Bison, ...) of allowed values for the "Related project" property.

Date

2022-12-08

Abstract

We introduce a new formalism of higher-dimensional timed automata, based on Pratt and van Glabbeek's higher-dimensional automata and Alur and Dill's timed automata. We prove that their reachability is PSPACE-complete and can be decided using zone-based algorithms. We also extend the setting to higher-dimensional hybrid automata. The interest of our formalism is in modeling systems which exhibit both real-time behavior and concurrency. Other existing formalisms for real-time modeling identify concurrency and interleaving, which, as we shall argue, is problematic.

Bibtex (lrde.bib)

@Article{	  fahrenberg.22.lites,
  title		= {Higher-Dimensional Timed and Hybrid Automata},
  volume	= 8,
  url		= {https://ojs.dagstuhl.de/index.php/lites/article/view/lites-v008-i002-a003},
  doi		= {10.4230/LITES.8.2.3},
  abstract	= {We introduce a new formalism of higher-dimensional timed
		  automata, based on Pratt and van Glabbeek's
		  higher-dimensional automata and Alur and Dill's timed
		  automata. We prove that their reachability is
		  PSPACE-complete and can be decided using zone-based
		  algorithms. We also extend the setting to
		  higher-dimensional hybrid automata. The interest of our
		  formalism is in modeling systems which exhibit both
		  real-time behavior and concurrency. Other existing
		  formalisms for real-time modeling identify concurrency and
		  interleaving, which, as we shall argue, is problematic.},
  number	= 2,
  journal	= {Leibniz Transactions on Embedded Systems},
  author	= {Fahrenberg, Uli},
  year		= 2022,
  month		= dec,
  pages		= {03:1-03:16}
}