Reasoning with Metric Temporal Logic and Resettable Skewed Clocks

The formal verification of distributed real-time systems is challenging due to the interaction between the local computation and the communication between the different nodes of a network. The overall correctness of the system relies on local properties and timing exchange of data between components. This requires to take into account the drift of local clocks and their synchronization. The reference time of local properties may be given by skewed and resettable (thus non-monotonic) clocks. In this paper, we consider automated reasoning over MTLSK, a variant of MTL over Resettable Skewed Clocks. We focus on metric operators with lower and upper parametric bounds. We provide an encoding into temporal logic modulo the theory of reals and we solve satisfiability with SMT-based model checking techniques. We implemented and evaluated the approach on typical properties of real-time systems.