Informační systém Masarykovy univerzity 

Compositional Approach to Suspension and Other Improvements to LTL Translation

česky | in English

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, 18 s. ISBN 978-3-642-39175-0. doi:10.1007/978-3-642-39176-7_6.
Další formáty:   BibTeX LaTeX RIS
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
Originální jazyk angličtina
Typ výsledku Článek ve sborníku
Obor Informatika
Stát vydavatele Spojené státy americké
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 0302-9743
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 formela-conference, linear time logic, Model-Checking
Příznaky Mezinárodní význam, Recenzováno
Změnil Změnil: doc. RNDr. Jan Strejček, Ph.D., učo 3366. Změněno: 15. 11. 2013 23:28.
Anotace
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 VaVNázev: Centrum excelence - Institut teoretické informatiky (CE-ITI) (Akronym: CE-ITI)
Investor: Grantová agentura ČR, Projekty na podporu excelence v základním výzkumu
MUNI/A/0739/2012, interní kód MUNázev: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity (Akronym: SKOMU)
Investor: Masarykova univerzita, Grantová agentura MU, Kategorie A - Specifický výzkum - Studentské výzkumné projekty
MUNI/A/0760/2012, interní kód MUNázev: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace II. (Akronym: FI MAV II.)
Investor: Masarykova univerzita, Grantová agentura MU, Kategorie A - Specifický výzkum - Studentské výzkumné projekty
VytisknoutZobrazeno: 17. 10. 2017 11:27

Relevantní odkazy 


Nahoru | Aktuální datum a čas: 17. 10. 2017 11:27, 42. (sudý) týden

Kontakty: istech(zavináč/atsign)fi(tečka/dot)muni(tečka/dot)cz, studijní odd., správci práv, is-technici, e-technici, IT podpora | Použití cookies | Více o Informačním systému