Revising Distributed UNITY Programs Is NP-Complete

Borzoo Bonakdarpour and Sandeep S. Kulkarni


We focus on automated revision techniques for adding \textsc{Unity} properties to distributed programs. We show that unlike centralized programs, where multiple safety properties along with one progress property can be simultaneously added in polynomial-time, addition of only one safety or one progress property to distributed programs is NP-complete. We also propose an efficient symbolic heuristic for adding a \textsf{leads-to} property to a distributed program. We demonstrate the application of this heuristic in automated synthesis of recovery paths in fault-tolerant distributed programs.


Return to the publication list
Return to the Sandeep's home page