Elements of distributed algorithms. Modeling and analysis with Petri nets
The book presents a large variety of distributed algorithms using a Petri net based technique. The correctness of these algorithms is provided by means of temporal logic. The text is divided into four main parts. Part A consists of two chapters. The first one introduces some elementary concepts: local states and actions, interleaved and concurrent runs, the assumption of progress and fairness. The second one concentrates on modelling, with the introduced concepts, for various distributed algorithms (sequential and parallel buffers, the dinning philosophers, an asynchronous stack, the crosstalk problem, mutual exclusion problems, distributed testing of message lines). Part B contains chapters III to VI. The third one introduces the system nets as a generalisation of the elementary system nets. Various distributed algorithms, modelled as system nets (producer/consumer, dinning philosophers problem, asynchronous stack, the paradigm of constraint programming, variants of mutual exclusion behaviour, rearrangement problem), are presented in the fourth chapter. The fifth chapter deals with problems occurring in networks of communicating agents. So, distributed algorithms for detecting loss of messages and enforcing copies of lost messages to neighboring receivers in network, are presented. Finally, the case of a master process obtaining acknowledgements or refusals from a set of slave process, is investigated. The sixth chapter presents some network algorithms (leader election and spanning trees, the echo algorithm, mutual exclusion algorithms in networks, algorithms about some contract or agreement among sites of a network, synchronization mechanisms, distributed self stabilization). Part C contains chapters VII to IX and deals with the analysis of some properties for elementary system models. In the seventh chapter some state properties, including place invariants and initialized traps, are defined for elementary system nets. Some case studies are provided in this respect. The eigth and the nineth chapters introduce progress properties based on interleaved runs as well as on concurrent runs. Part D covers chapters X to XIII and in analogy to the analysis of elementary system nets, considers state properties (in the tenth chapter) and progress properties (chapters XI and XII) for system nets. In the last chapter the case studies developed in part B (chapters IV, V and VI) are reconsidered and formally verified. The book provides a very useful support for university courses in the area of distributed algorithms.
- Petri nets. Theoretical models and analysis methods for concurrent systems
- scientific article; zbMATH DE number 51631
- scientific article; zbMATH DE number 3890722
- scientific article; zbMATH DE number 4045167
- Nested Petri nets: modeling and analysis of distributed systems with object structure
- Petri net based verification of distributed algorithms: An example
- scientific article; zbMATH DE number 1173911
- scientific article; zbMATH DE number 2020760
- Petri net based verification of distributed algorithms: An example
- Further results on generalised communicating P systems
- Abstract state machines: a unifying view of models of computation and of system design frameworks
- On stubborn sets in the verification of linear time temporal properties
- Possible worlds and resources: The semantics of \(\mathbf{BI}\)
- Plan coordination by revision in collective agent based systems.
- Modal algebra and Petri nets
- Observable liveness of Petri nets
- Implementing dataflow with threads
- Keep it fair: equivalence and composition
- Petri net reactive modules
- On Distributability of Petri Nets
- A Distributed Computing Model for Dataflow, Controlflow, and Workflow in Fractionated Cyber-Physical Systems
- Oclets – Scenario-Based Modeling with Petri Nets
- Modeling and simulation of distributed systems. With CD-ROM
- Verification of distributed algorithms with algebraic Petri nets
- Distributed Control of Discrete-Event Systems: A First Step
- Representation and Execution of Petri Nets Using Rewriting Logic as a Unifying Framework
- Petri games: synthesis of distributed systems with causal memory
- The 4C Spectrum of Fundamental Behavioral Relations for Concurrent Systems
- Graph-based communication in Eden
- Partially ordered knowledge sharing and fractionated systems in the context of other models for distributed computing
- A Hybrid Approach to Modeling Biological Systems
- Encoding the dynamics of deterministic systems
- ESTL: A Temporal Logic for Events and States
- Relational structures model of concurrency
This page was built for publication: Elements of distributed algorithms. Modeling and analysis with Petri nets
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4372017)
