Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

When Do You Start Counting? Revisiting Counting and Pnueli Modalities in Timed Logics

Hsi-Ming Ho, Khushraj Madnani

TL;DR

This paper investigates counting and Pnueli modalities in timed logics, focusing on expressing counts of events within arbitrary intervals and relating these to well-known fragments like EMITL and Q2MLO. It shows that counting modalities for $I=igl< a,b igr>$ can be expressed in $ extup{Q2MLO}^{ extsf{fut}}$ (and in unilateral EMITL) using automata modalities, and it reconciles conflicting prior results by extending techniques to unilateral intervals and rational constants. A key contribution is the correction of folklore, proving that $C_I^k$ for $I=igl< a,b igr>$ can be captured by $C_I^k$ with $I=[0,b angle$ in both pointwise and continuous semantics under certain conditions, with broader generalizations to $ ext{P}^2_I$ and FO formulas. The results advance understanding of expressiveness in timed logics, suggesting robust expressiveness of Q2MLO and highlighting avenues for further refinement and decidability results in MITL-like frameworks with counting and Pnueli modalities.

Abstract

Pnueli first noticed that certain simple 'counting' properties appear to be inexpressible in popular timed temporal logics such as Metric Interval Temporal Logic (MITL). This interesting observation has since been studied extensively, culminating in strong timed logics that are capable of expressing such properties yet remain decidable. A slightly more general case, namely where one asserts the existence of a sequence of events in an arbitrary interval of the form <a, b> (instead of an upper-bound interval of the form [0, b>, which starts from the current point in time), has however not been addressed satisfactorily in the existing literature. We show that counting in [0, b> is in fact as powerful as counting in <a, b>; moreover, the general property 'there exist x', x'' in I such that x' <= x'' and phi(x', x'') holds' can be expressed in Extended Metric Interval Temporal Logic (EMITL) with only [0, b>.

When Do You Start Counting? Revisiting Counting and Pnueli Modalities in Timed Logics

TL;DR

This paper investigates counting and Pnueli modalities in timed logics, focusing on expressing counts of events within arbitrary intervals and relating these to well-known fragments like EMITL and Q2MLO. It shows that counting modalities for can be expressed in (and in unilateral EMITL) using automata modalities, and it reconciles conflicting prior results by extending techniques to unilateral intervals and rational constants. A key contribution is the correction of folklore, proving that for can be captured by with in both pointwise and continuous semantics under certain conditions, with broader generalizations to and FO formulas. The results advance understanding of expressiveness in timed logics, suggesting robust expressiveness of Q2MLO and highlighting avenues for further refinement and decidability results in MITL-like frameworks with counting and Pnueli modalities.

Abstract

Pnueli first noticed that certain simple 'counting' properties appear to be inexpressible in popular timed temporal logics such as Metric Interval Temporal Logic (MITL). This interesting observation has since been studied extensively, culminating in strong timed logics that are capable of expressing such properties yet remain decidable. A slightly more general case, namely where one asserts the existence of a sequence of events in an arbitrary interval of the form <a, b> (instead of an upper-bound interval of the form [0, b>, which starts from the current point in time), has however not been addressed satisfactorily in the existing literature. We show that counting in [0, b> is in fact as powerful as counting in <a, b>; moreover, the general property 'there exist x', x'' in I such that x' <= x'' and phi(x', x'') holds' can be expressed in Extended Metric Interval Temporal Logic (EMITL) with only [0, b>.
Paper Structure (22 sections, 15 theorems, 19 equations, 6 figures)

This paper contains 22 sections, 15 theorems, 19 equations, 6 figures.

Table of Contents

  1. Introduction
  2. Timed logics.
  3. Specifying multiple events.
  4. Expressiveness.
  5. Contributions.
  6. Related work.
  7. Preliminaries
  8. Timed languages.
  9. Metric predicate logics.
  10. Metric temporal logics.
  11. Semantics.
  12. Expressiveness.
  13. Expressing counting modalities
  14. Counting events in arbitrary intervals.
  15. Counting events in $I$ by automata modalities.
  16. ...and 7 more sections

Key Result

Theorem 1

$\textup{\textmd{TLCI}}{}^\textsf{fut} \subseteq \text{aperiodic } \textup{\textmd{EMITL}}{}^\textsf{fut} \equiv \textup{\textmd{Q2MLO}}{}^\textsf{fut}$.

Figures (6)

  • Figure 1: Some timed temporal logics considered in this paper. Note that the definitions of TLC and TLP in Hirshfeld06 are less general but equally expressive in the continuous semantics.
  • Figure 2: The NFA$\mathcal{A}^{\mathop{\mathrm{\mathbin{\mathbf{U}}}}\nolimits}$ for $\varphi_1 \mathop{\mathrm{\mathbin{\mathbf{U}}}}\nolimits_I \varphi_2$.
  • Figure 3: The NFA$\mathcal{A}^{\mathop{\mathrm{\mathbf{C}}}\nolimits, 3}$ for $\mathop{\mathrm{\mathbf{C}}}\nolimits_I^{3} \varphi$.
  • Figure 4: Undesired scenario #1.
  • Figure 5: Desired scenario with $d(h_j, \ell_{j+1}) \geq 1$.
  • ...and 1 more figures

Theorems & Definitions (26)

  • Definition 1: $\textup{\textmd{TLCI}}{}^\textsf{fut}$ Rabinovich2010
  • Theorem 1
  • Theorem 2
  • Definition 2: $\textup{\textmd{TLPI}}{}^\textsf{fut}$ Rabinovich2010
  • Lemma 1
  • proof
  • Proposition 1
  • proof
  • Lemma 2
  • proof : Proof sketch.
  • ...and 16 more