2020/07/03 by Emily Clément, Thierry Jéron, Clement, Emily +6
Computer Science · #FOS: Computer and information sciences #Formal Languages and Automata Theory (cs.FL) #Formal Methods in Verification #Petri Nets in System Modeling #Real-Time Systems Scheduling
paper · pdf · doi:10.48550/arxiv.2007.01815
openalex publication_date 2020/07/03 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
Timed automata are a convenient mathematical model for modelling and reasoning about real-time systems. While they provide a powerful way of representing timing aspects of such systems, timed automata assume arbitrary precision and zero-delay actions; in particular, a state might be declared reachable in a timed automaton, but impossible to reach in the physical system it models. In this paper, we consider permissive strategies as a way to overcome this problem: such strategies propose intervals of delays instead of single delays, and aim at reaching a target state whichever delay actually takes place. We develop an algorithm for computing the optimal permissiveness (and an associated maximally-permissive strategy) in acyclic timed automata and games.