Minimal specification revision for weighted transition systems

In this paper, we study the problem of revising Linear Temporal Logic (LTL) formulas that capture specifications for optimal planning over weighted transition systems. Namely, it is assumed that the model of the system is a weighted finite state transition system. The LTL specification captures the system requirements which must be satisfied by a plan which costs less than a certain cost budget. If the cost bounds cannot be satisfied with the initial specification, then it is desirable to return to the user a specification that can be satisfied on the system within the desired cost budget. We prove that the specification revision problem for automata-based optimal planning is NP-complete. In order to provide exact solutions to the problem, we present an Integer Linear Program (ILP) and a Mixed-Integer Linear Program (MILP) formulation for different versions of the problem. Finally, we indicate that a Linear Program (LP) relaxation can compute fast approximations to the problem.