research-article

Probabilistic Temporal Logic Falsification of Cyber-Physical Systems

Authors:

Georgios Fainekos,

Sriram Sankaranarayanan,

Franjo Ivančić, and

Aarti GuptaAuthors Info & Claims

ACM Transactions on Embedded Computing Systems (TECS), Volume 12, Issue 2s

Article No.: 95, Pages 1 - 30

https://doi.org/10.1145/2465787.2465797

Published: 01 May 2013 Publication History

Abstract

We present a Monte-Carlo optimization technique for finding system behaviors that falsify a metric temporal logic (MTL) property. Our approach performs a random walk over the space of system inputs guided by a robustness metric defined by the MTL property. Robustness is guiding the search for a falsifying behavior by exploring trajectories with smaller robustness values. The resulting testing framework can be applied to a wide class of cyber-physical systems (CPS). We show through experiments on complex system models that using our framework can help automatically falsify properties with more consistency as compared to other means, such as uniform sampling.

References

[1]

Abbas, H. and Fainekos, G. 2011a. Linear hybrid system falsification through descent. Tech. rep. arXiv:1105.1733.

[2]

Abbas, H. and Fainekos, G. 2011b. Linear hybrid system falsification through local search. In Automated Technology for Verification and Analysis. Lecture Notes in Computer Science, vol. 6996. Springer, 503--510.

Digital Library

[3]

Alur, R., Dang, T., and Ivančić, F. 2003. Progress on reachability analysis of hybrid systems using predicate abstraction. In Hybrid Systems: Computation and Control. Lecture Notes in Computer Science, vol. 2623. Springer, 4--19.

Digital Library

[4]

Alur, R., Henzinger, T. A., Lafferriere, G., and Pappas, G. J. 2000. Discrete abstractions of hybrid systems. Proc. IEEE 88, 2, 971--984.

[5]

Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T. A., Ho, P.-H., Nicollin, X., Olivero, A., Sifakis, J., and Yovine, S. 1995. The algorithmic analysis of hybrid systems. Theor. Comput. Sci. 138, 1, 3--34.

Digital Library

[6]

Alur, R., Dang, T., Esposito, J., Hur, Y., Ivancic, F., Kumar, V., Lee, I., Mishra, P., Pappas, G. J., and Sokolsky, O. 2003. Hierarchical modeling and analysis of embedded systems. Proc. IEEE 91, 1, 11--28.

[7]

Andrieu, C., Freitas, N. D., Doucet, A., and Jordan, M. I. 2003. An introduction to MCMC for machine learning. Machine Learn. 50, 5--43.

[8]

Annapureddy, Y. S. R., Liu, C., Fainekos, G. E., and Sankaranarayanan, S. 2011. S-taliro: A tool for temporal logic falsification for hybrid systems. In Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, vol. 6605. Springer, 254--257.

Digital Library

[9]

Bandemer, H. and Gottwald, S. 1995. Fuzzy Sets, Fuzzy Logic, Fuzzy Methods, with Applications. Wiley, New York, NY.

[10]

Bhatia, A. and Frazzoli, E. 2004. Incremental search methods for reachability analysis of continuous and hybrid systems. In Proceedings of HSCC. Lecture Notes in Computer Science, vol. 2993. Springer, 142--156.

[11]

Boyd, S. and Vandenberghe, S. 2004. Convex Optimization. Cambridge University Press. http://www.stanford.edu/ boyd/cvxbook.html.

Digital Library

[12]

Branicky, M., Curtiss, M., Levine, J., and Morgan, S. 2006. Sampling-based planning, control and verification of hybrid systems. IEE Control Theory Appl. 153, 5, 575--590.

[13]

Chib, S. and Greenberg, E. 1995. Understanding the Metropolis-Hastings algorithm. Amer. Statistician 49, 4, 327--335.

[14]

Clarke, E., Donze, A., and Legay, A. 2009. Statistical model checking of analog mixed-signal circuits with an application to a third order Δ − σ modulator. In Hardware and Software: Verification and Testing. Lecture Notes in Computer Science, vol. 5394/2009. 149--163.

Digital Library

[15]

Cormen, T. H., Leiserson, C. E., Rivest, R. L., and Stein, C. 2001. Introduction to Algorithms 2nd Ed. MIT Press/McGraw-Hill.

Digital Library

