Revising Distributed UNITY Programs Is NP-Complete
Borzoo Bonakdarpour and Sandeep S. Kulkarni
Abstract
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.
Paper:
Return to the publication list
Return to the Sandeep's home page