Improvements of Simulation-based Reduction

From LRDE

Abstract

In model checking using Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \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 Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle 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 Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle n} -step simulations. We also present how we can extend the existing reduction to make it work with alternating automata.