Cílem projektu je umožnit ověřování vlastností systémů vyjádřených ve vhodné temporální logice na modelech vytvořených pomocí objektově orientovaných Petriho sítí, které jsou úzce spojeny s jazykem PNtalk. Řešení projektu bude probíhat zejména v rovině teoretické, přesto by mělo dojít k alespoň pokusné implementaci některých myšlenek v jazyce Prolog.

Popis anglicky
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.

Klíčová slova
Objektově orientované Petriho sítě, temporální logiky, model checking, exploze stavového prostoru

Klíčová slova anglicky
Object-oriented Petri nets, temporal logics, model checking, state space explosion

FEI-98-?

čeština

Vojnar Tomáš, prof. Ing., Ph.D. - hlavní řešitel

Ústav inteligentních systémů
- odpovědné pracoviště (23.10.2001 - nezadáno)
Výzkumná skupina automatizované analýzy a verifikace - VeriFIT
- interní (23.10.2001 - 31.12.1998)
Výzkumná skupina Petriho sítí
- interní (23.10.2001 - 31.12.1998)
Fakulta informačních technologií
- spolupříjemce (23.10.2001 - 31.12.1998)

Odpovědnost: Vojnar Tomáš, prof. Ing., Ph.D.