Metric temporal logic with counting

DOI10.1007/978-3-662-49630-5_20zbMATH Open1476.03018arXiv1512.09032OpenAlexW2213476453MaRDI QIDQ2811351FDOQ2811351

Shankara Narayanan Krishna, Khushraj Madnani, Paritosh K. Pandya

Publication date: 10 June 2016

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

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 ($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.

Full work available at URL: https://arxiv.org/abs/1512.09032

Recommendations

• Continuous time temporal logic with counting
• Deciding continuous-time metric temporal logic with counting modalities
• An Expressive Temporal Logic for Real Time
• Complexity of Metric Temporal Logics with Counting and the Pnueli Modalities
• scientific article; zbMATH DE number 7056237

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Temporal logic (03B44)

Cites Work

• An Expressive Temporal Logic for Real Time
• Complexity of metric temporal logics with counting and the Pnueli modalities
• Title not available (Why is that?)
• An until hierarchy and other applications of an Ehrenfeucht-Fraïssé game for temporal logic
• On the Expressiveness of MTL with Past Operators
• Metric Temporal Logic with Counting
• Title not available (Why is that?)
• On Expressive Powers of Timed Logics: Comparing Boundedness, Non-punctuality, and Deterministic Freezing
• On Construction of Safety Signal Automata for $MITL[\:\mathcal{U},\:\mathcal{S}]$ Using Temporal Projections

Cited In (7)

• Complexity of metric temporal logics with counting and the Pnueli modalities
• The compound interest in relaxing punctuality
• Title not available (Why is that?)
• Metric Temporal Logic with Counting
• Parametric Metric Interval Temporal Logic
• On Metric Temporal Łukasiewicz Logic
• Making Metric Temporal Logic Rational

This page was built for publication: Metric temporal logic with counting

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2811351)