Metric temporal logic with counting

DOI10.1007/978-3-662-49630-5_20MaRDI QIDQ2811351zbMATH OpenOpenAlexFDO

Authors 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)

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

Mathematics Subject Classification ID

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

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.

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

Cites work

• scientific article; zbMATH DE number 618821 (Why is no real title available?)
• An Expressive Temporal Logic for Real Time
• An until hierarchy and other applications of an Ehrenfeucht-Fraïssé game for temporal logic
• Complexity of metric temporal logics with counting and the Pnueli modalities
• Metric temporal logic with counting
• On construction of safety signal automata for \(\mathrm{MITL}[\mathcal{U},\mathcal{S}]\) using temporal projections
• On expressive powers of timed logics: comparing boundedness, non-punctuality, and deterministic freezing
• On the Expressiveness of MTL with Past Operators
• When is metric temporal logic expressively complete?

Cited in

(8)

• Complexity of metric temporal logics with counting and the Pnueli modalities
• The compound interest in relaxing punctuality
• Metric temporal logic with counting
• Deciding continuous-time metric temporal logic with counting modalities
• Parametric Metric Interval Temporal Logic
• Logics meet 1-clock alternating timed automata
• 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)