Accelerating Parameter Synthesis Using Semi-algebraic Constraints
| Authors | |
|---|---|
| Year of publication | 2019 |
| Type | Article in Proceedings |
| Conference | Integrated Formal Methods |
| MU Faculty or unit | |
| 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: |