Thesis Details

Převod LTL formulí s omezenými operátory do automatů s čítači

Bachelor's Thesis Student: Slezáková Alexandra Academic Year: 2019/2020 Supervisor: Holík Lukáš, doc. Mgr., Ph.D.
Language
Slovak
Abstract

This work solves translation of LTL with bounded repetition (temporal operators that have limited validity for a certain number of steps) to automaton with counters. Using classical methods, the automaton representation of such formulas is large, because the size of automaton may be exponential to the upper limit of the bounded repetition. We present a construction that creates the automaton independent from repetition.

The work represents a solution to the problem using the Büchi automaton with counters. The counters ensure that similar states and transitions are not created, which leads to a reduction in the size of the automaton. Our method is implemented and experimentally verified. We reduce the number of states of the automaton for formulas with large bound of operators several times in comparison to classical methods.

Keywords

translation of LTL formulas, LTL with bounded repetition, counting Büchi automaton, linear temporal logic, model checking

Department
Department of Intelligent Systems FIT BUT
Degree Programme
Information Technology
Files
Status
defended, grade A
Date
9 July 2020
Reviewer
Smrčka Aleš, Ing., Ph.D.
Committee
Rogalewicz Adam, doc. Mgr., Ph.D. (DITS FIT BUT), předseda
Burgetová Ivana, Ing., Ph.D. (DIFS FIT BUT), člen
Grézl František, Ing., Ph.D. (DCGM FIT BUT), člen
Smrčka Aleš, Ing., Ph.D. (DITS FIT BUT), člen
Vašíček Zdeněk, doc. Ing., Ph.D. (DCSY FIT BUT), člen
Citation
SLEZÁKOVÁ, Alexandra. Převod LTL formulí s omezenými operátory do automatů s čítači. Brno, 2020. Bachelor's Thesis. Brno University of Technology, Faculty of Information Technology. 2020-07-09. Supervised by Holík Lukáš. Available from: https://www.fit.vut.cz/study/thesis/22336/
BibTeX 
@bachelorsthesis{FITBT22336,
    author = "Alexandra Slez\'{a}kov\'{a}",
    type = "Bachelor's thesis",
    title = "P\v{r}evod LTL formul\'{i} s omezen\'{y}mi oper\'{a}tory do automat\r{u} s \v{c}\'{i}ta\v{c}i",
    school = "Brno University of Technology, Faculty of Information Technology",
    year = 2020,
    location = "Brno, CZ",
    language = "slovak",
    url = "https://www.fit.vut.cz/study/thesis/22336/"
}

Theses

Back to top