We propose to use the knowledge that an w-regular property is stutter insensitive to construct potentially smaller deterministic ω-automata for such a property, e.g. using Safra's determinization construction. This knowledge allows us to skip states that are redundant under stuttering, which can reduce the size of the generated automaton. In order to use this technique even for automata that are not completely insensitive to stuttering, we introduce the notion of partial stutter insensitiveness and apply our construction only on the subset of symbols for which stuttering is allowed. We evaluate the benefits of this heuristic in practice using multiple sets of benchmark formulas, © Springer-Verlag Berlin Heidelberg 2007.
CITATION STYLE
Klein, J., & Baier, C. (2007). On-the-fly stuttering in the construction of deterministic ω-automata. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4783 LNCS, pp. 51–61). Springer Verlag. https://doi.org/10.1007/978-3-540-76336-9_7
Mendeley helps you to discover research relevant for your work.