Occurrence net logics

• Autorzy: Haar S.
• Języki publikacji: EN

Abstrakty

EN

This paper investigates Occurrence (Petri) Nets on two levels: their structural theory and their interpretation in branching unfolding semantics of Petri Net systems. The key issue is the decomposition of occurrence nets into substructures given by the node relations associated with causal ordering, concurrency, and conflict. In addition to lines and cuts, which have long been studied in the context of causal nets, we introduce and study branches, trails, choices, and alternatives. All finite systems will be shown to satisfy certain density properties, i.e. non-empty intersections of substructures as above. On the semantic level, we introduce partial order logics to be interpreted on two different kind of frames, given by substructures of occurrence nets: on the frame of cuts, the CTL* type logics BFC and BLC, and the ``non-branching'' logic LLC, taylored to the frame given by the lattice of choices.

Słowa kluczowe

EN

concurrency; occurrence (Petri) nets; semantics; partial order logics

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2000
• Tom: Vol. 43, Nr 1-4
• Strony: 105--127
• Opis fizyczny: bibliogr. 20 poz.

Twórcy

autor

Haar S.

• Departément d'Informatique, Ecole Normale Supérieure, Paris, France,