Pithya: A Parallel Tool for Parameter Synthesis of Piecewise Multi-Affine Dynamical Systems

• Autoři: BENEŠ Nikola; BRIM Luboš; DEMKO Martin; PASTVA Samuel; ŠAFRÁNEK David
• Rok publikování: 2017
• Druh: Článek ve sborníku
• Konference: Computer Aided Verification. CAV 2017
• Fakulta / Pracoviště MU: Fakulta informatiky
• www: https://doi.org/10.1007/978-3-319-63387-9_29
• Doi: http://dx.doi.org/10.1007/978-3-319-63387-9_29
• Obor: Informatika
• Klíčová slova: model checking; satisfiability modulo theories; Computational Tree Logic; dynamical systems; distributed algorithms
• Popis: We present a novel tool for parameter synthesis of piecewise multi-affine dynamical systems from specifications expressed in a hybrid branching-time temporal logic. The tool is based on the algorithm of parallel semi-symbolic coloured model checking that extends standard model checking methods to cope with parametrised Kripke structures. The tool implements state-of-the-art techniques developed in our previous research and is primarily intended to be used for the analysis of dynamical systems with uncertain parameters that frequently arise in computational systems biology. However, it can be employed for any dynamical system where the non-linear equations can be sufficiently well approximated by piecewise multi-affine equations.

Související projekty

• Získávání parametrů biologických modelů pomocí techniky ověřování modelů
• The national infrastructure C4SYS - Centre for Systems Biology
• Rozsáhlé výpočetní systémy: modely, aplikace a verifikace VI.
• Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity