Verification of reactive system specifications with outer event conditional formula
Takenobu Aoshima, Naoki Yonezaki · 2002
We introduce an efficient tableau-based satisfiability checking procedure for a specification which consists of several modules. This method extracts reduced constraints from each module and verifies a property with them. We also show that this method is applicable to the decision procedure for strong satisfiability and stepwise satisfiability. Finally, we show the experimental results of the method.