Distributed Priority Synthesis
Chih-Hong Cheng (Fortiss GmbH), Rongjie Yan (ISCAS), Saddek Bensalem, (Verimag), Harald Ruess (Fortiss GmbH)

TL;DR
This paper introduces a formal approach for synthesizing distributed priorities in component-based systems to ensure safety, utilizing game-theoretic analysis, optimizations, and SAT solving, validated through case studies.
Contribution
It presents a novel formal framework for distributed priority synthesis using multi-player safety games, with optimized algorithms integrated into the VissBIP tool.
Findings
Effective algorithms for distributed priority synthesis
Successful validation on scheduling and robotics case studies
Enhanced scalability through diagnosis and SAT-based optimizations
Abstract
Given a set of interacting components with non-deterministic variable update and given safety requirements, the goal of priority synthesis is to restrict, by means of priorities, the set of possible interactions in such a way as to guarantee the given safety conditions for all possible runs. In distributed priority synthesis we are interested in obtaining local sets of priorities, which are deployed in terms of local component controllers sharing intended next moves between components in local neighborhoods only. These possible communication paths between local controllers are specified by means of a communication architecture. We formally define the problem of distributed priority synthesis in terms of a multi-player safety game between players for (angelically) selecting the next transition of the components and an environment for (demonically) updating uncontrollable variables. We…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
