research-article

Public Access

Parameter Invariant Monitoring for Signal Temporal Logic

Authors:

Insup LeeAuthors Info & Claims

HSCC '18: Proceedings of the 21st International Conference on Hybrid Systems: Computation and Control (part of CPS Week)

Pages 187 - 196

https://doi.org/10.1145/3178126.3178140

Published: 11 April 2018 Publication History

Abstract

Signal Temporal Logic (STL) is a prominent specification formalism for real-time systems, and monitoring these specifications, specially when (for different reasons such as learning) behavior of systems can change over time, is quite important. There are three main challenges in this area: (1) full observation of system state is not possible due to noise or nuisance parameters, (2) the whole execution is not available during the monitoring, and (3) computational complexity of monitoring continuous time signals is very high. Although, each of these challenges has been addressed by different works, to the best of our knowledge, no one has addressed them all together. In this paper, we show how to extend any parameter invariant test procedure for single points in time to a parameter invariant test procedure for efficiently monitoring continuous time executions of a system against STL properties. We also show, how to extend probabilistic error guarantee of the input test procedure to a probabilistic error guarantee for the constructed test procedure.

References

[1]

Rajeev Alur, Tomás Feder, and Thomas A. Henzinger. 1996. The Benefits of Relaxing Punctuality. J. ACM 43, 1 (1996), 116--146.

Digital Library

[2]

Andreas Bauer. 2010. Monitorability of omega-regular languages. CoRR abs/1006.3638 (2010). http://arxiv.org/abs/1006.3638

[3]

Andreas Bauer and Yliès Falcone. 2016. Decentralised LTL monitoring. Formal Methods in System Design 48, 1 (2016), 46--93.

Digital Library

[4]

Sanjian Chen, Matthew O'Kelly, James Weimer, Oleg Sokolsky, and Insup Lee. 2015. An Intraoperative Glucose Control Benchmark for Formal Verification. IFAC-PapersOnLine 48, 27 (2015), 211--217.

[5]

Marcelo d'Amorim and Grigore Roşu. 2005. Efficient Monitoring of ω-Languages. 364--378.

Digital Library

[6]

Jyotirmoy V. Deshmukh, Alexandre Donzé, Shromona Ghosh, XiaoqingJin, Garvit Juniwal, and Sanjit A. Seshia. 2015. Robust Online Monitoring of Signal Temporal Logic. 55--70.

[7]

Adel Dokhanchi, Bardh Hoxha, and Georgios Fainekos. 2014. On-Line Monitoring for Temporal Logic Robustness. 231--246.

[8]

Alexandre Donzé, Thomas Ferrère, and Oded Maler. 2013. Efficient Robust Monitoring for STL. 264--279.

[9]

Georgios E. Fainekos and George J. Pappas. 2007. Robust Sampling for MITL Specifications. Berlin, Heidelberg, 147--162.

Digital Library

[10]

Georgios E. Fainekos and George J. Pappas. 2009. Robustness of temporal logic specifications for continuous-time signals. Theoretical Computer Science 410, 42 (2009), 4262 - 4291.

Digital Library

[11]

Kalpana Gondi, Yogeshkumar Patel, and A. Prasad Sistla. 2009. Monitoring the Full Range of ω-Regular Properties of Stochastic Systems. 105--119.

Digital Library

[12]

Hsi-Ming Ho, Joël Ouaknine, and James Worrell. 2014. Online Monitoring of Metric Temporal Logic. In Runtime Verification. 178--192.

[13]

Jinfeng Huang, Jeroen Voeten, and Marc Geilen. 2003. Real-time Property Preservation in Approximations of Timed Systems. In MEMOCODE. Washington, DC, USA, 163--171.

Digital Library

[14]

R. Ivanov, J. Weimer, A. F. Simpao, M. A. Rehman, and I. Lee. 2016. Prediction of Critical Pulmonary Shunts in Infants. IEEE Transactions on Control Systems Technology 24, 6 (2016), 1936--1952.

