(2019) Efficient Trace Encodings of Bounded Synthesis for Asynchronous Distributed Systems.
This is the latest version of this item.
|
Text
HM19.pdf Download (338kB) | Preview |
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.
| Item Type: | Conference or Workshop Item (A Paper) (UNSPECIFIED) |
|---|---|
| Conference: | ATVA International Symposium on Automated Technology for Verification and Analysis |
| Depositing User: | Jesko Hecking-Harbusch |
| Date Deposited: | 14 Sep 2020 07:28 |
| Last Modified: | 14 Sep 2020 10:51 |
| Primary Research Area: | NRA2: Reliable Security Guarantees |
| URI: | https://publications.cispa.saarland/id/eprint/3180 |
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 |