Verification of communication structured acyclic nets using SAT

Model checking is an established strategy for automatic verification of software and hardware systems. It supports extensive analyses of the properties of states and behaviours of computing systems. Petri net verification using SAT-solvers has already received considerable attention and effective tools based on it have been developed. In this paper, we are concerned with the verification of communication structured acyclic nets (CSA-nets) which so far lacked robust verification methodology. CSA-nets are sets of acyclic nets which can communicate by means of synchronous and asynchronous interactions. In this paper, we introduce several propositional formulas which can be used to verify properties of CSA-nets using SAT-solvers.