[15]

Ron Koymans. 1990. Specifying real-time properties with metric temporal logic. Real-Time Systems 2, 4 (1990), 255--299.

Digital Library

[16]

Oded Maler and Dejan Nickovic. {n. d.}. Monitoring Temporal Properties of Continuous Signals.

[17]

Joël Ouaknine and James Worrell. 2008. Some Recent Results in Metric Temporal Logic. In FORMATS. 1--13.

Digital Library

[18]

Amir Pnueli. 1977. The Temporal Logic of Programs. In SFCS. 46--57.

Digital Library

[19]

Nima Roohi and Mahesh Viswanathan. 2018. Revisiting MITL to Fix Decision Procedures. In VMCAI. Springer International Publishing, 474--494.

[20]

Dorsa Sadigh and Ashish Kapoor. 2015. Safe Control under Uncertainty. CoRR abs/1510.07313 (2015).

[21]

Sadahiro Saeki. 1996. A Proof of the Existence of Infinite Product Probability Measures. (1996).

[22]

Prasanna Thati and Grigore RoÅ§u. 2005. Monitoring Algorithms for Metric Temporal Logic Specifications. Electronic Notes in Theoretical Computer Science 113 (2005), 145--162. Proceedings of the Fourth Workshop on Runtime Verification (RV 2004).

[23]

Yu Wang, Nima Roohi, MatthewWest, Mahesh Viswanathan, and Geir E. Dullerud. 2015. Statistical Verification of Dynamical Systems Using Set Oriented Methods. In HSCC. 169--178.

Digital Library

[24]

Y. Wang, N. Roohi, M. West, M. Viswanathan, and G. E. Dullerud. 2016. Verifying Continuous-time Stochastic Hybrid Systems via Mori-Zwanzig model reduction. In IEEE CDC. 3012--3017.

[25]

James Weimer, Sanjian Chen, Amy Peleckis, Michael R. Rickels, and Insup Lee. 2016. Physiology-Invariant Meal Detection for Type 1 Diabetes. Diabetes Technology & Therapeutics 18, 10 (2016), 616--624.

[26]

J. Weimer, R. Ivanov, S. Chen, A. Roederer, O. Sokolsky, and I. Lee. 2017. Parameter-Invariant Monitor Design for Cyber Physical Systems. Proc. IEEE PP, 99 (2017), 1--22.

Cited By

Yu GLee JBae K(2022)STLmc: Robust STL Model Checking of Hybrid Systems Using SMTComputer Aided Verification10.1007/978-3-031-13185-1_26(524-537)Online publication date: 7-Aug-2022
https://doi.org/10.1007/978-3-031-13185-1_26
Zhong BJordan CProvost J(2021)Extending Signal Temporal Logic with Quantitative Semantics by Intervals for Robust Monitoring of Cyber-physical SystemsACM Transactions on Cyber-Physical Systems10.1145/33778685:2(1-25)Online publication date: 4-Jan-2021
https://dl.acm.org/doi/10.1145/3377868
Lee JYu GBae K(2021)Efficient SMT-Based Model Checking for Signal Temporal Logic2021 36th IEEE/ACM International Conference on Automated Software Engineering (ASE)10.1109/ASE51524.2021.9678719(343-354)Online publication date: Nov-2021
https://doi.org/10.1109/ASE51524.2021.9678719
Show More Cited By

Index Terms

Parameter Invariant Monitoring for Signal Temporal Logic
1. Mathematics of computing
  1. Probability and statistics
    1. Probabilistic algorithms
2. Theory of computation
  1. Models of computation
    1. Probabilistic computation
    2. Timed and hybrid models

Recommendations

Extending Signal Temporal Logic with Quantitative Semantics by Intervals for Robust Monitoring of Cyber-physical Systems
Special Issue on Time for CPS and Regular Papers

