Model Checking of $\omega$-Independent Unbounded Petri Nets for an Unbounded System

This work on model checking of unbounded Petri nets either not really concern the <inline-formula xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink"><tex-math notation="LaTeX">$\omega$</tex-math></inline-formula>-component or only focus on the <inline-formula xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink"><tex-math notation="LaTeX">$\omega$</tex-math></inline-formula> symbols, which may lead to incorrect judgments. This article proposes a model checking approach of <inline-formula xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink"><tex-math notation="LaTeX">$\omega$</tex-math></inline-formula>-independent unbounded Petri nets. First, this approach can ensure the complete state space required for model checking by analyzing the enabled/unenabled marking set of conditionally enabled transition. Second, a comprehensive model checking process of <inline-formula xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink"><tex-math notation="LaTeX">$\omega$</tex-math></inline-formula>-independent unbounded PN is presented, including the generation of extended new modified reachability graph. Third, two theorems are presented to prove that extended new modified reachability graph includes complete reachable markings and sequences of transitions. Finally, the proposed new approach is illustrated through a practical example.