Other formats:
BibTeX
LaTeX
RIS
@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.
|