[16]

Dang, T., Donzé, A., and Maler, O. 2004. Verification of analog and mixed-signal circuits using hybrid system techniques. In Proceedings of the 5th International Conference on Formal Methods in Computer-Aided Design. Lecture Notes in Computer Science, vol. 3312. Springer, 21--36.

[17]

Dang, T., Donze, A., Maler, O., and Shalev, N. 2008. Sensitive state-space exploration. In Proceedings of the 47th IEEE CDC. 4049--4054.

[18]

de Alfaro, L., Faella, M., and Stoelinga, M. 2004. Linear and branching metrics for quantitative transition systems. In Proceedings of the 31st ICALP. Lecture Notes in Computer Science, vol. 3142. Springer, 97--109.

[19]

Donzé, A. and Maler, O. 2007. Systematic simulation using sensitivity analysis. In Proceeding of HSCC. Lecture Notes in Computer Science, vol. 4416. Springer, 174--189.

Digital Library

[20]

Egerstedt, M. and Martin, C. 2009. Control Theoretic Splines: Optimal Control, Statistics, and Path Planning. Princeton University Press, Princeton, NJ.

[21]

Esposito, J. M. and Kumar, V. 2004. An asynchronous integration and event detection algorithm for simulating multi-agent hybrid systems. ACM Trans. Model. Comput. Simul. 14, 4, 363--388.

Digital Library

[22]

Esposito, J. M., Kim, J., and Kumar, V. 2004. Adaptive RRTs for validating hybrid robotic control systems. In Proceedings of the International Workshop on the Algorithmic Foundations of Robotics.

[23]

Esterel Technologies. 2011. Scade success stories. http://www.esterel-technologies.com/technology/success-stories/.

[24]

Fainekos, G. E. and Pappas, G. J. 2006. Robustness of temporal logic specifications for finite state sequences in metric spaces. Tech. rep. MS-CIS-06-05, Dept. of CIS, Univ. of Pennsylvania.

[25]

Fainekos, G. E. and Pappas, G. J. 2009. Robustness of temporal logic specifications for continuous-time signals. Theor. Comput. Sci. 410, 42, 4262--4291.

Digital Library

[26]

Fainekos, G. E., Girard, A., and Pappas, G. J. 2006. Temporal logic verification using simulation. In Proceedings of FORMATS. Lecture Notes in Computer Science, vol. 4202. Springer, 171--186.

Digital Library

[27]

Fainekos, G. E., Sankaranarayanan, S., Ivančić, F., and Gupta, A. 2009. Robustness of model-based simulations. In Proceedings of the IEEE Real-Time Systems Symposium. 345--354.

Digital Library

[28]

Fehnker, A. and Ivančić, F. 2004. Benchmarks for hybrid systems verification. In Proceedings of HSCC. Lecture Notes in Computer Science, vol. 2993. Springer, 326--341.

[29]

Frehse, G., Guernic, C. L., Donz, A., Cotton, S., Ray, R., Lebeltel, O., Ripado, R., Girard, A., Dang, T., and Maler, O. 2011. Spaceex: Scalable verification of hybrid systems. In Proceedings of the 23rd CAV.

Digital Library

[30]

Frenkel, D. and Smit, B. 1996. Understanding Molecular Simulation: From Algorithms to Applications. Academic Press, Walthan, MA.

Digital Library

[31]

Girard, A. and Pappas, G. J. 2006. Verification using simulation. In Proceedings of HSCC. Lecture Notes in Computer Science, vol. 3927. Springer, 272--286.

Digital Library

[32]

Grosu, R. and Smolka, S. 2005. Monte carlo model checking. In Proceedings of TACAS. Lecture Notes in Computer Science, vol. 3440. Springer, 271--286.

Digital Library

[33]

Henzinger, T. A. 1996. The theory of hybrid automata. In Proceedings of LICS. 278--292.

Digital Library

[34]

Henzinger, T. A., Kopke, P. W., Puri, A., and Varaiya, P. 1998. What’s decidable about hybrid automata? J. Comput. Syst. Sci. 57, 1, 94--124.

Digital Library

[35]

Julius, A. A., Fainekos, G. E., Anand, M., Lee, I., and Pappas, G. J. 2007. Robust test generation and coverage for hybrid systems. In Proceedings of HSCC. Lecture Notes in Computer Science, vol. 4416. Springer, 329--342.

