Two examples of verification of multirate timed automata with Kronos

Abstract

Multirate timed automata are an extension of timed automata where each clock has its own speed varying between a lower and an upper bound that may change from one control location to another. This formalism is well-suited for specifying hybrid systems where the dynamics of the continuous variables are defined or can be approximated by giving the minimal and maximal rate of change. To avoid the difficulties inherent in the verification of multirate timed automata, we follow an approach that consists of first transforming the multirate timed automata into timed automata and then applying the symbolic techniques implemented in KRONOS. We show the practical interest of this approach analyzing two examples recently proposed in the literature and considered to be realistic case studies: a manufacturing plant and the Philips audio control protocol.