Checking Non-divergence, Channel-Bound and Global Cooperation Using SAT-Solvers

Divergence appears in message sequence chart specifications when an unbounded number of messages are pending within a communication channel. Several algorithms and tools have been already developed to detect this property. This paper explains why checking non-divergence is very close to the Boolean satisfiability problem and shows how SAT-solvers can be used to check this property efficiently. We show also how some other close properties can be checked similarly.