A modellellenőrzésről mint a formális verifikáció (más szóval a működés helyességének formális módszerekkel történő ellenőrzése/igazolása) egyik alapmódszeréről jegyzetünk részletesen ír az 5.2. fejezettől kezdődően. Itt az ellenőrizendő modellek a korábban (3.1. fejezet) megismert Kripke-struktúra vagy tranzíciós rendszer formájában adottak. Hogyan alkalmazható a modellellenőrzés Petri-háló alapú modellek vizsgálatára? A válasz triviális, ha a Petri-hálók elérhetőségi gráfjának és állapotterének kapcsolatára gondolunk: az elérhetőségi gráf a Petri-háló modell állapottere, ugyanakkor egy Kripke tranzíciós rendszerként is felfogható, amelyben az állapotokat a hozzájuk tartozó tokeneloszlás-vektorral címkézzük, az állapotátmeneteket pedig az ezeket kiváltó tüzelő tranzíciókkal. Így a Petri-háló modell verifikációját visszavezettük a háló elérhetőségi gráfjának mint Kripke tranzíciós rendszernek a modellellenőrzésére. Az ellenőrizendő tulajdonságokat pedig olyan temporális logikai kifejezésekkel tudjuk leírni, amelyek az állapotra (tehát a tokeneloszlás-vektor valamilyen jellemzőjére; pl.

search

a

search

helyen lévő tokenek száma) vagy az állapotátmenetre (pl.

search

tranzíció tüzelhető) vonatkoznak.