Handling of Past and Future with Phenesthe+

Writing temporal logic formulae for properties that combine instantaneous events with overlapping temporal phenomena of some duration is difficult in classical temporal logics. To address this issue, in previous work we introduced a new temporal logic with intuitive temporal modalities specifically tailored for the representation of both instantaneous and durative phenomena. We also provided an implementation of a complex event processing system, Phenesthe, based on this logic, that has been applied and tested on a real maritime surveillance scenario. In this work, we extend our temporal logic with two extra modalities to increase its expressive power for handling future formulae. We compare the expressive power of different fragments of our logic with Linear Temporal Logic and dyadic first-order logic. Furthermore, we define correctness criteria for stream processors that use our language. Last but not least, we evaluate empirically the performance of Phenesthe+, our extended implementation, and show that the increased expressive power does not affect efficiency significantly.

• Publication year

  2023

• Venue

  International Symposium on Games, Automata, Logics and Formal Verification

• Publication date

  2023-09-30

• Fields of study

  Computer Science

• Identifiers
  DOI 10.4204/EPTCS.390.3arXiv 2310.00997
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• Making Sense of Heterogeneous Maritime Data

  2022cited by this paper
• Representation and Processing of Instantaneous and Durative Temporal Phenomena

  2021influential reference
• Adventures in monitorability: from branching to linear time and back again

  2019influential reference
• Heterogeneous integrated dataset for Maritime Intelligence, surveillance, and reconnaissance

  2019cited by this paper
• Algebraic Operators for Processing Sets of Temporal Intervals in Relational Databases

  2018cited by this paper
• Lectures on Runtime Verification: Introductory and Advanced Topics

  2018cited by this paper
• From LTL to rLTL monitoring: improved monitorability through robust semantics

  2018cited by this paper
• LARS: A Logic-based framework for Analytic Reasoning over Streams

  2018cited by this paper
• Team Semantics for the Specification and Verification of Hyperproperties

  2017cited by this paper
• Interval vs. Point Temporal Logic Model Checking

  2017cited by this paper
• An Event Calculus for Event Recognition

  2015cited by this paper
• A Proof of Kamp's theorem

  2014cited by this paper
• Temporal Logics for Hyperproperties

  2013cited by this paper
• Runtime Verification for LTL and TLTL

  2011influential reference
• TESLA: a formally defined event specification language

  2010cited by this paper
• A Rule-Based Language for Complex Event Processing and Reasoning

  2010cited by this paper
• Decidable and Undecidable Fragments of Halpern and Shoham's Interval Temporal Logic: Towards a Complete Classification

  2008cited by this paper
• Modern temporal logic: The philosophical background

  2006cited by this paper
• LOLA: runtime monitoring of synchronous systems

  2005influential reference
• Sharpening the Undecidability of Interval Temporal Logic

  2000cited by this paper
• Point-versus interval-based temporal data models

  1998cited by this paper
• A propositional modal logic of time intervals

  1991cited by this paper
• Expressiveness and Completeness of an Interval Tense Logic

  1990cited by this paper
• A logic-based calculus of events

  1989cited by this paper
• Temporal Logic of Programs

  1987cited by this paper
• Maintaining knowledge about temporal intervals

  1983cited by this paper
• On the temporal analysis of fairness

  1980cited by this paper
• Tense logic and the theory of linear order

  1968cited by this paper

• No citing papers are available for this paper.