Time constraints are usually used in timed systems to rule on discrete behaviours based on the valuations of clocks. They are categorized into diagonal-free constraints and diagonal constraints. In timed automata, it is well-known that diagonal constraints are just a useful syntax sugar since each diagonal constraint can be encoded into diagonal-free constraints. However, it is yet unknown when recursion is taken into consideration. This paper investigates the decidability results of these systems with diagonal constraints, under the model of nested timed automata (NeTAs). We show that the NeTAs containing a singleton global clock with diagonal constraints are Turing complete, even when the clock assignment is restricted to the clock reset. In comparison, the reachability problem for a subclass, NeTAs without frozen clocks, is decidable under diagonal constraints.
CITATION STYLE
Wang, Y., Wen, Y., Li, G., & Yuen, S. (2017). Nested Timed Automata with Diagonal Constraints. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 10610 LNCS, pp. 396–412). Springer Verlag. https://doi.org/10.1007/978-3-319-68690-5_24
Mendeley helps you to discover research relevant for your work.