Practical symbolic model checking of the full µ-calculus using compositional abstractions
Peter Kelb, Dennis R. Dams, RT Rob Gerth · TU/e Research Portal · 1995
We apply abstract interpretation techniques to reduce the time and space requirements for model checking the full J-l-calculus over parallel processes.The abstractions can be computed compositionally.The techniques have been implemented in a StateCharts model checker.Experiments show a 17-fold reduction on the average in the size of the BDDs on non-trivial specifications.