Accelerating Parameter Synthesis Using Semi-algebraic Constraints

• Autoři: BENEŠ Nikola; BRIM Luboš; GELETKA Martin; PASTVA Samuel; ŠAFRÁNEK David
• Rok publikování: 2019
• Druh: Článek ve sborníku
• Konference: Integrated Formal Methods
• Fakulta / Pracoviště MU: Fakulta informatiky
• www: http://dx.doi.org/10.1007/978-3-030-34968-4_2
• Doi: http://dx.doi.org/10.1007/978-3-030-34968-4_2
• Klíčová slova: parameter synthesis; semi-algebraic set; CTL
• Popis: We propose a novel approach to parameter synthesis for parametrised Kripke structures and CTL specifications. In our method, we suppose the parametrisations form a semi-algebraic set and we utilise a symbolic representation using the so-called cylindrical algebraic decomposition of corresponding multivariate polynomials. Specifically, we propose a new data structure allowing to compute and efficiently manipulate such representations. The new method is significantly faster than our previous method based on SMT. We apply the method to a set of rational dynamical systems representing complex biological mechanisms with non-linear behaviour.

Související projekty

• Diskrétní bifurkační analýza reaktivních systémů