A near-optimal method for reasoning about action

摘要

We give an algorithm for “before-after” reasoning about action. The algorithm decides satisfiability and validity of formulas of propositional dynamic logic, a recently developed logic of change of state that subsumes the zero-order component of most other action-oriented logics. The algorithm requires time at most proportional to an exponentially growing function of the length (number of occurrences of variables and connectives) of the input. Fischer and Ladner have shown that that every algorithm for this problem must take exponential time, making this algorithm optimal to within a polynomial. Application areas include program verification, program synthesis, and discourse analysis. The algorithm is based on the method of semantic tableaux, appropriately generalized to dynamic logic. A formal treatment of the generalization, called Hintikka structures, is developed.