Assume–Guarantee Distributed Synthesis
| Autor: | Damien Zufferey, Kaushik Mallik, Anne-Kathrin Schmuck, Rupak Majumdar |
|---|---|
| Rok vydání: | 2020 |
| Předmět: |
Mathematical optimization
Current (mathematics) Computer science Process (computing) Approximation algorithm 02 engineering and technology Computer Graphics and Computer-Aided Design 020202 computer hardware & architecture Reactive synthesis Control system 0202 electrical engineering electronic engineering information engineering Electronic design automation Electrical and Electronic Engineering Software |
| Zdroj: | IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems |
| ISSN: | 1937-4151 0278-0070 |
| DOI: | 10.1109/tcad.2020.3012641 |
| Popis: | Distributed reactive synthesis is the problem of algorithmically constructing controllers of distributed, communicating systems so that each closed-loop system satisfies a given temporal specification. We present an algorithm, called negotiation , for sound (but necessarily incomplete) distributed reactive synthesis based on assume–guarantee decompositions. The negotiation algorithm iteratively constructs assumptions and guarantees for each system. In each iteration, each system attempts to fulfill its specification and its guarantee (from the previous round), under the current assumption on the other systems, by solving a reactive synthesis problem. If the specification is not realizable, the algorithm computes a sufficient assumption on the other systems that ensures it can realize the specification and guarantee. This additional assumption further constrains the behavior of other systems and they might require an additional assumption, leading to the next round in the negotiation. The process terminates when a compatible assumption–guarantee pair is found for each system, which is sufficient to also satisfy the specification of each system. We have built a tool called Agnes that implements this algorithm. Using Agnes, we empirically demonstrate the effectiveness of our proposed algorithm on two case studies. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|