We introduce on-the-fly composition, symbolic modelling and lazy iterated approximation refinement for game-semantic models. We present Mage, an experimental model checker implementing this new technology. We discuss several typical examples and compare Mage with BLAST and GameChecker, which are the state-of-the-art tools in on-the-fly software model checking, and game-based model checking.
展开▼
