Bakalářská práce

Counter Automata for MTL over Untimed Words

Tereza Kinská, učo 493111
Anotace

Tato práce představuje nový typ alternujícího automatu jménem COALA s počítacími množinami (tak zvanými "counting sety"), na který lze překládat MTL formule nad nečasovanými slovy. Přestože MTL formule, vyhodnocované nad nečasovanými slovy, je možné přeložit na LTL formule, a již bylo v literatuře prezentováno mnoho překladů LTL formule na automat, překlad z MTL do LTL způsobuje exponenciální nárůst …více

Abstract

This thesis presents a new type of alternating automaton with counting sets (called COALA), to which an MTL formula over untimed words can be translated. Although such an MTL formula can be translated to LTL and many algorithms for translating LTL into automata have already been presented, the translation causes an exponential blowup in the size of the formula, hence also in the size of the resulting …více

Klíčová slova
automata alternation alternating automata counting sets LTL MTL COALA
Zadání práce
MTL is an extension of LTL where temporal operators have intervals restricting their satisfaction. MTL formulae are usually interpreted over timed words. In this thesis, we interpret MTL formulae over (untimed) infinite words and use the intervals as abbreviation of sequences of nested X operators. The goal of the thesis is to extend the formalism of alternating automata with counters and introduce a translation of MTL formulae to these automata of linear size. The correctness of the translation will be proven and the translation will be implemented. Further, the translation will be applied to a set of MTL formulae from an industrial partner and the results will be presented, including the number of formulae translated to automata without alternation (i.e. to nondeterministic counter automata).
Administrativní informace
Práce zkontrolována:
5. 6. 2023 10:06, prof. RNDr. Jan Strejček, Ph.D., učo 3366
Plný text práce
1 MB / soubor PDF
Přílohy (1)
Jazyk práce
angličtina angličtina
Termín obhajoby
28. 6. 2023
Práce byla úspěšně obhájena

Vedoucí

prof. RNDr. Jan Strejček, Ph.D., učo 3366
KTP FI MU

Oponent

prof. RNDr. Mojmír Křetínský, CSc., učo 631
KTP FI MU
Citovat tuto práci
Masarykova univerzita Fakulta informatiky
Studijní program
Plán
Informatika

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.