skip to main content
10.1145/3178126.3178129acmconferencesArticle/Chapter ViewAbstractPublication PagescpsweekConference Proceedingsconference-collections
research-article

Specifying Timed Patterns using Temporal Logic

Published: 11 April 2018 Publication History

Abstract

Monitoring system behaviors using formal specifications appears to be an effective technique in analyzing cyber-physical systems. However, to achieve intended results in monitoring, specification languages need to be intuitive, elegant, and expressive at the first place. In this paper, we propose a metric extension of well-known Halpern-Shoham (hs) logic, called Metric Compass Logic (mcl), for monitoring purposes. Originally proposed for high-level temporal reasoning, the logic hs is very expressive and enables users to specify many temporal patterns in an intuitive and elegant way. As our main contribution, we present an offline monitoring technique for timed patterns specified in mcl. Our solution is built upon the framework developed for timed regular expressions (TRE) matching but explores a different (logical) direction. We finally study several practical features concerning atomic formulas and discuss a combined timed pattern speciication language with TRE.

References

[1]
James F Allen. Maintaining knowledge about temporal intervals. Communications of the ACM, 26(11):832--843, 1983.
[2]
Eugene Asarin, Paul Caspi, and Oded Maler. A Kleene theorem for timed automata. In Logic in Computer Science (LICS), pages 160--171, 1997.
[3]
Eugene Asarin, Paul Caspi, and Oded Maler. Timed regular expressions. Journal of ACM, 49(2):172--206, 2002.
[4]
Patrick Blackburn, Maarten De Rijke, and Yde Venema. Modal Logic, volume 53. Cambridge University Press, 2002.
[5]
Patrick Blackburn, Johan van Benthem, and Frank Wolter. Handbook of Modal Logic. Elsevier, 2006.
[6]
Marius Bozga, Susanne Graf, and Laurent Mounier If-2.0: A validation environment for component-based real-time systems. In Computer Aided Verification (CAV), pages 343--348. Springer, 2002.
[7]
Davide Bresolin, Dario Della Monica, Valentin Goranko, Angelo Montanari, and Guido Sciavicco. Metric propositional neighborhood logics: Expressiveness, decidability, and undecidability. In ECAI, volume 10, pages 695--700, 2010.
[8]
Zhou Chaochen, Charles Anthony Richard Hoare, and Anders P Ravn. A calculus of durations. Information processing letters, 40(5):269--276, 1991.
[9]
David L Dill. Timing assumptions and verification of finite-state concurrent systems. In International Conference on Computer Aided Verification, pages 197--212. Springer, 1989.
[10]
Dov Gabbay, Amir Pnueli, Saharon Shelah, and Jonathan Stavi. On the temporal analysis of fairness. In Proceedings of the 7th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 163--173. ACM, 1980.
[11]
Joseph Y Halpern and Yoav Shoham. A propositional modal logic of time intervals. Journal of the ACM (JACM), 38(4):935--962, 1991.
[12]
Klaus Havelund and Giles Reger. Runtime verification logics a language design perspective. In Models, Algorithms, Logics and Tools, pages 310--338. Springer, 2017.
[13]
Bjarni Jonnson and Alfred Tarski. Boolean algebras with operators. American Journal of Mathematics, 74(1):127--162, 1952.
[14]
Ron Koymans. Specifying real-time properties with metric temporal logic. Real-Time Systems, 2(4):255--299, 1990.
[15]
Martin Leucker and Christian Schallhart. A brief account of runtime verification. J. Log. Algebr. Program., 78(5):293--303, 2009.
[16]
Oded Maler. Some thoughts on runtime verification. In International Conference on Runtime Verifcation, pages 3--14, 2016.
[17]
Oded Maler and Dejan Nickovic. Monitoring temporal properties of continuous signals. In Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems, pages 152--166. Springer, 2004.
[18]
Angelo Montanari and Guido Sciavicco. A decidable logic for time intervals: Propositional neighborhood logic. In Proc. of the AAAI-2002 Workshop on Spatial and Temporal Reasoning, pages 27--34, 2002.
[19]
Ben Moszkowski. Executing temporal logic programs. In International Conference on Concurrency, pages 111--130. Springer, 1984.
[20]
Amir Pnueli. The temporal logic of programs. In Foundations of Computer Science, 1977., 18th Annual Symposium on, pages 46--57. IEEE, 1977.
[21]
Arthur N. Prior. Time and Modality. Clarendon Press Oxford, 1957.
[22]
Arthur N. Prior. Past, present and future. Clarendon Press Oxford, 1967.
[23]
Anders P Ravn. Design of embedded real-time computing systems. PhD thesis, Technical University of Denmark Lyngby, 1995.
[24]
Roni Rosner and Amir Pnueli. A choppy logic. Weizmann Institute of Science. Department of Applied Mathematics, 1986.
[25]
Dogan Ulus. Montre: A tool for monitoring timed regular expressions. In Computer Aided Verifcation (CAV), 2017.
[26]
Dogan Ulus, Thomas Ferrère, Eugene Asarin, and Oded Maler Timed pattern matching. In Formal Modeling and Analysis of Timed Systems (FORMATS), pages 222--236, 2014.
[27]
Dogan Ulus, Thomas Ferrère, Eugene Asarin, and Oded Maler. Online timed pattern matching using derivatives. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pages 736--751, 2016.
[28]
Yde Venema. Expressiveness and completeness of an interval tense logic. Notre Dame Journal of Formal Logic, 31(4):529--547, 1990.
[29]
Yde Venema. A modal logic for chopping intervals. Journal of Logic and Computation, 1(4):453--476, 1991.
[30]
Masaki Waga, Takumi Akazaki, and Ichiro Hasuo. A boyer-moore type algorithm for timed pattern matching. In International Conference on Formal Modeling and Analysis of Timed Systems, pages 121--139. Springer, 2016.
[31]
Masaki Waga, Ichiro Hasuo, and Kohei Suenaga. Efficient online timed pattern matching by automata-based skipping. In International Conference on Formal Modeling and Analysis of Timed Systems, pages 224--243. Springer, 2017.