Digital Library

[36]

Kapinski, J., Krogh, B. H., Maler, O., and Stursberg, O. 2003. On systematic simulation of open continuous systems. In Proceedings of HSCC. Lecture Notes in Computer Science, vol. 2623. Springer, 283--297.

Digital Library

[37]

Kopperman, R. 1988. All topologies come from generalized metrics. Amer. Math. Month. 95, 89--97.

Digital Library

[38]

Koymans, R. 1990. Specifying real-time properties with metric temporal logic. Real-Time Syst. 2, 4, 255--299.

Digital Library

[39]

Lamine, K. B. and Kabanza, F. 2000. Using fuzzy temporal logic for monitoring behavior-based mobile robots. In Proceedings of the IASTED International Conference Robotics and Applications, M. Hamza Ed., 116--122.

[40]

Lee, E. A. and Varaiya, P. 2003. Structure and Interpretation of Signals and Systems. Addison Wesley, Reading, MA.

[41]

Lerda, F., Kapinski, J., Clarke, E. M., and Krogh, B. H. 2008. Verification of supervisory control software using state proximity and merging. In Proceedings of HSCC. Lecture Notes in Computer Science, vol. 4981. Springer, 344--357.

Digital Library

[42]

Lovasz, L. and Vempala, S. 2003. Hit-and-run is fast and fun. Tech rep. MSR-TR-2003.05. http://www-math.mit.edu/ vempala/papers/logcon-hitrun.ps.

[43]

Lovasz, L. and Vempala, S. 2006. Hit-and-run from a corner. SIAM J. Comput. 35, 4, 985--1005.

Digital Library

[44]

Lygeros, J., Johansson, K. H., Simic, S. N., Zhang, J., and Sastry, S. 2003. Dynamical properties of hybrid automata. IEEE Trans. Autom. Control 48, 2--17.

[45]

Mathworks. 2011. Simulink user stories. http://www.mathworks.com/products/simulink/userstories.html.

[46]

Nahhal, T. and Dang, T. 2007. Test coverage for continuous and hybrid systems. In Proceedings of CAV. Lecture Notes in Computer Science, vol. 4590. Springer, 449--462.

Digital Library

[47]

Nghiem, T., Sankaranarayanan, S., Fainekos, G. E., Ivancic, F., Gupta, A., and Pappas, G. J. 2010. Monte-carlo techniques for falsification of temporal properties of non-linear hybrid systems. In Proceedings of the 13th ACM International Conference on Hybrid Systems: Computation and Control. 211--220.

Digital Library

[48]

Plaku, E., Kavraki, L. E., and Vardi, M. Y. 2007. Hybrid systems: From verification to falsification. In Proceedings of CAV. Lecture Notes in Computer Science, vol. 4590. Springer, 463--476.

Digital Library

[49]

Plaku, E., Kavraki, L. E., and Vardi, M. Y. 2009. Falsification of ltl safety properties in hybrid systems. In Proceedings of TACAS. Lecture Notes in Computer Science, vol. 5505. Springer, 368--382.

Digital Library

[50]

Press, W. H., Flannery, B. P., Teukolsky, S. A., and Vetterling, W. T. 1992. Numerical Recipes: The Art of Scientific Computing 2nd Ed. Cambridge University Press.

Digital Library

[51]

Randall, D. 2006. Rapidly mixing markov chains with applications in computer science and physics. Comput. Sci. Eng. 8, 2.

Digital Library

[52]

Rizk, A., Batt, G., Fages, F., and Soliman, S. 2008. On a continuous degree of satisfaction of temporal logic formulae with applications to systems biology. In Proceeding of the 6th International Conference on Computational Methods in Systems Biology. Lecture Notes in Computer Science, vol. 5307. Springer, 251--268.

Digital Library

[53]

Romeijn, H. and Smith, R. 1994. Simulated annealing for constrained global optimization. J. Global Optim. 5, 101--126.

[54]

Rubinstein, R. Y. and Kroese, D. P. 2008. Simulation and the Monte Carlo Method. Wiley Series in Probability and Mathematical Statistics.

Digital Library

[55]

Sanfelice, R. G. and Teel, A. R. 2010. Dynamical properties of hybrid systems simulators. Automatica 46, 2, 239--248.

Digital Library

[56]

