A new symbolic model checker for the analysis of synchronous finite-state and infinite-state systems