On-the-Fly Stuttering in the Construction of Deterministic $ømega$-Automata

Joachim KleinJoachim Klein, Christel BaierChristel Baier

DOI Link

Joachim Klein, Christel Baier
On-the-Fly Stuttering in the Construction of Deterministic $ømega$-Automata
Proc. of the 12th International Conference on Implementation and Application of Automata (CIAA), volume 4783 of Lecture Notes in Computer Science, 51--61, 2007. Springer

Details
Bibtex

KurzfassungAbstract
We propose to use the knowledge that an ω-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.
Forschungsgruppe:Research Group: Algebraische und logische Grundlagen der InformatikAlgebraic and Logical Foundations of Computer Science

The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-540-76336-9_7.

@inproceedings{KB2007,
  author    = {Joachim Klein and Christel Baier},
  title     = {On-the-Fly Stuttering in the Construction of Deterministic
               ${\o}mega$-Automata},
  booktitle = {Proc. of the 12th International Conference on Implementation and
               Application of Automata (CIAA)},
  series    = {Lecture Notes in Computer Science},
  volume    = {4783},
  publisher = {Springer},
  year      = {2007},
  pages     = {51--61},
  doi       = {10.1007/978-3-540-76336-9_7}
}