Bakalářská práce

Translation of MTL over Untimed Words to Counter Automata

Matej Gladiš
Anotace

Metrická temporálna logika (MTL) rozširuje lineárnu temporálnu logiku (LTL) o intervalové obmedzenia temporálnych operátorov. Nad nečasovanými nekonečnými slovami možno MTL formuly prevádzať na ekvivalentné automaty, avšak štandardné prístupy spočívajú v preklade MTL do LTL, čo spôsobuje rast veľkosti samotnej formuly a tým aj výsledného automatu v závislosti od veľkosti intervalov. Táto práca zavádza …více

Abstract

Metric Temporal Logic (MTL) extends Linear Temporal Logic (LTL) with interval constraints on temporal operators. Over untimed infinite words, an MTL formula can be translated into an equivalent automaton. However, standard approaches first translate MTL into LTL, causing both the formula and the resulting automaton to grow with the size of the intervals. This thesis introduces the counter transition …více

Klíčová slova
MTL LTL alternating automata transition-based generalised Büchi automata counter automata counting sets
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. The thesis will consider the interpretation of MTL formulae over (untimed) infinite words and use the intervals as abbreviations of sequences of nested X operators. The goal of the thesis is to extend a suitable omega-automata formalism with counters and introduce a translation of MTL formulae to these automata. 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. The obtained automata will be compared to transition-based generalised Büchi automata (TGBA) obtained from the MTL formulae by their transformation into equivalent LTL formulae and subsequent translation to TGBA by Spot.
Administrativní informace
Práce zkontrolována:
22. 5. 2026 17:35, prof. RNDr. Jan Strejček, Ph.D., učo 3366
Plný text práce
690,7 KB / soubor PDF
Přílohy (1)
Jazyk práce
angličtina angličtina
Termín obhajoby
25. 6. 2026
Práce byla úspěšně obhájena

Vedoucí

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

Oponent

doc. RNDr. Vojtěch Řehák, Ph.D., učo 3721
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.