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

D 2017

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

BENEŠ, Nikola, Luboš BRIM, Martin DEMKO, Samuel PASTVA, David ŠAFRÁNEK et. al.

Basic information

Original name

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

Authors

BENEŠ, Nikola (203 Czech Republic, belonging to the institution), Luboš BRIM (203 Czech Republic, guarantor, belonging to the institution), Martin DEMKO (703 Slovakia, belonging to the institution), Samuel PASTVA (703 Slovakia, belonging to the institution) and David ŠAFRÁNEK (203 Czech Republic, belonging to the institution)

Edition

LNCS 10426. Cham, Computer Aided Verification. CAV 2017, p. 591-598, 8 pp. 2017

Publisher

Springer International Publishing

Other information

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

Czech Republic

Confidentiality degree

není předmětem státního či obchodního tajemství

Publication form

printed version "print"

References:

URL

Impact factor

Impact factor: 0.402 in 2005

RIV identification code

RIV/00216224:14330/17:00094898

Organization unit

Faculty of Informatics

ISBN

978-3-319-63386-2

ISSN

DOI

http://dx.doi.org/10.1007/978-3-319-63387-9_29

UT WoS

000432196400029

Keywords in English

model checking; satisfiability modulo theories; Computational Tree Logic; dynamical systems; distributed algorithms

Abstract

V originále

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.

Links

GA15-11089S, research and development project

Name: Získávání parametrů biologických modelů pomocí techniky ověřování modelů

Investor: Czech Science Foundation

LM2015055, research and development project

Name: Centrum pro systémovou biologii (Acronym: C4SYS)

Investor: Ministry of Education, Youth and Sports of the CR

MUNI/A/0897/2016, interní kód MU

Name: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace VI.

Investor: Masaryk University, Category A

MUNI/A/0992/2016, interní kód MU

Name: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity (Acronym: SKOMU)

Investor: Masaryk University, Category A

Citovat

BENEŠ, Nikola, Luboš BRIM, Martin DEMKO, Samuel PASTVA and David ŠAFRÁNEK. Pithya: A Parallel Tool for Parameter Synthesis of Piecewise Multi-Affine Dynamical Systems. In Rupak Majumdar and Viktor Kunčak. Computer Aided Verification. CAV 2017. LNCS 10426. Cham: Springer International Publishing, 2017, p. 591-598. ISBN 978-3-319-63386-2. Available from: https://dx.doi.org/10.1007/978-3-319-63387-9_29.

@inproceedings{1387857,
   author = {Beneš, Nikola and Brim, Luboš and Demko, Martin and Pastva, Samuel and Šafránek, David},
   address = {Cham},
   booktitle = {Computer Aided Verification. CAV 2017},
   doi = {http://dx.doi.org/10.1007/978-3-319-63387-9_29},
   edition = {LNCS 10426},
   editor = {Rupak Majumdar and Viktor Kunčak},
   keywords = {model checking; satisfiability modulo theories; Computational Tree Logic; dynamical systems; distributed algorithms},
   howpublished = {tištěná verze "print"},
   language = {eng},
   location = {Cham},
   isbn = {978-3-319-63386-2},
   pages = {591-598},
   publisher = {Springer International Publishing},
   title = {Pithya: A Parallel Tool for Parameter Synthesis of Piecewise Multi-Affine Dynamical Systems},
   url = {https://doi.org/10.1007/978-3-319-63387-9_29},
   year = {2017}
}

TY  - JOUR
ID  - 1387857
AU  - Beneš, Nikola - Brim, Luboš - Demko, Martin - Pastva, Samuel - Šafránek, David
PY  - 2017
TI  - Pithya: A Parallel Tool for Parameter Synthesis of Piecewise Multi-Affine Dynamical Systems
PB  - Springer International Publishing
CY  - Cham
SN  - 9783319633862
KW  - model checking
KW  - satisfiability modulo theories
KW  - Computational Tree Logic
KW  - dynamical systems
KW  - distributed algorithms
UR  - https://doi.org/10.1007/978-3-319-63387-9_29
N2  - 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.
ER  -

BENEŠ, Nikola, Luboš BRIM, Martin DEMKO, Samuel PASTVA and David ŠAFRÁNEK. Pithya: A Parallel Tool for Parameter Synthesis of Piecewise Multi-Affine Dynamical Systems. In Rupak Majumdar and Viktor Kunčak. \textit{Computer Aided Verification. CAV 2017}. LNCS 10426. Cham: Springer International Publishing, 2017, p.~591-598. ISBN~978-3-319-63386-2. Available from: https://dx.doi.org/10.1007/978-3-319-63387-9\_{}29.

Detailed Information on Publication Record