Verification of communication structured acyclic nets using SAT

Copyright \ua9 2021 for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0). 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