Higher-Dimensional Timed and Hybrid Automata

From LRDE

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}
}