Parallel SMT-Based Parameter Synthesis with Application to Piecewise Multi-Affine Systems

Investor logo

Warning

This publication doesn't include Faculty of Economics and Administration. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

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

Year of publication 2016
Type Article in Proceedings
Conference Automated Technology for Verification and Analysis. ATVA 2016
MU Faculty or unit

Faculty of Informatics

Citation
Doi http://dx.doi.org/10.1007/978-3-319-46520-3_13
Field Informatics
Keywords model checking; satisfiability modulo theories; Computational Tree Logic; dynamical systems; distributed algorithms
Description We propose a novel scalable parallel algorithm for synthesis of interdependent parameters from CTL specifications for non-linear dynamical systems. The method employs a symbolic representation of sets of parameter valuations in terms of the first-order theory of the reals. To demonstrate its practicability, we apply the method to a class of piecewise multi-affine dynamical systems representing dynamics of biological systems with complex non-linear behaviour.
Related projects:

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