A Theory of Sampling for Continuous-time Metric Temporal Logic

TL;DR

This paper investigates how sampling affects the semantics of Metric Temporal Logic (MTL) in continuous and discrete-time models, providing a foundation for reducing continuous-time verification to discrete-time.

Contribution

It establishes the relationship between continuous and discrete-time MTL satisfiability, enabling automated discretization techniques for system verification.

Findings

Sampling preserves MTL semantics for flat formulas

Discrete-time sequences can approximate continuous-time models

Reduction of continuous-time verification to discrete-time is feasible

Abstract

This paper revisits the classical notion of sampling in the setting of real-time temporal logics for the modeling and analysis of systems. The relationship between the satisfiability of Metric Temporal Logic (MTL) formulas over continuous-time models and over discrete-time models is studied. It is shown to what extent discrete-time sequences obtained by sampling continuous-time signals capture the semantics of MTL formulas over the two time domains. The main results apply to "flat" formulas that do not nest temporal operators and can be applied to the problem of reducing the verification problem for MTL over continuous-time models to the same problem over discrete-time, resulting in an automated partial practically-efficient discretization technique.