Global State Checker: Towards SAT-Based Reachability Analysis of Communicating State Machines
Petra Radeljak Kaufmann, Martin Kronegger, Andreas Pfandler, Martina Seidl, Magdalena Widl · 2013
We present a novel propositional encoding for the reachability problem of communicating state machines. The problem deals with the question whether there is a path to some combination of states in a state machine view starting from a given configuration. Reachability analysis finds its application in many verification scenarios. By using an encoding inspired by approaches to encode planning problems in artificial intelligence, we obtain a compact representation of the reachability problem in propositional logic. We present the formal framework for our encoding and a prototype implementation. A first case study underpins its effectiveness.