D 2013

Effective Translation of LTL to Deterministic Rabin Automata: Beyond the (F,G)-Fragment

BLAHOUDEK, František, Tomáš BABIAK, Mojmír KŘETÍNSKÝ and Jan STREJČEK

Basic information

Original name

Effective Translation of LTL to Deterministic Rabin Automata: Beyond the (F,G)-Fragment

Name in Czech

Efektivní překlad LTL na deterministické Rabinovy automaty

Authors

BLAHOUDEK, František (203 Czech Republic, belonging to the institution), Tomáš BABIAK (703 Slovakia, belonging to the institution), Mojmír KŘETÍNSKÝ (203 Czech Republic, belonging to the institution) and Jan STREJČEK (203 Czech Republic, guarantor, belonging to the institution)

Edition

Berlin Heidelberg, 11th International Symposium on Automated Technology for Verification and Analysis, ATVA 2013, p. 24-38, 15 pp. 2013

Publisher

Springer

Other information

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

United States of America

Confidentiality degree

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

Publication form

printed version "print"

Impact factor

Impact factor: 0.402 in 2005

RIV identification code

RIV/00216224:14330/13:00066175

Organization unit

Faculty of Informatics

ISBN

978-3-319-02443-1

ISSN

DOI

Keywords in English

linear temporal logic; deterministic omega-automata

Tags

Tags

International impact, Reviewed
Změněno: 15/11/2013 23:58, prof. RNDr. Jan Strejček, Ph.D.

Abstract

ORIG CZ

V originále

Some applications of linear temporal logic (LTL) require to translate formulae of the logic to deterministic omega-automata. There are currently two translators producing deterministic automata: ltl2dstar working for the whole LTL and Rabinizer applicable to the fragment LTL(F,G). We present a new translation to deterministic Rabin automata via alternating automata and deterministic transition-based generalized Rabin automata. Our translation applies to a fragment that is strictly larger than LTL(F,G). Experimental results show that our algorithm can produce significantly smaller automata compared to Rabinizer and ltl2dstar, especially for more complex LTL formulae.

In Czech

Některé aplikace Lineární temporální logiky (LTL) vyžadují překlad formulí této logiky na deterministické omega-automaty. V současnosti existují dva překladače produkující deterministické automaty: ltl2dstar zpracovávající celou logiku LTL a Rabinizer použitelný pouze na fragmentu LTL (F,G). Představujeme nový algoritmus pro překlad LTL formulí na deterministické Rabinovy automaty přes alternující automaty a deterministické zobecněné Rabinovy automaty s akceptující podmínkou na hranách. Náš překlad funguje pro fragment LTL, který je striktně větší než LTL(F,G). Experimentální výsledky ukazují, že náš algoritmus může produkovat podstatně menší automaty v porovnání s Rabinizerem s ltl2dstar, zejména pro složitější LTL formule.

Links

GBP202/12/G061, research and development project
Name: Centrum excelence - Institut teoretické informatiky (CE-ITI) (Acronym: CE-ITI)
Investor: Czech Science Foundation
MUNI/A/0739/2012, interní kód MU
Name: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity (Acronym: SKOMU)
Investor: Masaryk University, Category A
MUNI/A/0760/2012, interní kód MU
Name: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace II. (Acronym: FI MAV II.)
Investor: Masaryk University, Category A