Skip to main content

Revising UNITY Programs: Possibilities and Limitations

Publication Type
Year of Publication
Conference/Journal Name
International Conference on Principles of Distributed Systems (OPODIS)
We concentrate on automatic addition of UNITY properties unless, stable, invariant, and leads-to to programs. We formally define the
problem of adding UNITY properties to programs while preserving their existing properties. For cases where one simultaneously adds a single leads-to property along with a conjunction of unless, stable, and invariant properties to an existing program, we present a sound and complete algorithm with polynomial time complexity (in program state space). However, for cases where one simultaneously adds two leads-to properties to a program, we present a somewhat unexpected result that such addition is NP-complete. Therefore, in general, adding one leads-to property is significantly easier than adding two (or more) leads-to properties.