Timed scenarios: Consistency, equivalence and optimization

Abstract

We develop a new method for determining the consistency of timed scenarios. If the scenario is consistent, we obtain a canonical representation for the entire class of equivalent scenarios. This allows us to optimise a scenario according to various criteria. In particular, we are able to minimize the largest constant in the scenario’s set of constraints: this technique is directly relevant to decreasing the costs of verification for timed automata synthesized from timed scenarios.