A Tool for Model Checking Eventual Model Checking in a Stratified Way

We present a tool for model checking eventual properties in a stratified w ay t hat c an e ase t he n otorious s tate space explosion problem. As shown by the name, the tool is dedicated to eventual properties formalized as $\diamond\varphi$ where $\varphi$ is a state proposition. It is possible to formalize crucial requirements/properties that should be satisfied by a lot of software systems. For example, termination is such a requirement/property. Therefore, it is meaningful to concentrate on the properties. We also conduct some case studies showing that the state space explosion can be eased to a certain scope with the technique/tool.