On Boolean Encodings of Transition Relation for Parallel Compositions of Transition Systems.
Andrzej Zbrzezny · CS&P · 2013
We present and compare different Boolean encodings of the transition relation for the parallel composition of transition systems, both for the asynchronous and the synchronous semantics. We compare the encodings considered by applying them to the SAT-based bounded model checking (BMC) of ECTL∗ properties. We provide experimental results which show that our new encoding for the asynchronous semantics significantly increases the efficiency of the SATbased BMC.