Abstract interpretation of reactive systems : abstractions preserving $\forall$CTL*, $\exists$CTL* and CTL*
Dennis R. Dams, Orna Grümberg, RT Rob Gerth · TU/e Research Portal · 1994
The need for formal verification or systems on one h<lnd, and the advent of comp1ex reactive systems on the other, call for the development of automated verification techniques.Model checking is one such technique, which has proven quite successful.However, the state explosion problem remains thcstuJllbling block ,in m