Bounded Variability of Metric Temporal Logic

TL;DR

This paper investigates the complexity of determining bounded variability in Metric Temporal Logic, revealing undecidability over dense time and exponential-space complexity over discrete time, with some fragments being more tractable.

Contribution

It establishes the undecidability of bounded variability for MTL over dense time and characterizes the complexity over discrete time, also discussing more manageable MTL fragments.

Findings

Undecidability of bounded variability over dense-time models.

Exponential-space complexity of bounded variability over discrete-time models.

Identification of MTL fragments with more tractable bounded variability reasoning.

Abstract

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 employ 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 Temporal 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 negative results, we also briefly discuss small fragments of MTL that are more amenable to reasoning about bounded variability.