compositionalityconcurrencydistributed systemmodel transformationPetri netreal time systemtime Petri net
Distributed systems (68M14) Reliability, testing and fault tolerance of networks and computer systems (68M15) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)
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.
- Bridging the Gap Between Timed Automata and Bounded Time Petri Nets
- Characterizing finite Kripke structures in propositional temporal logic
- Comparison of the Expressiveness of Arc, Place and Transition Time Petri Nets
- Compositional specification of timed systems
- Computer Aided Verification
- Formal Modeling and Analysis of Timed Systems
- scientific article; zbMATH DE number 1956600 (Why is no real title available?)
- Recoverability of Communication Protocols--Implications of a Theoretical Study
- The tool TINA – Construction of abstract state spaces for petri nets and time petri nets
- Timed Petri Nets and Timed Automata: On the Discriminating Power of Zeno Sequences
- A brief survey and synthesis of the roles of time in Petri nets.
- On persistency in time Petri nets
- scientific article; zbMATH DE number 1696462 (Why is no real title available?)
- Comparative trace semantics of time Petri nets
- scientific article; zbMATH DE number 2088660 (Why is no real title available?)
- scientific article; zbMATH DE number 2088661 (Why is no real title available?)
- scientific article; zbMATH DE number 1799524 (Why is no real title available?)
- Formalization of Petri nets with clocks
- scientific article; zbMATH DE number 4143457 (Why is no real title available?)
- On Multi-enabledness in Time Petri Nets
- Applications and Theory of Petri Nets 2004
- A compositional partial order semantics for Petri net components
This page was built for publication: On the composition of time Petri nets
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q645045)
