Handling of Past and Future with Phenesthe+

Manolis Pitsikalis
(University of Liverpool)
Alexei Lisitsa
(University of Liverpool)
Patrick Totzke
(University of Liverpool)

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.

In Antonis Achilleos and Dario Della Monica: Proceedings of the Fourteenth International Symposium on Games, Automata, Logics, and Formal Verification (GandALF 2023), Udine, Italy, 18-20th September 2023, Electronic Proceedings in Theoretical Computer Science 390, pp. 33–49.
Published: 30th September 2023.

ArXived at: https://dx.doi.org/10.4204/EPTCS.390.3 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org