Coupling asynchrony and interrupts: Place chart nets

Abstract

A model, called Place Chart Nets (PCN), is presented. It allows the modeling of both asynchronicity and exception handling (preemption). Contrary to State Charts and other reactive models, which are inherently synchronous, PCNs specify a system behavior using partial orders. Contrary to Petri nets, PCNs have a notion of hierarchy. Contrary to other hierarchical models based on Petri net extensions, the hierarchy in PCNs is determined by preemption. We show that PCNs axe a non-trivial generalization of classical PNs, in the sense that (1) for the finite (bounded) case modeling a PCN may require an exponentially larger PN, (2) for the infinite (unbounded) case the class of PCN languages properly inchdes the class of PN languages and (3) boundedness of PCNs is decidable. Then we present synthesis of safe PCNs from transition systems, which generalizes the theory of regions previously developed for PNs.