Model checking is a system validation technique: given a model of the system ("how we think it behaves") and a specification of the property
to be considered ("how we want it to behave"), model checking is a technique that systematically checks the validity of the property in the model.
DSPN is a graphical method for the modeling of discrete-event systems like computer architectures, communication systems, 
and manufacturing systems, where events may occur either without consuming time, after a deterministic time, or after an exponentially distributed time.
In this presentation we will show our current research in the application and extension of model checking techniques
(previously developed for Markov chains) to DSPNs, in order to check properties specified using this formalism.