Coupling asynchrony and interrupts: Place Chart Nets and their synthesis

Abstract

This talk presents a model, called Place Chart Nets (PCN). 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 are a non-trivial generalization of classical Petri Nets (which can be viewed as concurrent FSMs), in the sense that (1) for the finite (bounded) case modeling a PCN may require an exponentially larger Petri net, (2) for the infinite (unbounded) case a class of PCN languages properly includes a class of Petri net languages and (3) k-boundedness of a sub-marking is decidable.

Then we present a method for synthesis of PCNs from transition systems, which generalizes the theory of regions previously developed for Petri nets. This technique allows one to extract concurrency and hierarchy hidden in the initial "flat" transition system.

Relevant Papers

Place Chart Nets and Their Synthesis