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

Varování

Publikace nespadá pod Ekonomicko-správní fakultu, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.

Název česky	Překlad logiky LTL na Büchiho Automaty: Opětovně vylepšeno
Autoři	BABIAK Tomáš
Rok publikování	2010
Druh	Článek ve sborníku
Konference	Proceedings of 9th International Summer School on Modelling and Verifying Parallel Processes 2010 (MOVEP 2010)
Fakulta / Pracoviště MU	Fakulta informatiky
Citace
Obor	Informatika
Klíčová slova	LTL; linear time logic; translation of LTL; Büchi Automata; model checking
Popis	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é.
Související projekty:	Vysoce paralelní a distribuované výpočetní systémy Verifikace a analýza velmi velkých počítačových systémů Rozsáhlé výpočetní systémy: modely, aplikace a verifikace