Original title: HyperLTL Model Checking
Translated title: HyperLTL Model Checking
Authors: Alexaj, Ondrej ; Strejček, Jan (referee) ; Lengál, Ondřej (advisor)
Document type: Bachelor's theses
Year: 2024
Language: eng
Publisher: Vysoké učení technické v Brně. Fakulta informačních technologií
Abstract: [eng] [cze]
HyperLTL model checking je technika pre overenie systému voči danej hypervlastnosti vyjadrenej logikou HyperLTL, ktorá dokáže prepojiť viaceré spustenia systému. Hoci bol vytvorený algoritmický prístup založený na automatoch, spolieha sa na štandardné operácie -automatov. Cieľom tejto práce je prekonať kompletný state-of-the-art HyperLTL model checker AutoHyper využitím efektívnejších čiastkových operácií nad automatmi, najmä komplementácie a inklúzie. Implementácia HyperLTL model checkingu v modulárne založenom nástroji pre komplementáciu, Kofola, viedla k výraznému zvýšeniu výkonu v porovnaní s referenčným nástrojom. Napokon, náš prístup ku kontrole jazykovej inklúzie vykazuje výrazné zmenšenie generovaného stavového priestoru. Keďže ide o bežne používanú operáciu nad automatmi, náš prístup by potenciálne mohol prispieť k pokroku aj v iných oblastiach verifikácie. HyperLTL model checking is an approach to verifying a system against a given hyperproperty, which is able to relate multiple executions of a system. The algorithmic approach based on automata which relies on standard -automata operations is well established. The aim of this work is to outperform the complete state-of-the-art HyperLTL model checker AutoHyper by employing more efficient partial automata operations, in particular complementation and inclusion. The implementation of HyperLTL model checking in a novel modular-based complementation tool Kofola resulted in a significant enhancement in performance compared to the reference tool. Finally, our approach to language inclusion checking shows a notable improvement in terms of the generated state space. As a commonly used automata operation, it could potentially contribute to the advancement of other areas of verification.
Keywords: formálna verifikácia; HyperLTL; jazyková inklúzia; model checking; prázdnosť jazyka; TGBA; formal verification; HyperLTL; language emptiness; language inclusion; model checking; on-the-fly; TGBA

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

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


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