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

TL;DR

This paper investigates the expressiveness of counting properties in timed logics, showing that counting over arbitrary intervals can be expressed within existing decidable logics, extending previous understanding of their capabilities.

Contribution

It demonstrates that counting in arbitrary intervals is as expressive as in bounded intervals within EMITL, addressing a gap in the literature.

Findings

Counting in [0, b> is as powerful as in <a, b> intervals.

The property of existence of event pairs satisfying certain conditions can be expressed in EMITL.

Extended Metric Interval Temporal Logic can express more complex counting properties than previously known.

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