{"id":{"repo_id":"brno-tech","oai_identifier":"oai:dspace.vut.cz:11012/246576"},"canonical_url":"https://search.dev.ndltd.org/etd/brno-tech/oai:dspace.vut.cz:11012/246576","repository":{"repo_id":"brno-tech","name":"Brno University of Technology","base_url":"https://dspace.vut.cz/oai/request"},"display":{"title":"HyperLTL Model Checking","abstract":"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.","abstract_html":"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.","abstract_has_math":false,"creators":["Alexaj, Ondrej"],"institution":"Vysoké učení technické v Brně. Fakulta informačních technologií","degree_name":null,"degree_level":null,"degree_discipline":null,"degree_department":null,"school":null,"contributors":[],"advisors":["Lengál, Ondřej"],"committee_chairs":[],"committee_members":[],"year":null,"date_issued":"","date_published":null,"updated_at":"2026-07-24T01:22:44Z","subjects":["formálna verifikácia","model checking","HyperLTL","TGBA","jazyková inklúzia","prázdnosť jazyka","formal verification","language inclusion","on-the-fly","language emptiness"],"languages":["en"],"rights":["Standardní licenční smlouva - přístup k plnému textu bez omezení"],"rights_urls":[],"identifier_entries":[{"key":"dc:identifier.other","label":"Dc Identifier Other","values":["154514"],"render_values":[{"text":"154514","href":null,"code":true}]}]},"links":{"outbound_url":"http://hdl.handle.net/11012/246576","outbound_label":"Handle","outbound_source":"dc:identifier.uri"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor.advisor","label":"Advisor","values":["Lengál, Ondřej"]},{"key":"dc:creator","label":"Author","values":["Alexaj, Ondrej"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:publisher","label":"Institution","values":["Vysoké učení technické v Brně. Fakulta informačních technologií"]},{"key":"dc:type","label":"Dc Type","values":["Text"]},{"key":"thesis:institution_name","label":"Thesis Institution Name","values":["Bc."]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["formálna verifikácia","model checking","HyperLTL","TGBA","jazyková inklúzia","prázdnosť jazyka","formal verification","language inclusion","on-the-fly","language emptiness"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language.iso","label":"Language (ISO)","values":["en"]},{"key":"dc:rights","label":"Dc Rights","values":["Standardní licenční smlouva - přístup k plnému textu bez omezení"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier.other","label":"Dc Identifier Other","values":["154514"]},{"key":"dc:identifier.uri","label":"Identifier URI","values":["http://hdl.handle.net/11012/246576"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description.abstract","label":"Abstract","values":["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."]},{"key":"dc:title","label":"Title","values":["HyperLTL Model Checking"]}]}],"canonical_facts":{"dc:contributor.advisor":["Lengál, Ondřej"],"dc:creator":["Alexaj, Ondrej"],"dc:description.abstract":["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."],"dc:identifier.other":["154514"],"dc:identifier.uri":["http://hdl.handle.net/11012/246576"],"dc:language.iso":["en"],"dc:publisher":["Vysoké učení technické v Brně. Fakulta informačních technologií"],"dc:rights":["Standardní licenční smlouva - přístup k plnému textu bez omezení"],"dc:subject":["formálna verifikácia","model checking","HyperLTL","TGBA","jazyková inklúzia","prázdnosť jazyka","formal verification","language inclusion","on-the-fly","language emptiness"],"dc:title":["HyperLTL Model Checking"],"dc:type":["Text"],"thesis:institution_name":["Bc."]},"updated_at":"2026-07-24T01:22:44Z"}