Monitoring is the core procedure of runtime verification of cyber-physical systems (CPS) and provides an evaluation of a signal with respect to a given specification. For formally specifying requirements with time constraints for CPS, Signal Temporal ...
Monitoring Algorithms for Metric Temporal Logic Specifications

Program execution traces can be so large in practical testing and monitoring applications that it would be very expensive, if not impossible, to store them for detailed analysis. Monitoring execution traces without storing them, can be a nontrivial ...
Monitoring business constraints with linear temporal logic: an approach based on colored automata
BPM'11: Proceedings of the 9th international conference on Business process management

Today's information systems record real-time information about business processes. This enables the monitoring of business constraints at runtime. In this paper, we present a novel runtime verification framework based on linear temporal logic and ...

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

Copyright © 2018 ACM.

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

SIGBED: ACM Special Interest Group on Embedded Systems

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 11 April 2018

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed limited

Funding Sources

NSF
ONR

Conference

HSCC '18

Sponsor:

SIGBED

HSCC '18: 21st International Conference on Hybrid Systems: Computation and Control

April 11 - 13, 2018

Porto, Portugal

Acceptance Rates

Overall Acceptance Rate 153 of 373 submissions, 41%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

8
Total Citations
View Citations
339
Total Downloads

Downloads (Last 12 months)56
Downloads (Last 6 weeks)7

Reflects downloads up to 02 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Yu GLee JBae K(2022)STLmc: Robust STL Model Checking of Hybrid Systems Using SMTComputer Aided Verification10.1007/978-3-031-13185-1_26(524-537)Online publication date: 7-Aug-2022
https://doi.org/10.1007/978-3-031-13185-1_26
Zhong BJordan CProvost J(2021)Extending Signal Temporal Logic with Quantitative Semantics by Intervals for Robust Monitoring of Cyber-physical SystemsACM Transactions on Cyber-Physical Systems10.1145/33778685:2(1-25)Online publication date: 4-Jan-2021
https://dl.acm.org/doi/10.1145/3377868
Lee JYu GBae K(2021)Efficient SMT-Based Model Checking for Signal Temporal Logic2021 36th IEEE/ACM International Conference on Automated Software Engineering (ASE)10.1109/ASE51524.2021.9678719(343-354)Online publication date: Nov-2021
https://doi.org/10.1109/ASE51524.2021.9678719
Wu MWang JDeshmukh JWang C(2019)Shield Synthesis for Real: Enforcing Safety in Cyber-Physical Systems2019 Formal Methods in Computer Aided Design (FMCAD)10.23919/FMCAD.2019.8894264(129-137)Online publication date: Oct-2019
https://doi.org/10.23919/FMCAD.2019.8894264
Abbas HPant YMangharam ROzay NPrabhakar P(2019)Temporal logic robustness for general signal classesProceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control10.1145/3302504.3311817(45-56)Online publication date: 16-Apr-2019
https://dl.acm.org/doi/10.1145/3302504.3311817
Bae KLee J(2019)Bounded model checking of signal temporal logic properties using syntactic separationProceedings of the ACM on Programming Languages10.1145/32903643:POPL(1-30)Online publication date: 2-Jan-2019
https://dl.acm.org/doi/10.1145/3290364
Kannan SKim MLee ISokolsky OViswanathan M(2019)A Retrospective Look at the Monitoring and Checking (MaC) FrameworkRuntime Verification10.1007/978-3-030-32079-9_1(1-14)Online publication date: 1-Oct-2019
https://doi.org/10.1007/978-3-030-32079-9_1
Liu LXie GLi R(2018)Synchronization Stability Analysis of Medical Cyber-Physical Cloud System Considering Multi-Closed-LoopsJournal of Circuits, Systems and Computers10.1142/S0218126619501986(1950198)Online publication date: 14-Nov-2018
https://doi.org/10.1142/S0218126619501986

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Figures

Tables

Media

View Table of Conten