 |
    |
Hierarchical Reasoning and Model Generation for the Verification of Parametric Hybrid Systems
Viorica Sofronie-Stokkermans
University of Koblenz-Landau and Max-Planck-Institut für Informatik, Saarbrücken, Germanysofronie@uni-koblenz.de
Abstract. In this paper we study possibilities of using hierarchical reasoning, quantifier elimination and model generation for the verification of parametric hybrid systems, where the parameters can be constants or functions. Our goal is to automatically provide guarantees that such systems satisfy certain safety or invariance conditions. We first analyze the possibility of automatically generating such guarantees in the form of constraints on parameters, then show that we can also synthesise so-called criticality functions, typically used for proving stability and/or safety of hybrid systems. We illustrate our methods on several examples.
LNAI 7898, p. 360 ff.
lncs@springer.com
© Springer-Verlag Berlin Heidelberg 2013