Algorithms for Synthesizing Priorities in Component-based Systems
Chih-Hong Cheng, Saddek Bensalem, Yu-Fang Chen, Rongjie Yan, Barbara, Jobstmann, Harald Ruess, Christian Buckl, Alois Knoll

TL;DR
This paper introduces algorithms for synthesizing safe, deadlock-free component-based systems using priorities, combining fault localization and repair techniques, with preprocessing methods to handle complex systems efficiently.
Contribution
It presents novel algorithms that integrate safety-game-based fault localization, SAT-based conflict resolution, and preprocessing techniques for scalable priority synthesis in complex systems.
Findings
Effective algorithms for priority synthesis ensuring safety and deadlock-freedom.
Preprocessing methods significantly improve scalability for complex systems.
Demonstrated success in synthesizing priorities in component-based systems.
Abstract
We present algorithms to synthesize component-based systems that are safe and deadlock-free using priorities, which define stateless-precedence between enabled actions. Our core method combines the concept of fault-localization (using safety-game) and fault-repair (using SAT for conflict resolution). For complex systems, we propose three complementary methods as preprocessing steps for priority synthesis, namely (a) data abstraction to reduce component complexities, (b) alphabet abstraction and #-deadlock to ignore components, and (c) automated assumption learning for compositional priority synthesis.
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.
Taxonomy
TopicsFormal Methods in Verification · Software Reliability and Analysis Research · Petri Nets in System Modeling
