Temporální vlastnosti modelů popsaných objektově orientovanými Petriho sítěmi

This project is based on a research in the area of formal analysis and
verification over models described by object-oriented Petri nets (OOPNs)
associated to the tool called PNtalk. This research includes proposing a suitable
specification language for specifying desired properties of systems modelled by
OOPNs and methods of verifying them via state spaces of OOPNs in an as effective
as possible way. The project is mostly theoretical, however, at least some of the
obtained theoretical proposals will be checked via a prototype implementation in
Prolog.