Super-solutions: Succinctly representing solutions in abductive annotated probabilistic temporal logic

Annotated Probabilistic Temporal (APT) logic programs are a form of logic programs that allow users to state (or systems to automatically learn) rules of the form "formula G becomes true δt time units after formula F became true with ℓ to u% probability." In this article, we deal with abductive reasoning in APT logic: given an APT logic program Pi;, a set of formulas H that can be "added" to Π, and a (temporal) goal g, is there a subset S of H such that Pi; ? S is consistent and entails the goal g? In general, there are many different solutions to the problem and some of them can be highly repetitive, differing only in some unimportant temporal aspects. We propose a compact representation called super-solutions that succinctly represent sets of such solutions. Super-solutions are compact, but lossless representations of sets of such solutions. We study the complexity of existence of basic, super-, and maximal super-solutions as well as check if a set is a solution/super-solution/maximal super-solution. We then leverage a geometric characterization of the problem to suggest a set of pruning strategies and interesting properties that can be leveraged to make the search of basic and super-solutions more efficient. We propose correct sequential algorithms to find solutions and super-solutions. In addition, we develop parallel algorithms to find basic and super-solutions.