Compositional synthesis of live and bounded free choice Petri nets

Javier Esparza, Manuel Silva

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

17 Scopus citations

Abstract

The paper defines two notions of composition of concurrent modules modelled by means of Petri nets: synchronisations and fusions. We study these two notions for the class of Free Choice nets, and characterise the compositions (within this class) that preserve liveness (absence of partial or global deadlocks) and boundedness (absence of overflows in finite stores). The characterisation shows which structures must be avoided in order to preserve the properties.

Original languageEnglish
Title of host publicationCONCUR 1991 - 2nd International Conference on Concurrency Theory, Proceedings
EditorsJos C.M. Baeten, Jos C.M. Baeten, Jan Frisco Groote
PublisherSpringer Verlag
Pages172-187
Number of pages16
ISBN (Print)9783540544302
DOIs
StatePublished - 1991
Externally publishedYes
Event2nd International Conference on Concurrency Theory, CONCUR 1991 - Amsterdam, Netherlands
Duration: 26 Aug 199129 Aug 1991

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume527 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference2nd International Conference on Concurrency Theory, CONCUR 1991
Country/TerritoryNetherlands
CityAmsterdam
Period26/08/9129/08/91

Keywords

  • Boundedness
  • Compositional synthesis
  • Free choice nets
  • Liveness
  • Petri nets

Fingerprint

Dive into the research topics of 'Compositional synthesis of live and bounded free choice Petri nets'. Together they form a unique fingerprint.

Cite this