research-article

Efficient Parametric Identification for STL

Authors:

Alexey Bakhirkin,

Thomas Ferrère,

Oded MalerAuthors Info & Claims

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

Pages 177 - 186

https://doi.org/10.1145/3178126.3178132

Published: 11 April 2018 Publication History

Abstract

We describe a new algorithm for the parametric identification problem for signal temporal logic (STL), stated as follows. Given a dense-time real-valued signal w and a parameterized temporal logic formula φ, compute the subset of the parameter space that renders the formula satisfied by the signal. Unlike previous solutions, which were based on search in the parameter space or quantifier elimination, our procedure works recursively on φ and computes the evolution over time of the set of valid parameter assignments. This procedure is similar to that of monitoring or computing the robustness of φ relative to w. Our implementation and experiments demonstrate that this approach can work well in practice.

References

[1]

Houssam Abbas and Georgios E. Fainekos. 2013. Computing descent direction of MTL robustness for non-linear systems. In American Control Conference. 4405--4410. http://ieeexplore.ieee.org/document/6580518/

[2]

Houssam Abbas, Bardh Hoxha, Georgios Fainekos, and Koichi Ueda. 2014. Robustness-guided temporal logic testing and verification for stochastic cyber-physical systems. In Cyber Technology in Automation, Control, and Intelligent Systems (CYBER), 2014 IEEE 4th Annual International Conference on. IEEE, 1--6.

[3]

Takumi Akazaki and Ichiro Hasuo. 2015. Time robustness in MTL and expressivity in hybrid system falsification. In CAV. Springer, 356--374.

[4]

Rajeev Alur and Thomas A Henzinger. 1994. A really temporal logic. Journal of the ACM (JACM) 41, 1 (1994), 181--203.

Digital Library

[5]

Yashwanth Annpureddy, Che Liu, Georgios E Fainekos, and Sriram Sankaranarayanan. 2011. S-TaLiRo: A Tool for Temporal Logic Falsification for Hybrid Systems. In TACAS, Vol. 6605. Springer, 254--257.

Digital Library

[6]

Eugene Asarin, Alexandre Donzé, Oded Maler, and Dejan Nickovic. 2011. Parametric identification of temporal properties. In Runtime Verification. Springer, 147--160.

Digital Library

[7]

Alexey Bakhirkin, Thomas Ferrère, Oded Maler, and Dogan Ulus. 2017. On the Quantitative Semantics of Regular Expressions over Real-Valued Signals. In International Conference on Formal Modeling and Analysis of Timed Systems. Springer, 189--206.

[8]

Ezio Bartocci, Luca Bortolussi, and Laura Nenzi. 2013. A temporal logic approach to modular design of synthetic biological circuits. In International Conference on Computational Methods in Systems Biology. Springer, 164--177.

Digital Library

[9]

Ezio Bartocci, Jyotirmoy Deshmukh, Alexandre Donzé, Georgios Fainekos, Oded Maler, Dejan Nickovic, and Sriram Sankaranarayanan. 2018. Specification-based Monitoring of Cyber-Physical Systems: A Survey on Theory, Tools and Applications. In The Handbook of Runtime Verification.

[10]

Giuseppe Bombara and Calin Belta. 2017. Signal Clustering Using Temporal Logics. Springer International Publishing, Cham, 121--137.

[11]

Giuseppe Bombara, Cristian-Ioan Vasile, Francisco Penedo, Hirotoshi Yasuoka, and Calin Belta. 2016. A Decision Tree Approach to Data Classification using Signal Temporal Logic. In HSCC. ACM, 1--10.

Digital Library

[12]

Lubos Brim, P Dluhoš, D Šafránek, and Tomas Vejpustek. 2014. STL*: Extending signal temporal logic with signal-value freezing operator. Information and Computation 236 (2014), 52--67.

Digital Library

[13]

Sara Bufo, Ezio Bartocci, Guido Sanguinetti, Massimo Borelli, Umberto Lucangelo, and Luca Bortolussi. 2014. Temporal Logic Based Monitoring of Assisted Ventilation in Intensive Care Patients. In Leveraging Applications of Formal Methods, Verification and Validation. Specialized Techniques and Applications - 6th International Symposium, ISoLA 2014, Imperial, Corfu, Greece, October 8-11, 2014, Proceedings, Part II. 391--403.

