Petri games: synthesis of distributed systems with causal memory

DOI10.1016/J.IC.2016.07.006zbMATH Open1362.68211arXiv1406.1069OpenAlexW1993831991MaRDI QIDQ515654FDOQ515654

Authors: Bernd Finkbeiner, Ernst-Rüdiger Olderog 

Publication date: 16 March 2017

Published in: Information and Computation (Search for Journal in Brave)

Abstract: We present a new multiplayer game model for the interaction and the flow of information in a distributed system. The players are tokens on a Petri net. As long as the players move in independent parts of the net, they do not know of each other; when they synchronize at a joint transition, each player gets informed of the causal history of the other player. We show that for Petri games with a single environment player and an arbitrary bounded number of system players, deciding the existence of a safety strategy for the system players is EXPTIME-complete.

Full work available at URL: https://arxiv.org/abs/1406.1069

Recommendations

• Petri games: synthesis of distributed systems with causal memory
• The synthesis problem for repeatedly communicating Petri games
• Bounded synthesis for Petri games
• High-level representation of benchmark families for Petri games
• scientific article; zbMATH DE number 7278100

zbMATH Keywords

causalitysynthesisPetri netsunfoldingstrategiescutsgraph games

Mathematics Subject Classification ID

Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Games involving graphs (91A43) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Cites Work

• Alternating-time temporal logic
• An \(O(n^2)\) time algorithm for alternating Büchi games
• Petri nets, event structures and domains. I
• Title not available (Why is that?)
• Provably Difficult Combinatorial Games
• Title not available (Why is that?)
• Branching processes of Petri nets
• Notes on finite asynchronous automata
• Unfoldings: A partial-order approach to model checking.
• FST TCS 2003: Foundations of Software Technology and Theoretical Computer Science
• Nets, Terms and Formulas
• Canonical prefixes of Petri net unfoldings
• Title not available (Why is that?)
• Process versus unfolding semantics for Place/Transition Petri nets
• Model checking using net unfoldings
• Distributed synthesis for acyclic architectures
• Bounded synthesis for Petri games
• Title not available (Why is that?)
• Petri games: synthesis of distributed systems with causal memory
• Title not available (Why is that?)
• Computer Science Logic
• Asynchronous Games over Tree Architectures
• FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
• FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science

Cited In (16)

• Title not available (Why is that?)
• Model checking data flows in concurrent network updates
• Canonical representations for direct generation of strategies in high-level Petri games
• Title not available (Why is that?)
• Solving high-level Petri games
• Bounded synthesis for Petri games
• High-level representation of benchmark families for Petri games
• Title not available (Why is that?)
• A two-player asynchronous game on fully observable Petri nets
• The synthesis problem for repeatedly communicating Petri games
• Distributed Asynchronous Games With Causal Memory are Undecidable
• Title not available (Why is that?)
• Efficient trace encodings of bounded synthesis for asynchronous distributed systems
• FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
• Petri games: synthesis of distributed systems with causal memory
• Implementable strategies for a two-player asynchronous game on Petri nets

Uses Software

• MCGP

This page was built for publication: Petri games: synthesis of distributed systems with causal memory

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q515654)