D 2010

Translation of LTL to Büchi Automata: Improved Once Again

BABIAK, Tomáš

Základní údaje

Originální název

Translation of LTL to Büchi Automata: Improved Once Again

Název česky

Překlad logiky LTL na Büchiho Automaty: Opětovně vylepšeno

Autoři

Vydání

Aachen, Germany, Proceedings of 9th International Summer School on Modelling and Verifying Parallel Processes 2010 (MOVEP 2010), od s. 41-46, 6 s. 2010

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Německo

Utajení

není předmětem státního či obchodního tajemství

Označené pro přenos do RIV

Ne

Organizační jednotka

Fakulta informatiky

Klíčová slova česky

LTL; logika lineárního času; překlad LTL; Büchiho automaty; ověřování modelu

Klíčová slova anglicky

LTL; linear time logic; translation of LTL; Büchi Automata; model checking

Příznaky

Mezinárodní význam
Změněno: 16. 1. 2011 23:00, RNDr. Tomáš Babiak, Ph.D.

Anotace

ORIG CZ

V originále

We present an improvement of an algorithm translating LTL formulae into Büchi automata via alternating automata. In particular, we improve the transformation of alternating Büchi automata to generalized Büchi automata, where we temporarily ignore some transitions leading from the alternating automata states corresponding to subformulae that are prefix-invariant. Experimental results show that our improvements can lead to faster translation and less nondeterminism of the resulting Büchi automata.

Česky

V článku představujeme vylepšení algoritmu, který překládá LTL formule na Büchiho automaty pomocí alternujících automatů. Konkrétněji zlepšujeme převod alternujících Büchiho automatů na generalizované Büchiho automaty, kde dočasně ignorujeme některé přechody vedoucí ze stavů alternujícího automatu, které odpovídají prefixově invariantním formulím. Experimentální výsledky ukazují, že naše zlepšení může vést k rychlejšímu překladu a výsledným Büchiho automatům, které jsou méně nedeterministické.

Návaznosti

GA201/09/1389, projekt VaV
Název: Verifikace a analýza velmi velkých počítačových systémů
Investor: Grantová agentura ČR, Verifikace a analýza velmi velkých počítačových systémů
MSM0021622419, záměr
Název: Vysoce paralelní a distribuované výpočetní systémy
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Vysoce paralelní a distribuované výpočetní systémy
MUNI/A/0914/2009, interní kód MU
Název: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace (Akronym: SV-FI MAV)
Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace, DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty