Skip to main content

Complexity Results in Revising UNITY Programs

Publication Type
Year of Publication
Conference/Journal Name
ACM Transactions on Autonomous and Adaptive Systems (TAAS)
We concentrate on automatic revision of untimed and real-time programs with respect to UNITY properties. The main focus of this paper is to identify instances where addition of UNITY properties can be achieved efficiently (in polynomial-time) and where the problem of
adding UNITY properties is difficult (NP-complete). Regarding efficient revision, we present a sound and complete algorithm that adds a single leads-to property (respectively, bounded-time leads-to property) and a conjunction of unless, stable, and invariant properties (respectively, bounded-time unless and stable) to an existing untimed (respectively, real-time) UNITY program in polynomial-time in the state space (respectively, region graph) of the given program. Regarding hardness results, we show that (1) while one leads-to (respectively, ensures) property can be added in polynomial-time, the problem of adding two such properties (or any combination of
leads-to and ensures) is NP-complete, (2) if maximum non-determinism is desired then the problem of adding even a single leads-to property is NP-complete, and (3) the problem of providing maximum non-determinism while adding a single bounded-time leads-to property to a real-time program is NP-complete (in the size of the program’s region graph) even if the original program satisfies the corresponding unbounded leads-to property.