Algorithms for Synthesizing Priorities in Component-based Systems

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.