Metric Temporal Logic with Counting

TL;DR

This paper extends Metric Temporal Logic with counting modalities, enhancing its expressive power while maintaining decidability through a reduction to standard MTL, enabling more precise specifications of resource-bounded real-time systems.

Contribution

It introduces and studies the logic CTMTL with counting modalities, proving its decidability via reduction to MTL, and explores its expressive power using EF games with counting moves.

Findings

Decidability of CTMTL established through reduction to MTL.

Expressive power of CTMTL characterized using EF games.

Extension of MITL with counting modalities is elementarily decidable.

Abstract

Ability to count number of occurrences of events within a specified time interval is very useful in specification of resource bounded real time computation. In this paper, we study an extension of Metric Temporal Logic ($\mathsf{MTL}$) with two different counting modalities called $\mathsf{C}$ and $\mathsf{UT}$ (until with threshold), which enhance the expressive power of $\mathsf{MTL}$ in orthogonal fashion. We confine ourselves only to the future fragment of $\mathsf{MTL}$ interpreted in a pointwise manner over finite timed words. We provide a comprehensive study of the expressive power of logic $\mathsf{CTMTL}$ and its fragments using the technique of EF games extended with suitable counting moves. Finally, as our main result, we establish the decidability of $\mathsf{CTMTL}$ by giving an equisatisfiable reduction from $\mathsf{CTMTL}$ to $\mathsf{MTL}$. The reduction provides one more example of the use of temporal projections with oversampling introduced earlier for proving decidability. Our reduction also implies that $\mathsf{MITL}$ extended with $\mathsf{C}$ and $\mathsf{UT}$ modalities is elementarily decidable.