LTL model checking of colored Petri nets based on net unfoldings
LTL model checking of colored Petri nets based on net unfoldings
Summary: The model-checking algorithm from [\textit{F. Wallner}, Lect. Notes Comput. Sci. 939, 207-218 (1998)] is adapted to colored Petri nets (CPN) [\textit{K. Jensen}, Colored Petri nets. Basic concepts, analysis methods and practical use, Vol. 2, Springer-Verlag, Berlin (1995; Zbl 0865.68084)]. A state-based semantics of LTL for CPN is given and correctness is proven of the approach proposed. It is also shown how to apply this model checking technique to interval-timed CPN.
LTL semantics, Specification and verification (program logics, model checking, etc.), net unfolding, Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.), Semantics in the theory of computing, colored Petri nets, model-checking algorithm
LTL semantics, Specification and verification (program logics, model checking, etc.), net unfolding, Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.), Semantics in the theory of computing, colored Petri nets, model-checking algorithm