On the composition of time Petri nets
type: Item
instance of: scholarly article
title: On the composition of time Petri nets
zbMATH Open document ID: 1238.68101
author: Florent Peres
author: Bernard Berthomieu
author: François Vernadat
published in: Discrete Event Dynamic Systems
publication date: 2011-11-08T00:00:00Z
review text: The design and verification of concurrent and distributed systems, especially when their dynamic behaviour is time-dependent, is an intrinsically hard problem. One of conceptually elegant and efficient ways of dealing with this problem is to use a modular, or compositional, construction of such systems. Moreover, one also requires that the behaviour of a composite system can be derived from the behaviours of its components. Petri nets are a fundamental model of concurrent and distributed systems, and time Petri nets (TPN) allow one to express timing constrains of potential activities providing an adequate modelling framework for real time systems. In general, Petri nets support a compositional approach thanks to parallel composition and transition synchronisation. However, in presence of time, the method for assembling components based on transition synchronisation is not always compositional. Motivated by this observation, the paper addresses the following specific question: how to construct a concurrent system in a compositional manner from components specified by TPNs? This, in turn, leads to another question: given a TPN component, how can one transform it into an equivalent model where synchronised transitions are not time-dependent? The solution proposed in this paper is based on a new class of TPNs called forbid/allow TPNs (faTPNs). The ``forbid'' relation is similar to the priority relation, whereas the ``allow'' relation is in a way an inverse of priority. The class of faTPNs is then investigated and its general applicability discussed.
reviewed by: Maciej Koutny
Mathematics Subject Classification ID: 68Q85
Mathematics Subject Classification ID: 68Q60
Mathematics Subject Classification ID: 68Q55
Mathematics Subject Classification ID: 68N19
Mathematics Subject Classification ID: 68N30
Mathematics Subject Classification ID: 68M14
Mathematics Subject Classification ID: 68M15
zbMATH DE Number: 5969017
zbMATH Keywords: distributed system
zbMATH Keywords: concurrency
zbMATH Keywords: real time system
zbMATH Keywords: Petri net
zbMATH Keywords: compositionality
zbMATH Keywords: time Petri net
zbMATH Keywords: model transformation
describes a project that uses: TINA
MaRDI profile type: Publication
full work available at URL: s10626-011-0102-2
OpenAlex ID: W2024286707
cites work: Formal Modeling and Analysis of Timed Systems
cites work: Q4417948
cites work: The tool TINA – Construction of abstract state spaces for petri nets and time petri nets
cites work: Bridging the Gap Between Timed Automata and Bounded Time Petri Nets
cites work: Comparison of the Expressiveness of Arc, Place and Transition Time Petri Nets
cites work: Timed Petri Nets and Timed Automata: On the Discriminating Power of Zeno Sequences
cites work: Characterizing finite Kripke structures in propositional temporal logic
cites work: Computer Aided Verification
cites work: Recoverability of Communication Protocols--Implications of a Theoretical Study
cites work: Compositional specification of timed systems
DOI: 10.1007/S10626-011-0102-2
Recommended article: Q2766569
Recommended article: Q3474896
Recommended article: The expressive power of time Petri nets
Recommended article: Q4220896
Recommended article: Time and Petri Nets
Recommended article: Q3357558
Recommended article: Time Recursive Petri Nets
description: scientific article; zbMATH DE number 5969017