This paper presents a symbolic verification approach that models a CPS whose requirements are specified using ECA rules into a Petri net. The PN is then given as input to the model checking tool SMART for the verification of several properties. In this work, we provide algorithms to verify the termination and the confluence properties.