A Symbolic Algorithm for Shortest EG Witness Generation

Witness generation is a fundamental model checker feature, but generating shortest witnesses for an EG CTL formula has long been a difficult problem of both theoretical and practical relevance. We propose a symbolic approach to shortest EG witness generation based on edge-valued multi-way decision diagrams. We employ a fix point symbolic iteration to compute the transitive closure enhanced with distance information, using the saturation algorithm to cope with the high computational complexity of this approach. We also extend this approach to tackling the shortest witness generation for other properties and the shortest fair witness generation. Experimental results show that our approach can generate a shortest witness which could not be found within acceptable time using previous algorithms.