Parametric deadlock-freeness checking timed automata

Abstract

Distributed real-time systems are notoriously difficult to design,and must be verified,e. g.,using model checking. In particular,deadlocks must be avoided as they either yield a system subject to potential blocking,or denote an ill-formed model. Timed automata are a powerful formalism to model and verify distributed systems with timing constraints. In this work,we investigate synthesis of timing constants in timed automata for which the model is guaranteed to be deadlock-free.