Metric temporal logic with counting

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 (MTL) with two different counting modalities called C and UT (until with threshold), which enhance the expressive power of MTL in orthogonal fashion. We confine ourselves only to the future fragment of MTL interpreted in a pointwise manner over finite timed words. We provide a comprehensive study of the expressive power of logic 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 CTMTL by giving an equisatisfiable reduction from CTMTL to 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 MITL extended with C and UT modalities is elementarily decidable.