Sankaranarayanan, S., Chang, R. M., Jiang, G., and Ivancic, F. 2007. State space exploration using feedback constraint generation and monte-carlo sampling. In Proceedings of ESEC/SIGSOFT FSE. 321--330.

Digital Library

[57]

Seda, A. K. and Hitzler, P. 2008. Generalized distance functions in the theory of computation. Comput. J. 53, 4.

Digital Library

[58]

Smith, R. 1984. Monte Carlo procedures for generating points uniformly distributed over bounded regions. Oper. Res. 38, 3, 1296--1308.

Digital Library

[59]

Smith, R. L. 1996. The hit-and-run sampler: A globally reaching markov chain sampler for generating arbitrary multivariate distributions. In Proceedings of the 28th Conference on Winter Simulation. 260--264.

Digital Library

[60]

Sontag, E. D. 1998. Mathematical Control Theory: Deterministic Finite Dimensional Systems 2nd Ed. Springer.

Digital Library

[61]

Tripakis, S. and Dang, T. 2009. Model-Based Design for Embedded Systems. CRC Press, 383--436.

Digital Library

[62]

Younes, H. L. S. and Simmons, R. G. 2006. Statistical probabilitistic model checking with a focus on time-bounded properties. Inform. Comput. 204, 9, 1368--1409.

Digital Library

[63]

Zabinsky, A., Smith, R., MacDonald, J., Romeijn, H., and Kaufman, D. 1993. Improving hit-and-run for global optimization. J. Global Optim. 3, 171--192.

[64]

Zhao, Q., Krogh, B. H., and Hubbard, P. 2003. Generating test inputs for embedded control systems. IEEE Control Syst. Mag. Aug., 49--57.

Cited By

Abou-Mrad CAbbas H(2024)Approximating the Geometry of Temporal Logic FormulasProceedings of the 27th ACM International Conference on Hybrid Systems: Computation and Control10.1145/3641513.3650139(1-10)Online publication date: 14-May-2024
https://dl.acm.org/doi/10.1145/3641513.3650139
Biewer SBaum KSterz SHermanns HHetmank SLanger MLauber-Rönsberg ALehr F(2024)Software doping analysis for human oversightFormal Methods in System Design10.1007/s10703-024-00445-2Online publication date: 4-Apr-2024
https://doi.org/10.1007/s10703-024-00445-2
Iyer RKalbarczyk ZNakka N(2024)Classical Dependability Techniques and Modern Computing SystemsDependable Computing10.1002/9781119743453.ch2(25-56)Online publication date: 26-Apr-2024
https://doi.org/10.1002/9781119743453.ch2
Show More Cited By

Index Terms

Probabilistic Temporal Logic Falsification of Cyber-Physical Systems
1. Mathematics of computing
  1. Probability and statistics
    1. Probabilistic algorithms
    2. Probabilistic reasoning algorithms
      1. Markov-chain Monte Carlo methods
      2. Sequential Monte Carlo methods

Recommendations

Falsification of temporal properties of hybrid systems using the cross-entropy method
HSCC '12: Proceedings of the 15th ACM international conference on Hybrid Systems: Computation and Control

Randomized testing is a popular approach for checking properties of large embedded system designs. It is well known that a uniform random choice of test inputs is often sub-optimal. Ideally, the choice of inputs has to be guided by choosing the right ...
Read More
Monte-carlo techniques for falsification of temporal properties of non-linear hybrid systems
HSCC '10: Proceedings of the 13th ACM international conference on Hybrid systems: computation and control

We present a Monte-Carlo optimization technique for finding inputs to a system that falsify a given Metric Temporal Logic (MTL) property. Our approach performs a random walk over the space of inputs guided by a robustness metric defined by the MTL ...
Read More
Relaxed Decidability and the Robust Semantics of Metric Temporal Logic
HSCC '17: Proceedings of the 20th International Conference on Hybrid Systems: Computation and Control

Relaxed notions of decidability widen the scope of automatic verification of hybrid systems. In quasi-decidability and delta-decidability, the fundamental compromise is that if we are willing to accept a slight error in the algorithm's answer, or a ...
Read More

Comments

Information & Contributors

Information

Published In

cover image ACM Transactions on Embedded Computing Systems

ACM Transactions on Embedded Computing Systems Volume 12, Issue 2s

