Advertisement
Published in:
2015 | OriginalPaper | Chapter
An SMT-based Approach to analyze Non-Linear Relations of Parameters for Hybrid Systems
Authors : Xian Li, Klaus Schneider
Published in: Formal Modeling and Verification of Cyber-Physical Systems
Publisher: Springer Fachmedien Wiesbaden
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
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.