Improvements of Simulation-based Reduction

Authors

Laurent Xu

Type

techreport

Year

2017

Number

1706

Abstract

In model checking using $\omega$-automata, the construction of smaller automata reduces a lot the runtime and the memory consumption of costly operations such as the synchronized product. As the minimization of deterministic Büchi automata is an NP-complete problem, we focus our work on reduction operations. Spot already implements a method of reduction by simulation working with all existential automata with any type of acceptance. This method uses a one-step simulation based on the signatures of the states. L. Clemente and R. Mayr propose a reduction by $n$-step simulation only working with Büchi automata and show that increasing this number of steps may improve the reduction. We try to generalize the existing reduction operation in Spot to make it work with signature-based $n$-step simulations. We also present how we can extend the existing reduction to make it work with alternating automata.