Compositional Approach to Suspension and Other Improvements to
LTL Translation

D 2013

Compositional Approach to Suspension and Other Improvements to LTL Translation

BABIAK, Tomáš, Thomas BADIE, Alexandre DURET-LUTZ, Mojmír KŘETÍNSKÝ, Jan STREJČEK et. al.

Basic information

Original name

Compositional Approach to Suspension and Other Improvements to LTL Translation

Authors

BABIAK, Tomáš (703 Slovakia, belonging to the institution), Thomas BADIE (250 France), Alexandre DURET-LUTZ (250 France), 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

LNCS 7976. Berlin Heidelberg, Model Checking Software - 20th International Symposium, SPIN 2013, p. 81-98, 18 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:00066141

Organization unit

Faculty of Informatics

ISBN

978-3-642-39175-0

ISSN

DOI

http://dx.doi.org/10.1007/978-3-642-39176-7_6

Keywords in English

linear time logic; model-checking; translation LTL to Buchi automata

Abstract

V originále

Recently, there was defined a fragment of LTL (containing fairness properties among other interesting formulae) whose validity over a given infinite word depends only on an arbitrary suffix of the word. Building upon an existing translation from LTL to Büchi automata, we introduce a compositional approach where subformulae of this fragment are translated separately from the rest of an input formula and the produced automata are composed in a way that the subformulae are checked only in relevant accepting strongly connected components of the final automaton. Further, we suggest improvements over some procedures commonly applied to generalized Büchi automata, namely over generalized acceptance simplification and over degeneralization. Finally we show how existing simulation-based reductions can be implemented in a signature-based framework in a way that improves the determinism of the automaton.

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

Citovat

BABIAK, Tomáš, Thomas BADIE, Alexandre DURET-LUTZ, Mojmír KŘETÍNSKÝ and Jan STREJČEK. Compositional Approach to Suspension and Other Improvements to LTL Translation. In Ezio Bartocci, C. R. Ramakrishnan. Model Checking Software - 20th International Symposium, SPIN 2013. LNCS 7976. Berlin Heidelberg: Springer, 2013, p. 81-98. ISBN 978-3-642-39175-0. Available from: https://dx.doi.org/10.1007/978-3-642-39176-7_6.

@inproceedings{1110031,
   author = {Babiak, Tomáš and Badie, Thomas and DuretandLutz, Alexandre and Křetínský, Mojmír and Strejček, Jan},
   address = {Berlin Heidelberg},
   booktitle = {Model Checking Software - 20th International Symposium, SPIN 2013},
   doi = {http://dx.doi.org/10.1007/978-3-642-39176-7_6},
   edition = {LNCS 7976},
   editor = {Ezio Bartocci, C. R. Ramakrishnan},
   keywords = {linear time logic; model-checking; translation LTL to Buchi automata},
   howpublished = {tištěná verze "print"},
   language = {eng},
   location = {Berlin Heidelberg},
   isbn = {978-3-642-39175-0},
   pages = {81-98},
   publisher = {Springer},
   title = {Compositional Approach to Suspension and Other Improvements to LTL Translation},
   year = {2013}
}

TY  - JOUR
ID  - 1110031
AU  - Babiak, Tomáš - Badie, Thomas - Duret-Lutz, Alexandre - Křetínský, Mojmír - Strejček, Jan
PY  - 2013
TI  - Compositional Approach to Suspension and Other Improvements to LTL Translation
PB  - Springer
CY  - Berlin Heidelberg
SN  - 9783642391750
KW  - linear time logic
KW  - model-checking
KW  - translation LTL to Buchi automata
N2  - Recently, there was defined a fragment of LTL (containing fairness properties among other interesting formulae) whose validity over a given infinite word depends only on an arbitrary suffix of the word. Building upon an existing translation from LTL to Büchi automata, we introduce a compositional approach where subformulae of this fragment are translated separately from the rest of an input formula and the produced automata are composed in a way that the subformulae are checked only in relevant accepting strongly connected components of the final automaton. Further, we suggest improvements over some procedures commonly applied to generalized Büchi automata, namely over generalized acceptance simplification and over degeneralization. Finally we show how existing simulation-based reductions can be implemented in a signature-based framework in a way that improves the determinism of the automaton.
ER  -

BABIAK, Tomáš, Thomas BADIE, Alexandre DURET-LUTZ, Mojmír KŘETÍNSKÝ and Jan STREJČEK. Compositional Approach to Suspension and Other Improvements to LTL Translation. In Ezio Bartocci, C. R. Ramakrishnan. \textit{Model Checking Software - 20th International Symposium, SPIN 2013}. LNCS 7976. Berlin Heidelberg: Springer, 2013, p.~81-98. ISBN~978-3-642-39175-0. Available from: https://dx.doi.org/10.1007/978-3-642-39176-7\_{}6.

Detailed Information on Publication Record