Skip to main content

Revising Distributed UNITY Programs is NP-Complete

Publication Type
Year of Publication
2008
Conference/Journal Name
International Conference on Principles of Distributed Systems (OPODIS)
Publisher
Springer
Abstract
We focus on automated revision techniques for adding UNITY properties to distributed programs. We show that unlike centralized pro-
grams, 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 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.