[14]

Fraser Cameron, Georgios E. Fainekos, David M. Maahs, and Sriram Sankaranarayanan. 2015. Towards a Verified Artificial Pancreas: Challenges and Solutions for Runtime Verification. In Runtime Verification - 6th International Conference, RV 2015 Vienna, Austria, September 22-25, 2015. Proceedings. 3--17.

[15]

Thao Dang, Tommaso Dreossi, and Carla Piazza. 2015. Parameter synthesis through temporal logic specifications. In International Symposium on Formal Methods. Springer, 213--230.

[16]

Alexandre Donzé. 2010. Breach, a toolbox for verification and parameter synthesis of hybrid systems. In CAV, Vol. 10. Springer, 167--170.

Digital Library

[17]

Alexandre Donzé, Eric Fanchon, Lucie Martine Gattepaille, Oded Maler, and Philippe Tracqui. 2011. Robustness analysis and behavior discrimination in enzymatic reaction networks. PloS one 6, 9 (2011), e24246.

[18]

Alexandre Donzé, Thomas Ferrere, and Oded Maler. 2013. Efficient robust monitoring for STL. In CAV. 264--279.

[19]

A. Donzé, B. Krogh, and A. Rajhans. 2009. Parameter synthesis for hybrid systems with an application to simulink models. In HSCC (LNCS). Springer-Verlag.

Digital Library

[20]

Alexandre DonzéandOdedMaler. 2010. RobustSatisfactionofTemporalLogic over Real-Valued Signals. In FORMATS. 92--106.

Digital Library

[21]

Georgios E. Fainekos and Georges J. Pappas. 2006. Robustness of Temporal Logic Specifications. In FATES/RV (LNCS), Vol. 4262. Springer, 178--192.

Digital Library

[22]

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

[23]

Samira S Farahani, Vasumathi Raman, and Richard M Murray. 2015. Robust model predictive control for signal temporal logic synthesis. IFAC-PapersOnLine 48, 27 (2015), 323--328.

[24]

Carlo Alberto Furia and Matteo Rossi. 2007. On the expressiveness of MTL variants over dense time. In International Conference on Formal Modeling and Analysis of Timed Systems. Springer, 163--178.

Digital Library

[25]

Bardh Hoxha, Adel Dokhanchi, and Georgios Fainekos. 2017. Mining parametric temporal logic properties in model-based design for cyber-physical systems. International Journal on Software Tools for Technology Transfer (2017), 1--15.

Digital Library

[26]

Susmit Jha, Ashish Tiwari, Sanjit A. Seshia, Tuhin Sahai, and Natarajan Shankar. 2017. TeLEx: Passive STL Learning Using Only Positive Examples. In Runtime Verification. 208--224.

[27]

Xiaoqing Jin, Alexandre Donzé, Jyotirmoy V. Deshmukh, and Sanjit A. Seshia. 2013. Mining Requirements from Closed-loop Control Models. In HSCC.

Digital Library

[28]

Kevin D Jones, Victor Konrad, and Dejan Nickovic. 2010. Analog property checkers: a DDR2 case study. Formal Methods in System Design 36, 2 (2010), 114--130.

Digital Library

[29]

Eric S Kim, Murat Arcak, and Sanjit A Seshia. 2016. Directed specifications and assumption mining for monotone dynamical systems. In Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control. ACM, 21--30.

Digital Library

[30]

Zhaodan Kong, Austin Jones, and Calin Belta. 2017. Temporal logics for learning and detection of anomalous behavior. IEEE Trans. Automat. Control 62, 3 (2017), 1210--1222.

[31]

Julien Legriel, Colas Le Guernic, Scott Cotton, and Oded Maler. 2010. Approximating the Pareto Front of Multi-criteria Optimization Problems. In TACAS (LNCS), Vol. 6015. Springer, 69--83.

Digital Library

[32]

D. Lemire. 2006. Streaming Maximum-Minimum Filter Using No More than Three Comparisons per Element. CoRR abs/cs/0610046 (2006).

