2011/07/06 by Chih‐Hong Cheng, Cheng, Chih-Hong, Saddek Bensalem +13
Computer Science · #FOS: Computer and information sciences #FOS: Electrical engineering #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Petri Nets in System Modeling #Software Reliability and Analysis Research #Systems and Control (eess.SY) #electronic engineering #information engineering
paper · pdf · doi:10.48550/arxiv.1107.1383
openalex publication_date 2011/07/06 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.