Domain learning is the task of inferring actions' preconditions and effects (domains) from executed sequences of actions (plans) along with a varying detail of information about the corresponding world states. Remarkably, even if the state remains completely unobserved, as in this work, we can infer the existence of certain state features if we assume that the plans we learn from are non-redundant. Moreover, plans might be redundant regardless of the underlying domain. We study the computational complexity of deciding whether there exists a domain in which a given plan is justified in the sense that either no single action (well-justification) or no set of actions (perfect justification) can be removed without violating correctness of the plan. We allow either arbitrarily large domains or domains with a polynomial bound on the number of state variables. We show that the problem is in P for well-justified plans and arbitrary domains, NP-complete for well-justified plans and bounded domains, in coNP for perfectly justified plans and arbitrary domains, and in Σ₂ for perfectly justified plans and bounded domains.

We introduce a new version of general game-playing in which one of the players chooses the length of the game up front. Consider a classical planning problem and two players who take turns applying actions. Player 1 wins iff the goal is true after a predetermined number of moves has been made. Is there a number r such that player 1 has a winning strategy for the game of length r? We show that this problem is EXPSPACE-complete. Moreover, we show that the problem is equivalent to the plan existence problem for a class of fully observable non-deterministic hierarchical task network planning problems under the solution concept with fixed methods, which was introduced in prior work. This class consists of all regular loop-unrolling problems, where a problem is loop-unrolling if it has at most one compound task name and at most two methods. As a corollary, we obtain hardness for regular problems, solving an open problem.

Both numeric planning and Hierarchical Task Network (HTN) planning are highly expressive planning formalisms – at the cost of being undecidable in general. For both formalisms, decidable fragments are known. Studying these restricted fragments has lead to valuable insights, which ultimately gave rise to the development of new efficient planning algorithms. We identify new decidable fragments of both numeric and HTN planning. For HTN planning, we introduce the fragments of one-hole-digging, initial, and final problems. The former restrict every task network to have at most one compound task, while the latter two restrict compound tasks to be order-minimal or order-maximal, respectively. For numeric planning, we introduce Positive Numeric Planning (PNP) where the value of numeric variables can only be non-negative. We determine the complexity of these fragments: they are Ackermann-complete – which is significantly more difficult than any prior known decidable fragment, but still barely decidable.

Abstract Automata operating on infinite objects feature prominently in the theory of the modal $$\mu $$ -calculus. One such application concerns the tableau games introduced by Niwiński & Walukiewicz, of which the winning condition for infinite plays can be naturally checked by a nondeterministic parity stream automaton. Inspired by work of Jungteerapanich and Stirling we show how determinization constructions of this automaton may be used to directly obtain proof systems for the $$\mu $$ -calculus. More concretely, we introduce a binary tree construction for determinizing nondeterministic parity stream automata. Using this construction we define the annotated cyclic proof system $$\textsf{BT}$$ , where formulas are annotated by tuples of binary strings. Soundness and Completeness of this system follow almost immediately from the correctness of the determinization method.