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

D 2016

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

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

Základní údaje

Originální název

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

Autoři

BENEŠ, Nikola (203 Česká republika, domácí), Luboš BRIM (203 Česká republika, domácí), Martin DEMKO (703 Slovensko, domácí), Samuel PASTVA (703 Slovensko, domácí) a David ŠAFRÁNEK (203 Česká republika, garant, domácí)

Vydání

LNCS 9938. Neuveden, Automated Technology for Verification and Analysis. ATVA 2016, od s. 192-208, 17 s. 2016

Nakladatel

Springer International Publishing

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Česká republika

Utajení

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

Forma vydání

tištěná verze "print"

Impakt faktor

Impact factor: 0.402 v roce 2005

Kód RIV

RIV/00216224:14330/16:00088098

Organizační jednotka

Fakulta informatiky

ISBN

978-3-319-46519-7

ISSN

DOI

http://dx.doi.org/10.1007/978-3-319-46520-3_13

UT WoS

000389808100013

Klíčová slova anglicky

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

Štítky

core_A, firank_A

Příznaky

Mezinárodní význam, Recenzováno

Změněno: 13. 5. 2020 19:15, RNDr. Pavel Šmerk, Ph.D.

Anotace

V originále

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.

Návaznosti

GA15-11089S, projekt VaV

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

Investor: Grantová agentura ČR, Získávání parametrů biologických modelů pomocí techniky ověřování modelů

MUNI/A/0945/2015, interní kód MU

Název: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace V.

Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace V., DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty

Citovat

BENEŠ, Nikola, Luboš BRIM, Martin DEMKO, Samuel PASTVA a David ŠAFRÁNEK. Parallel SMT-Based Parameter Synthesis with Application to Piecewise Multi-Affine Systems. In Cyrille Artho et al. Automated Technology for Verification and Analysis. ATVA 2016. LNCS 9938. Neuveden: Springer International Publishing, 2016, s. 192-208. ISBN 978-3-319-46519-7. Dostupné z: https://dx.doi.org/10.1007/978-3-319-46520-3_13.

@inproceedings{1352259,
   author = {Beneš, Nikola and Brim, Luboš and Demko, Martin and Pastva, Samuel and Šafránek, David},
   address = {Neuveden},
   booktitle = {Automated Technology for Verification and Analysis. ATVA 2016},
   doi = {http://dx.doi.org/10.1007/978-3-319-46520-3_13},
   edition = {LNCS 9938},
   editor = {Cyrille Artho et al.},
   keywords = {model checking; satisfiability modulo theories; Computational Tree Logic; dynamical systems; distributed algorithms},
   howpublished = {tištěná verze "print"},
   language = {eng},
   location = {Neuveden},
   isbn = {978-3-319-46519-7},
   pages = {192-208},
   publisher = {Springer International Publishing},
   title = {Parallel SMT-Based Parameter Synthesis with Application to Piecewise Multi-Affine Systems},
   year = {2016}
}

TY  - JOUR
ID  - 1352259
AU  - Beneš, Nikola - Brim, Luboš - Demko, Martin - Pastva, Samuel - Šafránek, David
PY  - 2016
TI  - Parallel SMT-Based Parameter Synthesis with Application to Piecewise Multi-Affine Systems
PB  - Springer International Publishing
CY  - Neuveden
SN  - 9783319465197
KW  - model checking
KW  - satisfiability modulo theories
KW  - Computational Tree Logic
KW  - dynamical systems
KW  - distributed algorithms
N2  - 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.
ER  -

BENEŠ, Nikola, Luboš BRIM, Martin DEMKO, Samuel PASTVA a David ŠAFRÁNEK. Parallel SMT-Based Parameter Synthesis with Application to Piecewise Multi-Affine Systems. In Cyrille Artho et al. \textit{Automated Technology for Verification and Analysis. ATVA 2016}. LNCS 9938. Neuveden: Springer International Publishing, 2016, s.~192-208. ISBN~978-3-319-46519-7. Dostupné z: https://dx.doi.org/10.1007/978-3-319-46520-3\_{}13.

Podrobný výpis o publikaci