CONTEXT-DEPENDENTMINIMIZATION OF STATE/EVENT SYSTEMS
Gerd Behrmann, Kåre J. Kristoffersen, Kim G. Larsen · Proceedings of the Estonian Academy of Sciences Physics Mathematics · 1998
This paper presents a technique for efficient checking of reachability properties of concurrent state/event systems.The technique improves the traditional algorithm for the forwards exploration of the global state space by the incremental construction of subsystems kept small using a context-dependent minimization.A tool has been implemented to verify state/event systems.Experimental results report on a feasible automatic verification of the correctness of Milner's scheduler -an often used benchmark -with 100 cells.This result dramatically improves the previous best results for this benchmark.Moreover, our technique has proved well applicable to industrial designs of sizes up to 400 concurrent state machines.