Verification of conditional partial order graphs

The Conditional Partial Order Graph (CPOG) Model introduced recently is a novel technique for specification and synthesis of asynchronous controllers. It combines advantages of both Petri nets and FSM-based approaches and is capable of modelling systems with a high degree of concurrency and multiple choice. The paper extends the basic model of CPOGs to handle dynamic evaluation of internal control signals and introduces behavioural semantics for CPOGs. The extended model has a strong need for verification support, e.g. reachability analysis, deadlock detection etc. and this paper presents SAT-based characterisations for the most important CPOG verification problems.