Metric Temporal Logic with Counting
Khushraj Madnani, Shankara Narayanan Krishna, Paritosh Pandya

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 () with two different counting modalities called and (until with threshold), which enhance the expressive power of in orthogonal fashion. We confine ourselves only to the future fragment of interpreted in a pointwise manner over finite timed words. We provide a comprehensive study of the expressive power of logic and its fragments using the technique of EF games extended with suitable counting moves. Finally, as our main result, we establish the decidability of by giving an equisatisfiable reduction from to . The reduction provides one…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · Logic, programming, and type systems · Model-Driven Software Engineering Techniques
