Metric Temporal Logic with Counting

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.