Revising Distributed UNITY Programs is NP-Complete
MICHIGAN STATE UNIV EAST LANSING DEPT OF COMPUTER SCIENCE/ENGINEERING
Pagination or Media Count:
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 programs 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.
- Computer Programming and Software