Digital Library

[33]

Oded Maler and Dejan Nickovic. 2004. Monitoring Temporal Properties of Continuous Signals. In FORMATS/FTRTFT. 152--166.

[34]

Truong Nghiem, Sriram Sankaranarayanan, Georgios Fainekos, Franjo Ivancić, Aarti Gupta, and George J Pappas. 2010. Monte-carlo techniques for falsification of temporal properties of non-linear hybrid systems. In HSCC. ACM, 211--220.

Digital Library

[35]

Dejan Nickovic. 2008. Checking timed and hybrid properties: Theory and applications. Ph.D. Dissertation. Université Joseph Fourier, Grenoble, France.

[36]

Pierluigi Nuzzo, Huan Xu, Necmiye Ozay, John B Finn, Alberto L Sangiovanni-Vincentelli, Richard M Murray, Alexandre Donzé, and Sanjit A Seshia. 2014. A contract-based methodology for aircraft electric power system design. IEEE Access 2 (2014), 1--25.

[37]

Vasumathi Raman, Alexandre Donzé, Dorsa Sadigh, Richard M Murray, and Sanjit A Seshia. 2015. Reactive synthesis from signal temporal logic specifications. In Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control. ACM, 239--248.

Digital Library

[38]

Aurélien Rizk, Grégory Batt, François Fages, and Sylvain Soliman. 2008. On a continuous degree of satisfaction of temporal logic formulae with applications to systems biology. In CMSB. Springer, 251--268.

Digital Library

[39]

Simone Silvetti, Alberto Policriti, and Luca Bortolussi. 2017. An Active Learning Approach to the Falsification of Black Box Cyber-Physical Systems. arXiv preprint arXiv:1705.01879 (2017).

[40]

Szymon Stoma, Alexandre Donzé, François Bertaux, Oded Maler, and Gregory Batt. 2013. STL-based analysis of TRAIL-induced apoptosis challenges the notion of type I/type II cell line classification. PLoS computational biology 9, 5 (2013), e1003056.

[41]

Marcell Vazquez-Chanlatte, Jyotirmoy V. Deshmukh, Xiaoqing Jin, and Sanjit A. Seshia. 2017. Logical Clustering and Learning for Time-Series Data. SpringerInternational Publishing, Cham, 305--325.

[42]

Hengyi Yang, Bardh Hoxha, and Georgios E Fainekos. 2012. Querying Parametric Temporal Logic Properties on Embedded Systems. In ICTSS. Springer, 136--151.

Cited By

Liang KCardona GKamale DVasile C(2024)Learning Optimal Signal Temporal Logic Decision Trees for Classification: A Max-Flow MILP Formulation2024 IEEE 63rd Conference on Decision and Control (CDC)10.1109/CDC56724.2024.10886055(8332-8337)Online publication date: 16-Dec-2024
https://doi.org/10.1109/CDC56724.2024.10886055
Khandait TPedrielli G(2024)HyperPart-X: Probabilistic Guarantees for Parameter Mining of Signal Temporal Logic Formulas in Cyber-Physical SystemsRuntime Verification10.1007/978-3-031-74234-7_6(89-106)Online publication date: 14-Oct-2024
https://dl.acm.org/doi/10.1007/978-3-031-74234-7_6
Li DCai MVasile CTron R(2023)Learning Signal Temporal Logic through Neural Network for Interpretable Classification2023 American Control Conference (ACC)10.23919/ACC55779.2023.10156357(1907-1914)Online publication date: 31-May-2023
https://doi.org/10.23919/ACC55779.2023.10156357
Show More Cited By

Index Terms

Efficient Parametric Identification for STL
1. Computing methodologies
  1. Modeling and simulation
    1. Simulation evaluation
2. Theory of computation
  1. Logic
    1. Modal and temporal logics

Recommendations

Backpropagation for Parametric STL
2019 IEEE Intelligent Vehicles Symposium (IV)
This paper proposes a method to evaluate Signal Temporal Logic (STL) robustness formulas using computation graphs. This method results in efficient computations and enables the use of backpropagation for optimizing over STL parameters. Inferring STL ...
Parametric identification of temporal properties
RV'11: Proceedings of the Second international conference on Runtime verification

