Diplomová práce
Získaná ocenění: Cena děkana FI za vynikající závěrečnou práci

CTL Model Checking for Petri Nets and the Arithmetical Hierarchy

Bc. Jan Mačák
Anotace

Práce se zabývá problémem stavově založeného model-checkingu Petriho sítí pro logiku větvícího se času (CTL). Petriho sítě a formule CTL mohou být poměrně přirozeným způsobem využity pro definování množin n-tic přirozených čísel. V práci je dokázáno, že třída všech takovýchto množin obsahuje právě všechny množiny definovatelné v jazyce aritmetiky (v predikátové logice prvního řádu). V práci jsou také …více

Abstract

The subject of interest of the thesis is state-based model checking for Petri nets and branching-time logic CTL. Petri nets and CTL formulae may be, in a rather natural way, used to define sets of n-tuples of natural numbers. It is proved that the class of all such sets contains exactly all arithmetical sets. Moreover, fragments of CTL corresponding to individual classes of the arithmetical hierarchy …více

Klíčová slova
model checking Petri nets CTL arithmetical hierarchy arithmetical sets logic computability Petriho sítě aritmetická hierarchie aritmetické množiny logika vyčíslitelnost
Zadání práce
The aim of the thesis is to establish the connection between the arithmetical hierarchy and the CTL model-checking problem for Petri nets. Furthermore, the work should also identify new fragments of CTL where the model-checking problem for Petri nets is decidable.
Administrativní informace
Práce zkontrolována:
16. 12. 2023 10:18, prof. RNDr. Antonín Kučera, Ph.D., učo 2508
Plný text práce
690,5 KB / soubor PDF
Jazyk práce
angličtina angličtina
Termín obhajoby
13. 2. 2024
Práce byla úspěšně obhájena

Vedoucí

prof. RNDr. Antonín Kučera, Ph.D., učo 2508
ITI KTP FI MU

Oponent

RNDr. Michal Ajdarów, Ph.D.
abs FI MU
Citovat tuto práci
Masarykova univerzita Fakulta informatiky
Studijní program
Plán
Principy programovacích jazyků

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.