Automated Model Revision for Coordinated Open Systems

Model checking, which can be represent as the paradigm "specifying→verifying", is an effective technology for automatic system verification. But model checking is generally used only to verify the correctness of a system, not to modify it. Sometimes this can be a major limitation. We propose a framework for ATL alpha beta model revision in this paper, study the computational complexity of its related problems, and show that the proposed framework consists with the minimal change principle in propositional belief update. By this paper, We extend the paradigm of ATL model checking to "specifying→verifying→revising" and establish the theoretical basis for automatic revising the strategic ability related properties of coordinated open systems.