• A
  • A
  • A
  • АБB
  • АБB
  • АБB
  • А
  • А
  • А
  • А
  • А
Обычная версия сайта

Глава

Petri nets behavioral equivalence checking in SMV

Drozdov D., Dubinin V., Kulagin V.

This paper proposes an approach to k-bounded Petri nets behavioral equivalence checking using the model checking method and mainstream verifier nuSMV. For the comparison of behavior of two nets, an add-in net is introduced which performs a supervisory control of these two nets. The approach uses an implicit word-to-word comparison of labeled Petri net languages with invisible transitions when computing CTL temporal logic formulas. The technique of Petri nets equivalence checking in SMV is briefly discussed followed by a simple case study.