Computing maximally-permissive strategies in acyclic timed automata

TL;DR

This paper introduces an algorithm to compute maximally-permissive strategies in acyclic timed automata, addressing the gap between theoretical reachability and physical system constraints by proposing delay intervals.

Contribution

It presents the first algorithm for computing optimal permissiveness in acyclic timed automata and games, enhancing the modeling of real-time systems with more realistic delay considerations.

Findings

Algorithm computes maximally-permissive strategies effectively.

Addresses discrepancy between automata reachability and physical system constraints.

Applicable to acyclic timed automata and games.

Abstract

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.