Original title: Hledání řídicích strategií pomocí UPPAAL STRATEGO
Translated title: Search of Control Strategies Using UPPAAL STRATEGO
Authors: Hruška, Filip ; Hrubý, Martin (referee) ; Strnadel, Josef (advisor)
Document type: Bachelor's theses
Year: 2020
Language: cze
Publisher: Vysoké učení technické v Brně. Fakulta informačních technologií
Abstract: [cze] [eng]
Tato práce se zabývá hledáním řídicích strategií v předem vybraných problémech z různých oblastí pomocí nástroje Uppaal Stratego. Byly vybrány čtyři oblasti k řešení, jmenovitě šachy, hanojské věže, posuvné pole a kinematický problém zahrnující balíček, auto a letadlo. Pro zvolené problémy a oblasti byla navržena a vytvořena sada jim odpovídajícím modelů. U hanojských věží a posuvného pole bylo možné úspěšně vyhodnotit relevantní strategie, zvedající pravděpodobnosti úspěchu až na více než 90 %. U dalších modelů byl nalezen problém ve velikosti stavového prostoru a strategie nebylo možné vyhodnotit, protože maximální kapacita paměti, kterou nástroj využívá, nebyla dostatečná. U kinematického problému se po omezení a zjednodušení modelu podařilo strategie vyhodnotit, ovšem u šachů to nebylo možné ani po významném zjednodušení. This thesis deals with finding control strategies for pre-selected problems from various areas using tool Uppaal Stratego. Four areas were selected, namely chess, a sliding puzzle, the tower of Hanoi, and a kinematic problem involving a package, a car, and an airplane. For the selected areas and problems, a set of models was designed and implemented. For the tower of Hanoi and the sliding field, it was possible to successfully evaluate relevant strategies, raising the probabilities of success to more than 90 %. For other models, a problem was found in the size of the state space and the strategies could not be evaluated because the maximum memory capacity that the tool uses was not sufficient. For the kinematic problem, after limiting and simplifying the model, the strategies were successfully evaluated, but for chess, this was not possible even after significant simplification.
Keywords: control strategy; formal verification; modal logic; model checking; query language; timed automata; Uppaal; Uppaal SMC; Uppaal Stratego; dotazovací jazyk; formální verifikace; modální logika; ověřování modelů; Uppaal; Uppaal SMC; Uppaal Stratego; časované automaty; řídicí strategie

Institution: Brno University of Technology (web)
Document availability information: Fulltext is available in the Brno University of Technology Digital Library.
Original record: http://hdl.handle.net/11012/191431

Permalink: http://www.nusl.cz/ntk/nusl-416223


The record appears in these collections:
Universities and colleges > Public universities > Brno University of Technology
Academic theses (ETDs) > Bachelor's theses