Thesis Details
Hledání řídicích strategií pomocí UPPAAL STRATEGO
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.
formal verification, model checking, timed automata, modal logic, query language, Uppaal, Uppaal SMC, Uppaal Stratego, control strategy
Drahanský Martin, prof. Ing., Dipl.-Ing., Ph.D. (DITS FIT BUT), člen
Grézl František, Ing., Ph.D. (DCGM FIT BUT), člen
Hrubý Martin, Ing., Ph.D. (DITS FIT BUT), člen
Polčák Libor, Ing., Ph.D. (DIFS FIT BUT), člen
@bachelorsthesis{FITBT22413,
author = "Filip Hru\v{s}ka",
type = "Bachelor's thesis",
title = "Hled\'{a}n\'{i} \v{r}\'{i}dic\'{i}ch strategi\'{i} pomoc\'{i} UPPAAL STRATEGO",
school = "Brno University of Technology, Faculty of Information Technology",
year = 2020,
location = "Brno, CZ",
language = "czech",
url = "https://www.fit.vut.cz/study/thesis/22413/"
}