Efficient Trace Encodings of Bounded Synthesis for Asynchronous Distributed Systems

Hecking-Harbusch, Jesko and Metzger, Niklas
(2019) Efficient Trace Encodings of Bounded Synthesis for Asynchronous Distributed Systems.
In: UNSPECIFIED.
Conference: ATVA International Symposium on Automated Technology for Verification and Analysis

This is the latest version of this item.

[img]
Preview
Text
HM19.pdf

Download (338kB) | Preview
Official URL: https://doi.org/10.1007/978-3-030-31784-3_22

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.

Available Versions of this Item

  • Efficient Trace Encodings of Bounded Synthesis for Asynchronous Distributed Systems. (deposited 14 Sep 2020 07:28) [Currently Displayed]

Actions

Actions (login required)

View Item View Item