Bounded Variability of Metric Temporal Logic

Previous work has shown that reasoning with real-time temporal logics is often simpler when restricted to models with bounded variability—where no more than v events may occur every V time units, for given v, V. When reasoning about formulas with intrinsic bounded variability, one can em-ploy the simpler techniques that rely on bounded variability, without any loss of generality. What is then the complexity of algorithmically deciding which formulas have intrinsic bounded variability? In this paper, we study the problem with reference to Metric Tem-poral Logic (MTL). We prove that deciding bounded variability of MTL formulas is undecidable over dense-time models, but with a undecidability degree lower than generic dense-time MTL satisfiability. Over discrete-time models, instead, deciding MTL bounded variability has the same exponential-space complexity as satisfiability. To complement these nega-tive results, we also briefly discuss small fragments of MTL that are more amenable to reasoning about bounded variability. 1 The Benefits of Bounding Variability In yet another instance of the principle that “there ain’t no such thing as a free lunch”, expressiveness of formal languages comes with a significant cost to pay in terms of complexity—and possibly undecidability—of algorithmic analysis. The trade-off between expressiveness and complexity is particularly critical for the real-time temporal logics, which dwell on the border of intractability. A chief research challenge is, therefore, identifying expressive temporal logic fragments without letting the “dark side ” of undecidability [6] prevail and abate practical usability