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

https://hal.sorbonne-universite.fr/hal-03390569
Contributor : Gestionnaire Hal-Su Connect in order to contact the contributor
Submitted on : Thursday, October 21, 2021 - 2:26:26 PM
Last modification on : Monday, December 6, 2021 - 5:12:03 PM

File

 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

Identifiers

Citation

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⟩

Share

Metrics

Record views

34