Abstract | ||
---|---|---|
We propose to use the knowledge that an !-regular prop- erty is stutter insensitive to construct potentially smaller deterministic !-automata for such a property, e.g. using Safra's determinization con- struction. 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 insen- sitiveness 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. |
Year | DOI | Venue |
---|---|---|
2007 | 10.1007/978-3-540-76336-9_7 | CIAA |
Keywords | DocType | Citations |
determinization,stuttering,ltl,rabin,ω- automaton.,deterministic | Conference | 0 |
PageRank | References | Authors |
0.34 | 16 | 2 |
Name | Order | Citations | PageRank |
---|---|---|---|
Joachim Klein | 1 | 118 | 9.33 |
Christel Baier | 2 | 3053 | 185.85 |