D 2019

Accelerating Parameter Synthesis Using Semi-algebraic Constraints

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

Basic information

Original name

Accelerating Parameter Synthesis Using Semi-algebraic Constraints

Authors

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

Edition

LNCS 11918. Cham, Integrated Formal Methods, p. 27-45, 19 pp. 2019

Publisher

Springer International Publishing

Other information

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10201 Computer sciences, information science, bioinformatics

Confidentiality degree

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

Publication form

electronic version available online

References:

Impact factor

Impact factor: 0.402 in 2005

RIV identification code

RIV/00216224:14330/19:00108262

Organization unit

Faculty of Informatics

ISBN

978-3-030-34967-7

ISSN

UT WoS

000611734300002

Keywords in English

parameter synthesis; semi-algebraic set; CTL

Tags

International impact, Reviewed
Změněno: 15/4/2021 12:06, doc. RNDr. David Šafránek, Ph.D.

Abstract

V originále

We propose a novel approach to parameter synthesis for parametrised Kripke structures and CTL specifications. In our method, we suppose the parametrisations form a semi-algebraic set and we utilise a symbolic representation using the so-called cylindrical algebraic decomposition of corresponding multivariate polynomials. Specifically, we propose a new data structure allowing to compute and efficiently manipulate such representations. The new method is significantly faster than our previous method based on SMT. We apply the method to a set of rational dynamical systems representing complex biological mechanisms with non-linear behaviour.

Links

GA18-00178S, research and development project
Name: Diskrétní bifurkační analýza reaktivních systémů
Investor: Czech Science Foundation