Ověřování temporálních vlastností modelů popsaných objektově orientovanými Petriho sítěmi

The goal of this project is to allow model checking of temporal formulae over
models described by OOPNs. To achieve this goal, it is necessary to define the
notion of the name abstracted state space of OOPNs, to propose a suitable
temporal logic for specifying properties of OOPN based models, and to develop
some model checking procedure for checking validity of formulae of this logic. It
is also unavoidable to fight against the state explosion problem in some way.
Here, it is supposed that we will be able to modify methods known from the area
of coloured Petri nets and make them work also in the context of the more
dynamical OOPNs.