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

• Autoři: BENEŠ Nikola; BRIM Luboš; DEMKO Martin; PASTVA Samuel; ŠAFRÁNEK David
• Rok publikování: 2016
• Druh: Článek ve sborníku
• Konference: Automated Technology for Verification and Analysis. ATVA 2016
• Fakulta / Pracoviště MU: Fakulta informatiky
• Doi: http://dx.doi.org/10.1007/978-3-319-46520-3_13
• Obor: Informatika
• Klíčová slova: model checking; satisfiability modulo theories; Computational Tree Logic; dynamical systems; distributed algorithms
• Popis: 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.

Související projekty

• Získávání parametrů biologických modelů pomocí techniky ověřování modelů
• Rozsáhlé výpočetní systémy: modely, aplikace a verifikace V.