Given a dense-time real-valued signal and a parameterized temporal logic formula with <em>both</em> magnitude and timing parameters, we compute the subset of the parameter space that renders the formula satisfied by the trace. We provide two preliminary ...
STL*

To express temporal properties of dense-time real-valued signals, the Signal Temporal Logic (STL) has been defined by Maler et al. The work presented a monitoring algorithm deciding the satisfiability of STL formulae on finite discrete samples of ...

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

Qualifiers

Research-article
Research
Refereed limited

Funding Sources

Austrian Science Fund (FWF)
European Research Council

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

23
Total Citations
View Citations
205
Total Downloads

Downloads (Last 12 months)4
Downloads (Last 6 weeks)1

Reflects downloads up to 02 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Liang KCardona GKamale DVasile C(2024)Learning Optimal Signal Temporal Logic Decision Trees for Classification: A Max-Flow MILP Formulation2024 IEEE 63rd Conference on Decision and Control (CDC)10.1109/CDC56724.2024.10886055(8332-8337)Online publication date: 16-Dec-2024
https://doi.org/10.1109/CDC56724.2024.10886055
Khandait TPedrielli G(2024)HyperPart-X: Probabilistic Guarantees for Parameter Mining of Signal Temporal Logic Formulas in Cyber-Physical SystemsRuntime Verification10.1007/978-3-031-74234-7_6(89-106)Online publication date: 14-Oct-2024
https://dl.acm.org/doi/10.1007/978-3-031-74234-7_6
Li DCai MVasile CTron R(2023)Learning Signal Temporal Logic through Neural Network for Interpretable Classification2023 American Control Conference (ACC)10.23919/ACC55779.2023.10156357(1907-1914)Online publication date: 31-May-2023
https://doi.org/10.23919/ACC55779.2023.10156357
Mambakam AAsarin EBasset NDang T(2023)Pattern Matching and Parameter Identification for Parametric Timed Regular ExpressionsProceedings of the 26th ACM International Conference on Hybrid Systems: Computation and Control10.1145/3575870.3587115(1-13)Online publication date: 9-May-2023
https://dl.acm.org/doi/10.1145/3575870.3587115
Waga MAndré ÉHasuo I(2023)Parametric Timed Pattern MatchingACM Transactions on Software Engineering and Methodology10.1145/351719432:1(1-35)Online publication date: 13-Feb-2023
https://dl.acm.org/doi/10.1145/3517194
Mamouras KChattopadhyay AWang Z(2023)A compositional framework for algebraic quantitative online monitoring over continuous-time signalsInternational Journal on Software Tools for Technology Transfer (STTT)10.1007/s10009-023-00719-w25:4(557-573)Online publication date: 1-Aug-2023
https://dl.acm.org/doi/10.1007/s10009-023-00719-w
Aasi EVasile CBahreinian MBelta C(2022)Classification of Time-Series Data Using Boosted Decision Trees2022 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS)10.1109/IROS47612.2022.9982105(1263-1268)Online publication date: 23-Oct-2022
https://doi.org/10.1109/IROS47612.2022.9982105
Fisman DSaadon S(2022)Learning and Characterizing Fully-Ordered Lattice AutomataAutomated Technology for Verification and Analysis10.1007/978-3-031-19992-9_17(266-282)Online publication date: 21-Oct-2022
https://doi.org/10.1007/978-3-031-19992-9_17
Chen HLin SSmolka SPaoletti N(2022)An STL-Based Formulation of Resilience in Cyber-Physical SystemsFormal Modeling and Analysis of Timed Systems10.1007/978-3-031-15839-1_7(117-135)Online publication date: 29-Aug-2022
https://doi.org/10.1007/978-3-031-15839-1_7
Bruto da Costa ADasgupta P(2021)Learning Temporal Causal Sequence Relationships from Real-Time Time-SeriesJournal of Artificial Intelligence Research10.1613/jair.1.1239570(205-243)Online publication date: 1-May-2021
https://dl.acm.org/doi/10.1613/jair.1.12395
Show More Cited By

View Options

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

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Table of Conten