Revising Distributed UNITY Programs is NP-Complete; Technical rept

摘要

We focus on automated revision techniques for adding Unity properties to distributed programs. We show that unlike centralized programs where multiple safety properties and one progress property can be added in polynomial-time, addition of a safety or a progress Unity property to distributed programs is significantly more difficult. Precisely, we show that such addition is NP-complete in the size of the given program's state space. We also propose an efficient symbolic heuristic for addition of a leads-to property to distributed programs, which has applications in automated program synthesis.