Special Section on Probabilistic Embedded Computing

May 2013

269 pages

ISSN:1539-9087

EISSN:1558-3465

DOI:10.1145/2465787

Issue’s Table of Contents

Copyright © 2013 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]

Publisher

Association for Computing Machinery

New York, NY, United States

Journal Family

ACM Journals for the Design of Smart and Connected Systems

Publication History

Published: 01 May 2013

Accepted: 01 December 2011

Revised: 01 November 2011

Received: 01 June 2011

Published in TECS Volume 12, Issue 2s

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed

Funding Sources

Division of Computer and Network Systems

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

113
Total Citations
View Citations
1,027
Total Downloads

Downloads (Last 12 months)67
Downloads (Last 6 weeks)6

Other Metrics

View Author Metrics

Citations

Cited By

Abou-Mrad CAbbas H(2024)Approximating the Geometry of Temporal Logic FormulasProceedings of the 27th ACM International Conference on Hybrid Systems: Computation and Control10.1145/3641513.3650139(1-10)Online publication date: 14-May-2024
https://dl.acm.org/doi/10.1145/3641513.3650139
Biewer SBaum KSterz SHermanns HHetmank SLanger MLauber-Rönsberg ALehr F(2024)Software doping analysis for human oversightFormal Methods in System Design10.1007/s10703-024-00445-2Online publication date: 4-Apr-2024
https://doi.org/10.1007/s10703-024-00445-2
Iyer RKalbarczyk ZNakka N(2024)Classical Dependability Techniques and Modern Computing SystemsDependable Computing10.1002/9781119743453.ch2(25-56)Online publication date: 26-Apr-2024
https://doi.org/10.1002/9781119743453.ch2
Iyer RKalbarczyk ZNakka N(2024)The FutureDependable Computing10.1002/9781119743453.ch14(745-796)Online publication date: 26-Apr-2024
https://doi.org/10.1002/9781119743453.ch14
Damm WHess DSchweda MSztipanovits JBengler KBiebl BFränzle MHagemann WHeld MIhme KKacianka SKerscher ALehnhoff SLuedtke APretschner ARakow ARieger JSonntag DSchwammberger MAustel BUnni AVeith E(2023)A Reference Architecture of Human Cyber-Physical Systems – Part I: Fundamental ConceptsACM Transactions on Cyber-Physical Systems10.1145/36228798:1(1-32)Online publication date: 20-Sep-2023
https://dl.acm.org/doi/10.1145/3622879
Maiti SBalabhaskara AAdhikary SKoley IDey SMeng WJensen CCremers CKirda E(2023)Targeted Attack Synthesis for Smart Grid Vulnerability AnalysisProceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security10.1145/3576915.3623155(2576-2590)Online publication date: 15-Nov-2023
https://dl.acm.org/doi/10.1145/3576915.3623155
Chandratre AHernandez Acosta TKhandait TPedrielli GFainekos G(2023)Stealthy attacks formalized as STL formulas for Falsification of CPS SecurityProceedings of the 26th ACM International Conference on Hybrid Systems: Computation and Control10.1145/3575870.3587122(1-8)Online publication date: 9-May-2023
https://dl.acm.org/doi/10.1145/3575870.3587122
Mancini TMelatti ITronci E(2023)Optimizing Highly-Parallel Simulation-Based Verification of Cyber-Physical SystemsIEEE Transactions on Software Engineering10.1109/TSE.2023.329843249:9(4443-4455)Online publication date: 1-Sep-2023
https://doi.org/10.1109/TSE.2023.3298432
Klischat MAlthoff M(2023)Falsifying Motion Plans of Autonomous Vehicles With Abstractly Specified Traffic ScenariosIEEE Transactions on Intelligent Vehicles10.1109/TIV.2022.31911798:2(1717-1730)Online publication date: Feb-2023
https://doi.org/10.1109/TIV.2022.3191179
Wetzlinger MKochdumper NBak SAlthoff M(2023)Fully Automated Verification of Linear Systems Using Inner and Outer Approximations of Reachable SetsIEEE Transactions on Automatic Control10.1109/TAC.2023.329200868:12(7771-7786)Online publication date: Dec-2023
https://doi.org/10.1109/TAC.2023.3292008
Show More Cited By

View Options

Get Access

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 Article

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Issue’s Table of Contents