Translating synchronous Petri Nets into PROMELA for verifying behavioural properties Artigo de Conferência