Accelerating Parameter Synthesis Using Semi-algebraic Constraints

Investor logo

Warning

This publication doesn't include Faculty of Education. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
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 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
Keywords parameter synthesis; semi-algebraic set; 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:

You are running an old browser version. We recommend updating your browser to its latest version.