Why Not Model Checking?




State-space explosion
More importantly, some states may be hidden