Higher-Dimensional Timed Automata
For verification of concurrent timed systems, this formalism offers a new way to model concurrency and time, but the results are theoretical and incremental.
The paper introduces higher-dimensional timed automata, combining higher-dimensional automata with timed automata, and proves reachability is PSPACE-complete with zone-based algorithms. It also addresses state-space explosion via tensor products and extends to hybrid automata.
We introduce a new formalism of higher-dimensional timed automata, based on van Glabbeek's higher-dimensional automata and Alur's timed automata. We prove that their reachability is PSPACE-complete and can be decided using zone-based algorithms. We also show how to use tensor products to combat state-space explosion and how to extend the setting to higher-dimensional hybrid automata.