Transition Systems of Elementary Net Systems with Localities Technical report series

摘要

In this paper, we investigate transition systems of a class of Petri nets suitable for the modeling and behavioral analysis of globally asynchronous locally synchronous (GALS) systems. The considered model of Elementary Net Systems with Localities (ENL-systems) is basically that of Elementary Net Systems (EN-systems) equipped with an explicit notion of locality. Each locality identifies a distinct set of events which may only be executed synchronously, i.e., in a maximally concurrent manner. For this reason, the overall behavior of an ENL-system cannot be represented by an interleaved transition system, with arcs being labeled by single events, but rather by a suitable notion of a step transition system, with arcs being labeled by sets of events executed concurrently.