Efficient trace encodings of bounded synthesis for asynchronous distributed systems

DOI10.1007/978-3-030-31784-3_22MaRDI QIDQ3297600zbMATH OpenOpenAlexFDO

Authors Jesko Hecking-Harbusch, Niklas Metzger

Publication date 20 July 2020

Published in Automated Technology for Verification and Analysis (Search for Journal in Brave)

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

Mathematics Subject Classification ID

Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Abstract: The manual implementation of distributed systems is an error-prone task because of the asynchronous interplay of components and the environment. Bounded synthesis automatically generates an implementation for the specification of the distributed system if one exists. So far, bounded synthesis for distributed systems does not utilize their asynchronous nature. Instead, concurrent behavior of components is encoded by all interleavings and only then checked against the specification. We close this gap by identifying true concurrency in synthesis of asynchronous distributed systems represented as Petri games. This defines when several interleavings can be subsumed by one true concurrent trace. Thereby, fewer and shorter verification problems have to be solved in each iteration of the bounded synthesis algorithm. For Petri games, experimental results show that our implementation using true concurrency outperforms the implementation based on checking all interleavings.

Recommendations

• Compositional synthesis of asynchronous automata
• Synthesis of Asynchronous Systems
• Synthesis of distributed algorithms using asynchronous automata.
• Distributed Asynchronous Automata
• Effective synthesis of asynchronous systems from GR(1) specifications

Cites work

• Asynchronous Games over Tree Architectures
• Automated synthesis of distributed controllers
• Automated Technology for Verification and Analysis
• Bounded Synthesis
• Bounded synthesis for Petri games
• Canonical prefixes of Petri net unfoldings
• Distributed synthesis for acyclic architectures
• Dynamic partial-order reduction for model checking software
• Encodings of bounded synthesis
• FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
• FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science
• scientific article; zbMATH DE number 3885321 (Why is no real title available?)
• scientific article; zbMATH DE number 4124989 (Why is no real title available?)
• scientific article; zbMATH DE number 1337888 (Why is no real title available?)
• scientific article; zbMATH DE number 1927560 (Why is no real title available?)
• scientific article; zbMATH DE number 7278100 (Why is no real title available?)
• Non-prenex QBF solving using abstraction
• On the control of asynchronous automata
• Petri games: synthesis of distributed systems with causal memory
• Recent advances in unfolding technique
• Solving QBF by abstraction
• Translating asynchronous games for distributed synthesis
• Unbeast: Symbolic Bounded Synthesis
• Unfoldings: A partial-order approach to model checking.

Cited in

(4)

• A fully abstract trace model for dataflow and asynchronous networks
• Translating asynchronous games for distributed synthesis
• Information Flow Guided Synthesis
• Distributed controller synthesis for deadlock avoidance

Describes a project that uses

Uses Software

• Acacia+
• Unbeast

This page was built for publication: Efficient trace encodings of bounded synthesis for asynchronous distributed systems

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