Résumé | Inclusion checking is a central algorithmic problem in the theory of automata, with important applications, e.g., in formal methods.
The problem is PSPACE-complete, thus under standard complexity-theoretic assumptions no deterministic algorithm with worst case polynomial time can be expected.
We optimize the so-called Ramsey-based approach to inclusion checking.
In this approach, one explores a semigroup of exponential size for a counter-example to inclusion.
The exploration starts from a small set of generators, and all elements of the semigroup are progressively computed by composition.
On the way, a test operation is used to check for counter-examples.
The exploration stops if a counter-example is found; otherwise, all elements are generated.
Clearly, exhaustive exploration of the semigroup is in general infeasible, due to its exponential size.
We show how coarse simulation-based subsumption preorders between elements of the semigroup can be designed,
allowing one to prune away significant parts of the search space.
Subsumption allows us to solve inclusion checking for automata with thousand states, which was unthinkable before.
More details can be found on http://www.languageinclusion.org/. |