以自動機理論發展之最小模型修復技術

Abstract

We combine the graph theory and the automaton theory for a general research framework of automatic system repair. This new framework not only allows us to analyze all system repairs expressible with B‥uchi automata but also can help us telling‘economic’repairs from‘expensive’repairs. Three criteria for model repair are proposed: repair for language containment, repair for language equivalence, and repair for bisimulation equivalence. We borrow the concept of graph-edit distance in the graph theory to define the repair cost for a system automaton. We establish the complexities of the problems of finding correct model repairs with minimum cost with the three criteria. We then present an algorithm that uses a breadth first approach to explore the repair space to solve the problem for a repair criterion. We also present a heuristic algorithm for bisimulation. Finally, we report our experiment that checks the performance of our algorithms.