Occurrence Net Logics

Stefan Haar 1
1 TRIO - Real time and interoperability
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : This paper investigates structural properties of occurrence (Petri) nets and their interpretation as unfolding semantics of Petri net systems. Occurrence nets (ONs) exhibit three kinds of node relations associated with causal ordering, concurrency, and conflict. We show that ONs can be decomposed in a natural way into substructures in each of which one or two of these relations are empty, namely: branches, trails, choices, lines, cuts and alternatives. All finite systems will be shown to satisfy certain density properties, i.e. non-empty intersections of substructures as above. Two unfolding semantics are studied: branching processes (introduced by Engelfriet, Wynskel et al.) and branching executions (Vogler). We present two partial order logics that can be interpreted over occurrence net semantics of either kind: the branching time logic BLC and a non-branching logic LLC whose frame is composed of choices, i.e. objects representing horizons of mutually exclusive global states compatible with the corresponding stage of the system.
Type de document :
Communication dans un congrès
Workshop Concurrency, Specification & Programming - CS & P'99, 1999, Varsovie/Pologne, 12 p, 1999
Liste complète des métadonnées

https://hal.inria.fr/inria-00098861
Contributeur : Publications Loria <>
Soumis le : mardi 26 septembre 2006 - 08:39:25
Dernière modification le : jeudi 11 janvier 2018 - 06:20:05

Identifiants

  • HAL Id : inria-00098861, version 1

Collections

Citation

Stefan Haar. Occurrence Net Logics. Workshop Concurrency, Specification & Programming - CS & P'99, 1999, Varsovie/Pologne, 12 p, 1999. 〈inria-00098861〉

Partager

Métriques

Consultations de la notice

154