Original title: Převod LTL formulí s omezenými operátory do automatů s čítači
Translated title: Translation of LTL with Bounded Repetition to Automata with Counters
Authors: Slezáková, Alexandra ; Smrčka, Aleš (referee) ; Holík, Lukáš (advisor)
Document type: Bachelor's theses
Year: 2020
Language: slo
Publisher: Vysoké učení technické v Brně. Fakulta informačních technologií
Abstract: [slo] [eng]
Táto práca rieši prevod LTL formulí s obmedzenými operátormi (temporálne operátory, ktoré majú obmedzenú platnosť na určitý počet krokov) do automatu s čítačmi. Použitím klasických metód je automatová reprezentácia takýchto formulí veľká, pretože veľkosť automatu môže byť exponenciálna k hornej hranici obmedzenia. Prezentujeme konštrukciu, ktorá vytvára automat nezávislý na obmedzení. Práca predstavuje riešenie problému pomocou čítačového Büchi automatu. Čítače zaisťujú nevytváranie podobných stavov a prechodov, čo vedie k zmenšeniu veľkosti automatu. Naša metóda je implementovaná a experimentálne overená. Počet stavov automatu pre formule s veľkým obmedzením operátora redukujeme niekoľkonásobne v porovnaní s klasickými metódami. 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: counting Büchi automaton; linear temporal logic; LTL with bounded repetition; model checking; translation of LTL formulas

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/191424

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


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