Methods of Translation of Petri Nets to NuSMV Language.
Marcin Szpyrka, Agnieszka Biernacka, Jerzy Biernacki · 2014
Abstract. The paper deals with the problem of translation of reachability graphs for place-transition and coloured Petri nets into the NuSMV language. The trans-lation algorithms presented in the paper have been implemented as a part of the PetriNet2NuSMV tool so the translation is made automatically. The PetriNet2Nu-SMV tool works with reachability graphs generated by the TINA and CPN Tools software. Thus, it provides the possibility of formal verification of Petri nets de-signed with these environments using model checking techniques and a main-stream model checker for LTL and CTL temporal logics.