Diplomová práce
Získaná ocenění: Cena děkana FI za vynikající závěrečnou práci

Paralelní syntéza parametrů z formulí hybridní logiky HUCTL

Parallel parameter synthesis from hybrid logic HUCTL formulas

Bc. Samuel Pastva, učo 410286
Anotace

Pri skúmaní komplexných javov v prírode sa často objavujú rôzne spôsoby modelovania, ktoré využívajú parametre pre popis neistoty vo fyzickom svete. Spojený s týmyto technikami je problém parametrickej syntézy, teda pre zvolenú vlastnosť spočítať parametrické valuácie pre ktoré model vlastnosť spĺňa. V tejto práci prezentujeme nový paralelný algoritmus pre riešenie problému parametrickej syntézy a …více

Abstract

In order to study complex phenomena arising in nature, one often uses various modelling frameworks which employ parameters to describe the uncertainty of the physical world. Related to these modelling techniques is the problem of parameter synthesis, that is to compute for a desired property the parameter valuations under which the property is satisfied in the model. In this work, we present a novel …více

Klíčová slova
parameter synthesis model checking temporal logic HUCTL dynamical system ordinary differential equation parallel algorithm parametrická syntéza overovanie modelov temporálna logika dynamický systém obyčajná diferenciálna rovnica paralelný algoritmus
Zadání práce

Cílem práce je navrhnout a implementovat paralelní algoritmus pro syntézu parametrů z vlastností formalizovaných v hybridní temporální logice HUCTL [1]. Množiny parametrů budou reprezentovány symbolicky jako formule vhodné logiky 1. řádu a algoritmus bude používat SMT pro jejích vyhodnocování [2]. Algoritmus bude na vstupu předpokládat parametrizovanou Kripkeho strukturu, která vznikne např. diskretizací ODE modelu či bude odvozena z Booleovské sítě. Cílový jazyk není specifikován, paralelní algoritmus by měl být schopen pracovat jak na architekturách s distribuovanou tak i sdílenou pamětí. Škálovatelnost výsledného programu bude ověřena na vhodné sadě příkladů.

[1] Brim, Luboš, et al. "High-performance discrete bifurcation analysis for piecewise-affine dynamical systems." International Workshop on Hybrid Systems Biology. Springer International Publishing, 2015.
[2] Beneš, Nikola, et al. "Parallel SMT-based parameter synthesis with application to piecewise multi-affine systems." International Symposium on Automated Technology for Verification and Analysis. Springer International Publishing, 2016.

Administrativní informace
Práce zkontrolována:
23. 5. 2017 07:50, prof. RNDr. Luboš Brim, CSc.
Plný text práce
512,2 KB / soubor PDF
Přílohy (1)
Jazyk práce
angličtina angličtina
Termín obhajoby
23. 6. 2017
Práce byla úspěšně obhájena

Vedoucí

prof. RNDr. Luboš Brim, CSc.
KTP FI MU

Oponent

doc. RNDr. David Šafránek, Ph.D., učo 3159
KSUZD FI MU
Citovat tuto práci
Masarykova univerzita Fakulta informatiky
Studijní program
Informatika
Obor

Práce na příbuzné téma

Seznam prací, které mají shodná klíčová slova.

Podobné práce

  • Přidání souboru

    Soubor nebo složku lze nahrát pomocí tlačítka Přidat.

  • Další operace se soubory

    Podrobnosti lze zjistit označením příslušného řádku.

  • Pohled pro experty

    Pro častou práci je možné zvolit režim Více možností.

  • Vyhledávání souborů

    Vyhledávaný výraz můžete zadat přímo do adresního řádku.

  • Rychlý přístup k souborům

    Pomocí funkce Nedávné je možné se rychle vrátit k právě prohlíženým souborům. Oblíbené soubory je také možné označit Hvězdičkou.