An SMT-based Approach to analyze Non-Linear Relations of Parameters for Hybrid Systems



Deriving constraints over parameters to avoid unexpected system behaviors is extremely important for parametric analysis of hybrid systems. In the long run, our project aims for an SMT-based approach to reveal non-linear relations between parameters for hybrid systems that are specified by parameterized formal models using standard data types (reals, integers and booleans) and affine dynamics. The problem we address is undecidable since the underlying logic consists of boolean combinations of propositional logic atoms as well as atoms from non-linear arithmetic theories over integers and reals with quantifiers. Currently, a symbolic simulation algorithm has been prototypically implemented based on a new developed prototypical constraint solver.


SMT, Constraints over Parameters, Parametric Analysis 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Bauer, K., Schneider, K.: From synchronous programs to symbolic representations of hybrid systems. In Johansson, K., Yi, W., eds.: Hybrid Systems: Computation and Control (HSCC), Stockholm, Sweden, ACM (2010) 41–50Google Scholar
  2. 2.
    Cimatti, A., Mover, S., Tonetta, S.: HyDI: A language for symbolic hybrid systems with discrete interaction. In: Software Engineering and Advanced Applications (SEAA), 2011 37th EUROMICRO Conference on, IEEE Computer Society (2011) 275–278Google Scholar
  3. 3.
    Li, X., Schneider, K.: A counterexample-guided approach to symbolic simulation of hybrid systems. In: Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV), Chemnitz, Germany, In proceeding (2015)Google Scholar
  4. 4.
    Bordeaux, L., Hamadi, Y., Zhang, L.: Propositional satisfiability and constraint programming: A comparative survey. ACM Computing Surveys (CSUR) 38 (2006)Google Scholar
  5. 5.
    Franzle, M., Herde, C.: HySAT: An efficient proof engine for bounded model checking of hybrid systems. Formal Methods in System Design (FMSD) 30 (2007) 179–198CrossRefGoogle Scholar
  6. 6.
    Cimatti, A., Griggio, A., Joost Schaafsma, B., Sebastiani, R.: The MathSAT5 SMT solver. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Volume 7795 of LNCS., Rome, Italy, Springer (2013) 93–107Google Scholar
  7. 7.
    CVC4. Scholar
  8. 8.
    Z3. Scholar
  9. 9.
    Platzer, A.: Logical Analysis of Hybrid Systems – Proving Theorems for Complex Dynamics. Springer (2010)Google Scholar
  10. 10.
    Andre, E., Fribourg, L., Kühne, U., Soulat, R.: IMITATOR 2.5: A tool for analyzing robustness in scheduling problems. In: Proceedings of the 18th International Symposium on Formal Methods (FM’12). Volume 7436 of Lecture Notes in Computer Science., Paris, France, Springer (2012) 33–36Google Scholar
  11. 11.
    Frehse, G., Le Guernic, C., Donze, A., Cotton, S., Ray, R., Lebeltel, O., Ripado, R., Girard, A., Dang, T., Maler, O.: SpaceEx: Scalable verification of hybrid systems. In: Computer Aided Verification (CAV). Volume 6806 of LNCS., Snowbird, Utah, USA, Springer (2011) 379–395Google Scholar
  12. 12.
    Annichini, A., Bouajjani, A., Sighireanu, M.: TReX: A tool for reachability analysis of complex systems. In: Computer Aided Verification (CAV). Volume 2102 of LNCS., Paris, France, Springer (2001) 368–372Google Scholar
  13. 13.
    Eggers, A., Franzle, M., Herde, C.: SAT modulo ODE: A direct SAT approach to hybrid systems. In: Automated Technology for Verification and Analysis (ATVA). Volume 5311 of LNCS., Seoul, South Korea, Springer (2008) 171–185Google Scholar
  14. 14.
    Gao, S., Kong, S., Clarke, E.: dReal: An SMT solver for nonlinear theories over the reals. In: Conference on Automated Deduction (CADE). Volume 7898 of LNCS., Lake Placid, NY, USA, Springer (2013) 208–214Google Scholar
  15. 15.
  16. 16.
    Reduce. Scholar
  17. 17.
    Bonami, P., Biegler, L., Conn, A., CornueJols, G., Grossmann, I., Laird, C., Lee, J., Lodi, A., Margot, F., Sawaya, N., Wüchter, A.: An algorithmic framework for convex mixed integer nonlinear programs. Discret. Optim. 5 (2008) 186–204MATHGoogle Scholar
  18. 18.
    Schneider, K.: The synchronous programming language Quartz. Internal Report 375, Department of Computer Science, University of Kaiserslautern, Kaiserslautern, Germany (2009)Google Scholar

Copyright information

© Springer Fachmedien Wiesbaden 2015

Authors and Affiliations

  1. 1.Embedded Systems Group, Department of Computer ScienceUniversity of KaiserslauternKaiserslauternGermany

Personalised recommendations