The simulation relation on finite state transition systems can be verified automatically by the Milner's method. In the case that systems have infinite many states, the verification can be completed by the deductive methods like Pnueli's. Though, they are hard to be done automatically. In the paper, we propose the idea of methods that can verify several properties on infinite-state systems automatically, based on Sipma's deductive model checking.
展开▼
