Skip to Main content Skip to Navigation
Journal articles

Revisiting Reachability in Polynomial Interrupt Timed Automata

Abstract : Polynomial Interrupt Timed Automata (PolITA) are finite automata with clocks organized along hierarchical levels. These clocks are equipped with an interruption mechanism, well suited to the modeling of real-time operating systems. Moreover, transitions between states contain polynomial guards and updates. The reachability problem in this class is known to be in 2EXPTIME with a decision procedure based on the cylindrical algebraic decomposition. We improve this complexity to EXPSPACE mainly using a combinatorial argument and we include a reduction leading to a PSPACE lower bound.
Document type :
Journal articles
Complete list of metadata
Contributor : Gestionnaire Hal-Su Connect in order to contact the contributor
Submitted on : Thursday, October 21, 2021 - 2:26:26 PM
Last modification on : Tuesday, January 4, 2022 - 6:39:15 AM


 Restricted access
To satisfy the distribution rights of the publisher, the document is embargoed until : 2023-03-30

Please log in to resquest access to the document



Béatrice Bérard, Serge Haddad. Revisiting Reachability in Polynomial Interrupt Timed Automata. Information Processing Letters, Elsevier, 2022, 174, pp.106208. ⟨10.1016/j.ipl.2021.106208⟩. ⟨hal-03390569⟩



Les métriques sont temporairement indisponibles