Publication details

Accelerating Parameter Synthesis Using Semi-algebraic Constraints

Authors

BENEŠ Nikola BRIM Luboš GELETKA Martin PASTVA Samuel ŠAFRÁNEK David

Year of publication 2019
Type Article in Proceedings
Conference Integrated Formal Methods
MU Faculty or unit

Faculty of Informatics

Citation
Web https://link.springer.com/chapter/10.1007/978-3-030-34968-4_2
Doi http://dx.doi.org/10.1007/978-3-030-34968-4_2
Keywords parameter synthesi; semi-algebraic se; CTL
Description 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.
Related projects: