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.

Základní údaje

Originální název

Compositional Approach to Suspension and Other Improvements to LTL Translation

Autoři

BABIAK, Tomáš (703 Slovensko, domácí), Thomas BADIE (250 Francie), Alexandre DURET-LUTZ (250 Francie), Mojmír KŘETÍNSKÝ (203 Česká republika, domácí) a Jan STREJČEK (203 Česká republika, garant, domácí)

Vydání

LNCS 7976. Berlin Heidelberg, Model Checking Software - 20th International Symposium, SPIN 2013, od s. 81-98, 18 s. 2013

Nakladatel

Springer

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Spojené státy

Utajení

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

Forma vydání

tištěná verze "print"

Impakt faktor

Impact factor: 0.402 v roce 2005

Kód RIV

RIV/00216224:14330/13:00066141

Organizační jednotka

Fakulta informatiky

ISBN

978-3-642-39175-0

ISSN

DOI

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

Klíčová slova anglicky

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

Štítky

firank_B, formela-conference, linear time logic, Model-Checking

Příznaky

Mezinárodní význam, Recenzováno

Změněno: 15. 11. 2013 23:28, prof. RNDr. Jan Strejček, Ph.D.

Anotace

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.

Návaznosti

GBP202/12/G061, projekt VaV

Název: Centrum excelence - Institut teoretické informatiky (CE-ITI) (Akronym: CE-ITI)

Investor: Grantová agentura ČR, Centrum excelence - Institut teoretické informatiky

MUNI/A/0739/2012, interní kód MU

Název: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity (Akronym: SKOMU)

Investor: Masarykova univerzita, Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity, DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty

MUNI/A/0760/2012, interní kód MU

Název: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace II. (Akronym: FI MAV II.)

Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace II., DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty

Citovat

BABIAK, Tomáš, Thomas BADIE, Alexandre DURET-LUTZ, Mojmír KŘETÍNSKÝ a 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, s. 81-98. ISBN 978-3-642-39175-0. Dostupné z: 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Ý a 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, s.~81-98. ISBN~978-3-642-39175-0. Dostupné z: https://dx.doi.org/10.1007/978-3-642-39176-7\_{}6.

Podrobný výpis o publikaci