# Metric Temporal Logic with Counting

arXiv: https://arxiv.org/abs/1512.09032 · HTML: https://mlsanity.com/paper/1512.09032/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 30 Dec 2015.

## Built on by (most cited first, 1 of 1)

- [Satisfiability Checking of Multi-Variable TPTL with Unilateral Intervals Is PSPACE-Complete](https://mlsanity.com/paper/2309.00386/) (2023)

## Abstract (arXiv)

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 (mathsfMTL) with two different counting modalities called mathsfC and mathsfUT (until with threshold), which enhance the expressive power of mathsfMTL in orthogonal fashion. We confine ourselves only to the future fragment of mathsfMTL interpreted in a pointwise manner over finite timed words. We provide a comprehensive study of the expressive power of logic mathsfCTMTL and its fragments using the technique of EF games extended with suitable counting moves. Finally, as our main result, we establish the decidability of mathsfCTMTL by giving an equisatisfiable reduction from mathsfCTMTL to mathsfMTL. The reduction provides one more example of the use of temporal projections with oversampling introduced earlier for proving decidability. Our reduction also implies that mathsfMITL extended with mathsfC and mathsfUT modalities is elementarily decidable.