Symbolic Automata for MTL∞0 with Super-Dense Semantics

Abstract

Many real-time systems, especially those involving hybrid dynamics, are more accurately modeled using super-dense time semantics. Metric temporal logics have been mostly studied under pointwise and dense-time semantics, and there is no principled automata construction for the super-dense case. This prevents the application of automata-based techniques for the symbolic verification of metric temporal properties. In this paper, we present a novel construction that translates MTL∞ 0 into Symbolic Timed Transition Systems (STTS) under super-dense semantics. Our approach addresses the unique challenge posed by super-dense time, i.e., the alignment of the truth value of subformulas, that can change during timed transitions, and of the corresponding variables in the STTS, that are restricted to change only during instantaneous transitions. The translation is proved correct and experimentally validated with an implementation on top of nuXmv.