Cited By

View all

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences
HSCC '18: Proceedings of the 21st International Conference on Hybrid Systems: Computation and Control (part of CPS Week)
April 2018
296 pages
ISBN:9781450356428
DOI:10.1145/3178126
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 11 April 2018

Permissions

Request permissions for this article.

Check for updates

Author Tags

  1. Formal methods
  2. Pattern matching
  3. Realtime and embedded systems
  4. Temporal logic

Qualifiers

  • Research-article
  • Research
  • Refereed limited

Conference

HSCC '18
Sponsor:

Acceptance Rates

Overall Acceptance Rate 153 of 373 submissions, 41%

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)7
  • Downloads (Last 6 weeks)0
Reflects downloads up to 02 Mar 2025

Other Metrics

Citations

Cited By

View all
  • (2024)Elements of Timed Pattern MatchingACM Transactions on Embedded Computing Systems10.1145/364511423:4(1-45)Online publication date: 10-Feb-2024
  • (2023)IntroductionChronicles: Formalization of a Temporal Model10.1007/978-3-031-33693-5_1(1-14)Online publication date: 2-May-2023
  • (2022)Model-bounded Monitoring of Hybrid SystemsACM Transactions on Cyber-Physical Systems10.1145/35290956:4(1-26)Online publication date: 25-Apr-2022
  • (2021)Monitoring First-Order Interval LogicSoftware Engineering and Formal Methods10.1007/978-3-030-92124-8_4(66-83)Online publication date: 3-Dec-2021
  • (2019)Symbolic Monitoring Against Specifications Parametric in Time and DataComputer Aided Verification10.1007/978-3-030-25540-4_30(520-539)Online publication date: 12-Jul-2019
  • (2018)Moore-Machine Filtering for Timed and Untimed Pattern MatchingIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems10.1109/TCAD.2018.285735837:11(2649-2660)Online publication date: Nov-2018

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media