Modal logic applied to events graph

The objective of this paper is to show how we can apply modal logic, named NK-logical system, to events graphs (particularly class of Petri nets). Those events graphs logical models are applied in turn to the verification of specification of discrete event dynamic systems. Given a specification (a description of a certain system constraint), we are able to use tools taken from the NK-logical system (especially analytic tableau) to verify if the specification is satisfiable or not in the modeled system. After showing notions of events graph, NK-logical system and the relation between them, we present in the end a simple example. Our aim is to explain the events graph modeling process in a direct way rather than through many proofs. We hope with this that beginners will be able to get some knowledge on logic and events-graph related matters.