Project Details

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

Project Period: 1. 1. 1998 - 31. 12. 1998

Project Type: grant

Code: FEI-98-?

Agency: Faculty of Electrical Engineering and Computer Science BUT

Program:

English title
Verifying Temporal Properties of Models Based on Object-Oriented Petri Nets
Type
grant
Keywords

Object-oriented Petri nets, temporal logics, model checking, state space explosion

Abstract

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.

Team members
Vojnar Tomáš, Ing., Ph.D. (UIVT FEI VUT) , research leader
Publications

1998

Back to top