Revising Distributed UNITY Programs Is NP-Complete

We focus on automated revision techniques for adding 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 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.

• Type: Conference
• Year: 2008
• Where: OPODIS
• Authors: Borzoo Bonakdarpour, Sandeep S. Kulkarni
• Keywords: Distributed And Parallel Computing, Distributed Programs, Multiple Safety Properties, OPODIS 2008, Progress Property