Generalised planning (GP) refers to the task of synthesising programs that solve families of related planning problems. We introduce a novel, yet simple method for GP: given a set of training problems, for each problem, compute an optimal plan for each goal atom in some order, perform goal regression on the resulting plans, and lift the corresponding outputs to obtain a set of first-order Condition → Actions rules. The rules collectively constitute a generalised plan that can be executed as is or alternatively be used to prune the planning search space. We formalise and prove the conditions under which our method is guaranteed to learn valid generalised plans and state space pruning axioms for search. Experiments demonstrate significant improvements over state-of-the-art (generalised) planners with respect to the 3 metrics of synthesis cost, planning coverage, and solution quality on various classical and numeric planning domains.

Reward machines (RMs) are automata structures that encode (non-Markovian) reward functions for reinforcement learning (RL). RMs can reward any behaviour representable in regular languages and, when paired with RL algorithms that exploit RM structure, have been shown to significantly improve sample efficiency in many domains. In this work, we present pushdown reward machines (pdRMs), an extension of reward machines based on deterministic pushdown automata. pdRMs can recognise and reward temporally extended behaviours representable in deterministic context-free languages, making them more expressive than reward machines. We introduce two variants of pdRM-based policies, one which has access to the entire stack of the pdRM, and one which can only access the top k symbols (for a given constant k) of the stack. We propose a procedure to check when the two kinds of policies (for a given environment, pdRM, and constant k) achieve the same optimal state values. We then provide theoretical results establishing the expressive power of pdRMs, and space complexity results for the proposed learning problems. Lastly, we propose an approach for off-policy RL algorithms that exploits counterfactual experiences with pdRMs. We conclude by providing experimental results showing how agents can be trained to perform tasks representable in deterministic context-free languages using pdRMs.

Grounding language in perception and action is a key challenge when building situated agents that can interact with humans, or other agents, via language. In the past, addressing this challenge has required manually designing the language grounding or curating massive datasets that associate language with the environment. We propose Ground-Compose-Reinforce, an end-to-end, neurosymbolic framework for training RL agents directly from high-level task specifications—without manually designed reward functions or other domain-specific oracles, and without massive datasets. These task specifications take the form of Reward Machines, automata-based representations that capture high-level task structure and are in some cases autoformalizable from natural language. Critically, we show that Reward Machines can be grounded using limited data by exploiting compositionality. Experiments in a custom Meta-World domain with only 350 labelled pretraining trajectories show that our framework faithfully elicits complex behaviours from high-level specifications—including behaviours that never appear in pretraining—while non-compositional approaches fail.

Large Language Model (LLM) agents have demonstrated impressive capabilities for social interaction and are increasingly being deployed in situations where they might engage with both human and artificial agents. These interactions represent a critical frontier for LLM-based agents, yet existing evaluation methods fail to measure how well these capabilities generalize to novel social situations. In this paper, we introduce a method for evaluating the ability of LLM-based agents to cooperate in zero-shot, mixed-motive environments using Concordia, a natural language multi-agent simulation environment. Our method measures general cooperative intelligence by testing an agent's ability to identify and exploit opportunities for mutual gain across diverse partners and contexts. We present empirical results from the NeurIPS 2024 Concordia Contest, where agents were evaluated on their ability to achieve mutual gains across a suite of diverse scenarios ranging from negotiation to collective action problems. Our findings reveal significant gaps between current agent capabilities and the robust generalization required for reliable cooperation, particularly in scenarios demanding persuasion and norm enforcement.

Training data attribution (TDA) provides insights into which training data is responsible for a learned model behavior. Gradient-based TDA methods such as influence functions and unrolled differentiation both involve a computation that resembles an inverse Hessian-vector product (iHVP), which is difficult to approximate efficiently. We introduce an algorithm (ASTRA) which uses the EKFAC-preconditioner on Neumann series iterations to arrive at an accurate iHVP approximation for TDA. ASTRA is easy to tune, requires fewer iterations than Neumann series iterations, and is more accurate than EKFAC-based approximations. Using ASTRA, we show that improving the accuracy of the iHVP approximation can significantly improve TDA performance.

Constrained clustering is a semi-supervised approach to determining meaningful groupings of data that respect userspecified constraints. Such constraints are typically used to enforce desirable structural and domain-specific properties of the resulting clusters. Notably, such constraints can significantly improve the quality and accuracy of clustering. Data clustering solutions can take on many different forms. Decision trees are a particularly desirable solution form because of their inherent interpretability. Unfortunately, existing decision tree clustering approaches do not support clustering constraints and do not provide strong theoretical guarantees with respect to solution quality. To address the task of decision tree clustering with constraints, we present a novel SAT-based encoding that solves the problem to an approximated optimality in relation to a well-known bi-criteria objective. Our framework is the first exact approach for interpretable constrained clustering with decision trees. Experiments involving a range of real-world and synthetic datasets demonstrate that our approach can produce interpretable clustering solutions that are of superior quality compared to their non-interpretable counterparts, with or without the addition of constraints. We further provide new insights into the trade-off between interpretability and the satisfaction of user-specified constraints, presenting extensions to our clustering approach that treat the satisfaction of constraints as an additional optimization objective.

Fully Observable Non-Deterministic (FOND) planning is a variant of classical symbolic planning in which actions are nondeterministic, with an action's outcome known only upon execution. It is a popular planning paradigm with applications ranging from robot planning to dialogue-agent design and reactive synthesis. Over the last 20 years, a number of approaches to FOND planning have emerged. In this work, we establish a new state of the art, following in the footsteps of some of the most powerful FOND planners to date. Our planner, PR2, decisively outperforms the four leading FOND planners, at times by a large margin, in 17 of 18 domains that represent a comprehensive benchmark suite. Ablation studies demonstrate the impact of various techniques we introduce, with the largest improvement coming from our novel FOND-aware heuristic.

Fair decision making has largely been studied with respect to a single decision. Here we investigate the notion of fairness in the context of sequential decision making where multiple stakeholders can be affected by the outcomes of decisions. We observe that fairness often depends on the history of the sequential decision-making process, and in this sense that it is inherently non-Markovian. We further observe that fairness often needs to be assessed at time points within the process, not just at the end of the process. To advance our understanding of this class of fairness problems, we explore the notion of non-Markovian fairness in the context of sequential decision making. We identify properties of non-Markovian fairness, including notions of long-term, anytime, periodic, and bounded fairness. We explore the interplay between non-Markovian fairness and memory and how memory can support construction of fair policies. Finally, we introduce the FairQCM algorithm, which can automatically augment its training data to improve sample efficiency in the synthesis of fair policies via reinforcement learning.

Reward Machines provide an automaton-inspired structure for specifying instructions, safety constraints, and other temporally extended reward-worthy behaviour. By exposing the underlying structure of a reward function, they enable the decomposition of an RL task, leading to impressive gains in sample efficiency. Although Reward Machines and similar formal specifications have a rich history of application towards sequential decision-making problems, prior frameworks have traditionally ignored ambiguity and uncertainty when interpreting the domain-specific vocabulary forming the building blocks of the reward function. Such uncertainty critically arises in many real-world settings due to factors like partial observability or noisy sensors. In this work, we explore the use of Reward Machines for Deep RL in noisy and uncertain environments. We characterize this problem as a POMDP and propose a suite of RL algorithms that exploit task structure under uncertain interpretation of the domain-specific vocabulary. Through theory and experiments, we expose pitfalls in naive approaches to this problem while simultaneously demonstrating how task structure can be successfully leveraged under noisy interpretations of the vocabulary.

Embedded ethics education integrates ethical considerations into computer sciences courses in support of ethics-informed design, development, and deployment of technology. Scholarly assessment has demonstrated that such modules can influence students' attitudes about the relevance and importance of ethics to their work, as well as their perceived ability to tackle ethical issues in the workplace. In this paper, we report on a study that investigates whether embedded ethics modules have an impact beyond the classroom. Specifically, we examine whether embedded ethics modules influence students to learn more about ethics on their own, whether students are better able to recognize ethical issues when they enter the workplace for an industrial or research work experience, and whether they report that the modules they participated in helped them to navigate the ethical situations they encountered at work. While further assessment is needed to investigate these questions fully, our results suggest that embedded ethics modules can indeed have this kind of positive impact beyond the classroom.

In recent years, neural sequence models have been applied successfully to solve combinatorial optimization problems. Solutions, encoded as sequences, are typically generated from trained models via beam search, a search algorithm that generates sequences token-by-token while keeping a fixed number of promising partial solutions at each step. In this paper, we explore the problem of augmenting beam search generation with the enforcement of requirements---hard constraints that any generated solution must adhere to. We propose a hybrid approach, by encoding the requirements in the form of a constraint satisfaction problem (CSP) and iteratively solving the CSP to cut any partial solution within the beam search that is incapable of satisfying the requirements. We study this problem in the context of vehicle routing problems (VRP) further augmented with capacity-related or temporal requirements. We experimentally show that cuts often allow us to satisfy the requirements with negligible impact on solution quality. Without the use of cuts, beam search is shown to be exponentially less likely to satisfy the requirements as the length of the solution increases and/or the requirements are strengthened.

Decision trees are a popular classification model in machine learning due to their interpretability and performance. However, the number of splits in decision trees grow exponentially with their depth which can incur a higher computational cost, increase data fragmentation, hinder interpretability, and restrict their applicability to memory-constrained hardware. In constrast, binary decision diagrams (BDD) utilize the same split across each level, leading to a linear number of splits in total. Recent work has considered optimal binary decision diagrams (BDD) as compact and accurate classification models, but has only focused on binary datasets and has not explicitly optimized the compactness of the resulting diagrams. In this work, we present a SAT-based encoding for a multi-terminal variant of BDDs (MTBDDs) that incorporates a state-of-the-art direct encoding of numerical features. We then develop and evaluate different approaches to explicitly optimize the compactness of the diagrams. In one family of approaches, we learn a tree BDD first and model the size of the diagram the tree will be reduced to as a secondary objective, in a one-stage or two-stage optimization scheme. Alternatively, we directly learn diagrams that support multi-dimensional splits for improved expressiveness. Our experiments show that direct encoding of numerical features leads to better performance. Furthermore, we show that exact optimization of size leads to more compact solutions while maintaining higher accuracy. Finally, our experiments show that multi-dimensional splits are a viable approach to achieving higher expressiveness with a lower computational cost.

Many important real-world Reinforcement Learning (RL) problems involve partial observability and require policies with memory. Unfortunately, standard deep RL algorithms for partially observable settings typically condition on the full history of interactions and are notoriously difficult to train. We propose a novel deep, partially observable RL algorithm based on modelling belief states — a technique typically used when solving tabular POMDPs, but that has traditionally been difficult to apply to more complex environments. Our approach simplifies policy learning by leveraging state information at training time, that may not be available at deployment time. We do so in two ways: first, we decouple belief state modelling (via unsupervised learning) from policy optimization (via RL); and second, we propose a representation learning approach to capture a compact set of reward-relevant features of the state. Experiments demonstrate the efficacy of our approach on partially observable domains requiring information seeking and long-term memory.

Constrained clustering is a semi-supervised task that employs a limited amount of labelled data, formulated as constraints, to incorporate domain-specific knowledge and to significantly improve clustering accuracy. Previous work has considered exact optimization formulations that can guarantee optimal clustering while satisfying all constraints, however these approaches lack interpretability. Recently, decision trees have been used to produce inherently interpretable clustering solutions, however existing approaches do not support clustering constraints and do not provide strong theoretical guarantees on solution quality. In this work, we present a novel SAT-based framework for interpretable clustering that supports clustering constraints and that also provides strong theoretical guarantees on solution quality. We also present new insight into the trade-off between interpretability and satisfaction of such user-provided constraints. Our framework is the first approach for interpretable and constrained clustering. Experiments with a range of real-world and synthetic datasets demonstrate that our approach can produce high-quality and interpretable constrained clustering solutions.

Within the field of automated planning, two areas of study are planning with preferences and epistemic planning. Planning with preferences involves generating plans that optimize for properties of the plan instead of, or in addition to, trying to reach a fixed goal. Epistemic planning allows for planning over the knowledge or belief states of one or more agents for the purpose of achieving epistemic goals (where agents have particular states of knowledge or belief). In this paper we motivate and explore the task of planning with epistemic preferences, proposing a method by which existing automated planning techniques can be combined for this purpose.

Constructing AI models that respond to text instructions is challenging, especially for sequential decision-making tasks. This work introduces a methodology, inspired by unCLIP, for instruction-tuning generative models of behavior without relying on a large dataset of instruction-labeled trajectories. Using this methodology, we create an instruction-tuned Video Pretraining (VPT) model called STEVE-1, which can follow short-horizon open-ended text and visual instructions in Minecraft. STEVE-1 is trained in two steps: adapting the pretrained VPT model to follow commands in MineCLIP's latent space, then training a prior to predict latent codes from text. This allows us to finetune VPT through self-supervised behavioral cloning and hindsight relabeling, reducing the need for costly human text annotations, and all for only $60 of compute. By leveraging pretrained models like VPT and MineCLIP and employing best practices from text-conditioned image generation, STEVE-1 sets a new bar for open-ended instruction following in Minecraft with low-level controls (mouse and keyboard) and raw pixel inputs, far outperforming previous baselines and robustly completing 12 of 13 tasks in our early-game evaluation suite. We provide experimental evidence highlighting key factors for downstream performance, including pretraining, classifier-free guidance, and data scaling. All resources, including our model weights, training scripts, and evaluation tools are made available for further research.

Embedding ethics modules in computer science (CS) courses is an approach to post-secondary ethics education that has been gaining traction. In contrast to dedicated courses on ethics in CS, embedding ethics modules into CS courses supports tight connections between ethical considerations and CS concepts, as well as enabling repeated exposure to ethics across multiple courses. Initial studies of the effectiveness of such modules suggest that this approach can increase both student interest in ethics and technology, and student self-efficacy towards incorporating ethical considerations in their computing work. Departments wishing to deploy embedded ethics (EE) modules need to decide how to invest resources, including class time, to maximize effectiveness while maintaining curriculum objectives. Such considerations include the number of EE module experiences a student has throughout their degree program, as well as the spacing of those experiences.

In sequential decision making, objective specifications are often underspecified or incomplete, neglecting to take into account potential (negative) side effects. Executing plans without consideration of their side effects can lead to catastrophic outcomes -- a concern recently raised in relation to the safety of AI. In this paper we investigate how to avoid side effects in a symbolic planning setting. We study the notion of minimizing side effects in the context of a planning environment where multiple independent agents co-exist. We define (classes of) negative side effects in terms of their effect on the agency of those other agents. Finally, we show how plans which minimize side effects of different types can be computed via compilations to cost-optimizing symbolic planning, and investigate experimentally.

Advanced social cognitive skills enhance the effectiveness of human-robot interactions. Research shows that an important precursor to the development of these abilities in humans is Theory of Mind (ToM) - the ability to attribute mental states to oneself and to others. In this work, we endow robots with ToM abilities and propose a ToM-based approach to proactive robotic assistance by appealing to epistemic planning techniques. Our evaluation shows that robots implementing our approach and demonstrating ToM are measurably more helpful and perceived by humans as more socially intelligent compared to robots with a deficit in ToM.

Recently, methods such as Decision Transformer that reduce reinforcement learning to a prediction task and solve it via supervised learning (RvS) have become popular due to their simplicity, robustness to hyperparameters, and strong overall performance on offline RL tasks. However, simply conditioning a probabilistic model on a desired return and taking the predicted action can fail dramatically in stochastic environments since trajectories that result in a return may have only achieved that return due to luck. In this work, we describe the limitations of RvS approaches in stochastic environments and propose a solution. Rather than simply conditioning on returns, as is standard practice, our proposed method, ESPER, conditions on learned average returns which are independent from environment stochasticity. Doing so allows ESPER to achieve strong alignment between target return and expected performance in real environments. We demonstrate this in several challenging stochastic offline-RL tasks including the challenging puzzle game 2048, and Connect Four playing against a stochastic opponent. In all tested domains, ESPER achieves significantly better alignment between the target return and achieved return than simply conditioning on returns. ESPER also achieves higher maximum performance than even the value-based baselines.

Text-based games present a unique class of sequential decision making problem in which agents interact with a partially observable, simulated environment via actions and observations conveyed through natural language. Such observations typically include instructions that, in a reinforcement learning (RL) setting, can directly or indirectly guide a player towards completing reward-worthy tasks. In this work, we study the ability of RL agents to follow such instructions. We conduct experiments that show that the performance of state-of-the-art text-based game agents is largely unaffected by the presence or absence of such instructions, and that these agents are typically unable to execute tasks to completion. To further study and address the task of instruction following, we equip RL agents with an internal structured representation of natural language instructions in the form of Linear Temporal Logic (LTL), a formal language that is increasingly used for temporally extended reward specification in RL. Our framework both supports and highlights the benefit of understanding the temporal semantics of instructions and in measuring progress towards achievement of such a temporally extended behaviour. Experiments with 500+ games in TextWorld demonstrate the superior performance of our approach.

Technology is shaping the way people live, work, and interact with each other, and graduates of our computer science programs increasingly find themselves designing algorithms and using data that raise ethical issues they may not be aware of or equipped to address. Courses that contemplate the role of technology in society have been a standard, but often optional, part of curricula for years. An emerging alternative is to embed ethical discussions as modules within CS courses. This approach offers the opportunity to tie ethical issues to technical content at the moment students learn it, and to have students engage with these issues repeatedly throughout their degree. However, little is known about the effect of embedded ethics education on students.

Reinforcement learning (RL) methods usually treat reward functions as black boxes. As such, these methods must extensively interact with the environment in order to discover rewards and optimal policies. In most RL applications, however, users have to program the reward function and, hence, there is the opportunity to make the reward function visible – to show the reward function’s code to the RL agent so it can exploit the function’s internal structure to learn optimal policies in a more sample efficient manner. In this paper, we show how to accomplish this idea in two steps. First, we propose reward machines, a type of finite state machine that supports the specification of reward functions while exposing reward function structure. We then describe different methodologies to exploit this structure to support learning, including automated reward shaping, task decomposition, and counterfactual reasoning with off-policy learning. Experiments on tabular and continuous domains, across different tasks and RL agents, show the benefits of exploiting reward structure with respect to sample efficiency and the quality of resultant policies. Finally, by virtue of being a form of finite state machine, reward machines have the expressive power of a regular language and as such support loops, sequences and conditionals, as well as the expression of temporally extended properties typical of linear temporal logic and non-Markovian reward specification.

Sequence classification is the task of predicting a class label given a sequence of observations. In many applications such as healthcare monitoring or intrusion detection, early classification is crucial to prompt intervention. In this work, we learn sequence classifiers that favour early classification from an evolving observation trace. While many state-of-the-art sequence classifiers are neural networks, and in particular LSTMs, our classifiers take the form of finite state automata and are learned via discrete optimization. Our automata-based classifiers are interpretable---supporting explanation, counterfactual reasoning, and human-in-the-loop modification---and have strong empirical performance. Experiments over a suite of goal recognition and behaviour classification datasets show our learned automata-based classifiers to have comparable test performance to LSTM-based classifiers, with the added advantage of being interpretable.

Decision trees are a popular classification model in machine learning due to their interpretability and performance. Traditionally, decision-tree classifiers are constructed using greedy heuristic algorithms, however these algorithms do not provide guarantees on the quality of the resultant trees. Instead, a recent line of work has studied the use of exact optimization approaches for constructing optimal decision trees. Most of the recent approaches that employ exact optimization are designed for datasets with binary features. While numeric and categorical features can be transformed to binary features, this transformation can introduce a large number of binary features and may not be efficient in practice. In this work, we present a novel SAT-based encoding for decision trees that supports non-binary features and demonstrate how it can be used to solve two well-studied variants of the optimal decision tree problem. We perform an extensive empirical analysis that shows our approach obtains superior performance and is often an order of magnitude faster than the current state-of-the-art exact techniques on non-binary datasets.

We address the problem of teaching a deep reinforcement learning (RL) agent to follow instructions in multi-task environments. Instructions are expressed in a well-known formal language {–} linear temporal logic (LTL) {–} and can specify a diversity of complex, temporally extended behaviours, including conditionals and alternative realizations. Our proposed learning approach exploits the compositional syntax and the semantics of LTL, enabling our RL agent to learn task-conditioned policies that generalize to new instructions, not observed during training. To reduce the overhead of learning LTL semantics, we introduce an environment-agnostic LTL pretraining scheme which improves sample-efficiency in downstream environments. Experiments on discrete and continuous domains target combinatorial task sets of up to $\sim10^{39}$ unique tasks and demonstrate the strength of our approach in learning to solve (unseen) tasks, given LTL instructions.

The objective of goal recognition is to infer a goal that accounts for the observed behavior of an actor. In this work, we introduce and formalize the notion of active goal recognition in which we endow the observer with agency to sense, reason, and act in the world with a view to enhancing and possibly expediting goal recognition, and/or to intervening in goal achievement. To this end, we present an algorithm for active goal recognition and a landmark-based approach to the elimination of hypothesized goals which leverages automated planning. Experiments demonstrate the merits of providing agency to the observer, and the effectiveness of our approach in potentially enhancing the observational power of the observer, as well as expediting and in some cases making possible the recognition of the actor's goal.

Agents change their beliefs about the plausibility of various aspects of domain dynamics -- effects of physical actions, results of sensing, and action preconditions -- as a consequence of their interactions with the world. In this paper we propose a way to conveniently represent domain dynamics in the situation calculus to support such belief change. Furthermore, we suggest patterns to follow when writing the axioms that describe the effects of actions, and prove how these patterns can control the extent to which observations change the agent's beliefs about action effects. We also discuss the relation of our work to the AGM postulates for belief revision. Finally, we show how beliefs about domain dynamics can be incorporated into a form of regression rewriting to support reasoning.

We consider a class of generalized planning problems based on the idea of quantifying over sets of similar objects. We show how we can adapt fully observable nondeterministic planning techniques to produce generalized solutions that are easy to instantiate over particular problem instances. We also describe how we can reformulate a classical planning problem into a quantified one. The reformulation allows us to solve the original planning task without grounding every action with respect to all objects in the problem, and a single solution can be applied to a possibly infinite set of related classical planning tasks. We report experimental results that show our approach is a practical and promising technique for solving an interesting class of problems.

In Reinforcement Learning (RL), an agent is guided by the rewards it receives from the reward function. Unfortunately, it may take many interactions with the environment to learn from sparse rewards, and it can be challenging to specify reward functions that reflect complex reward-worthy behavior. We propose using reward machines (RMs), which are automata-based representations that expose reward function structure, as a normal form representation for reward functions. We show how specifications of reward in various formal languages, including LTL and other regular languages, can be automatically translated into RMs, easing the burden of complex reward function specification. We then show how the exposed structure of the reward function can be exploited by tailored q-learning algorithms and automated reward shaping techniques in order to improve the sample efficiency of reinforcement learning methods. Experiments show that these RM-tailored techniques significantly outperform state-of-the-art (deep) RL algorithms, solving problems that otherwise cannot reasonably be solved by existing approaches.

We are concerned with the synthesis of strategies for sequential decision-making in non-deterministic dynamical environments where the objective is to satisfy a prescribed temporally extended goal. We frame this task as a Fully Observable Non-Deterministic planning problem with the goal expressed in Linear Temporal Logic (LTL), or LTL interpreted over finite traces (LTLf). While the problem is well-studied theoretically, existing algorithmic solutions typically compute so-called strong-cyclic solutions, which are predicated on an assumption of fairness. In this paper we introduce novel algorithms to compute so-called strong solutions, that guarantee goal satisfaction even in the absence of fairness. Our strategy generation algorithms are complemented with novel mechanisms to obtain proofs of unsolvability. We implemented and evaluated the performance of our approaches in a selection of domains with LTL and LTLf goals.

Reward Machines (RMs), originally proposed for specifying problems in Reinforcement Learning (RL), provide a structured, automata-based representation of a reward function that allows an agent to decompose problems into subproblems that can be efficiently learned using off-policy learning. Here we show that RMs can be learned from experience, instead of being specified by the user, and that the resulting problem decomposition can be used to effectively solve partially observable RL problems. We pose the task of learning RMs as a discrete optimization problem where the objective is to find an RM that decomposes the problem into a set of subproblems such that the combination of their optimal memoryless policies is an optimal policy for the original problem. We show the effectiveness of this approach on three partially observable domains, where it significantly outperforms A3C, PPO, and ACER, and discuss its advantages, limitations, and broader potential.

In this paper we propose Reward Machines {—} a type of finite state machine that supports the specification of reward functions while exposing reward function structure to the learner and supporting decomposition. We then present Q-Learning for Reward Machines (QRM), an algorithm which appropriately decomposes the reward machine and uses off-policy q-learning to simultaneously learn subpolicies for the different components. QRM is guaranteed to converge to an optimal policy in the tabular case, in contrast to Hierarchical Reinforcement Learning methods which might converge to suboptimal policies. We demonstrate this behavior experimentally in two discrete domains. We also show how function approximation methods like neural networks can be incorporated into QRM, and that doing so can find better policies more quickly than hierarchical methods in a domain with a continuous state space.

In this paper, we address the problem of LTL realizability and synthesis. State of the art techniques rely on so-called bounded synthesis methods, which reduce the problem to a safety game. Realizability is determined by solving synthesis in a dual game. We provide a unified view of duality, and introduce novel bounded realizability methods via reductions to reachability games. Further, we introduce algorithms, based on AI automated planning, to solve these safety and reachability games. This is the the first complete approach to LTL realizability and synthesis via automated planning. Experiments illustrate that reductions to reachability games are an alternative to reductions to safety games, and show that planning can be a competitive approach to LTL realizability and synthesis.

Automatic synthesis of software from specification is one of the classic problems in computer science. In the last decade, significant advances have been made in the synthesis of programs from specifications expressed in Linear Temporal Logic (LTL). LTL synthesis technology is central to a myriad of applications from the automated generation of controllers for Internet of Things devices, to the synthesis of control software for robotic applications. Unfortunately, the number of existing tools for LTL synthesis is limited, and using them requires specialized expertise. In this paper we present SynKit, a tool that offers LTL synthesis as a service. SynKit integrates a RESTful API and a web service with an editor, a solver, and a strategy visualizer.

Temporally extended goals are critical to the specification of a diversity of real-world planning problems. Here we examine the problem of non-deterministic planning with temporally extended goals specified in linear temporal logic (LTL), interpreted over either finite or infinite traces. Unlike existing LTL planners, we place no restrictions on our LTL formulae beyond those necessary to distinguish finite from infinite interpretations. We generate plans by compiling LTL temporally extended goals into problem instances described in the Planning Domain Definition Language that are solved by a state-of-the-art fully observable non-deterministic planner. We propose several different compilations based on translations of LTL to (Büchi) alternating or (Büchi) non-deterministic finite state automata, and evaluate various properties of the competing approaches. We address a diverse spectrum of LTL planning problems that, to this point, had not been solvable using AI planning techniques, and do so in a manner that demonstrates highly competitive performance.

State estimation is the task of estimating the state of a partially observable dynamical system given a sequence of executed actions and observations. In logical settings, state estimation can be realized via logical filtering, which is exact but can be intractable. We propose logical smoothing, a form of backwards reasoning that works in concert with approximated logical filtering to refine past beliefs in light of new observations. We characterize the notion of logical smoothing together with an algorithm for backwards-forwards state estimation. We also present an approximation of our smoothing algorithm that is space efficient. We prove properties of our algorithms, and experimentally demonstrate their behaviour, contrasting them with state estimation methods for planning. Smoothing and backwards-forwards reasoning are important techniques for reasoning about partially observable dynamical systems, introducing the logical analogue of effective techniques from control theory and dynamic programming.

The real-world application of planning techniques often requires models with numeric fluents. However, these fluents are not directly supported by most planners and heuristics. We describe a family of planning algorithms that takes a numeric planning problem and produces an abstracted representation that can be solved using any classical planner. The resulting abstract plan is generalized into a policy and then used to guide the search in the original numeric domain. We prove that our approach is sound, and we evaluate it on a set of standard benchmarks. We show that it can provide competitive performance when compared to other well-known algorithms for numeric planning, and a significant performance improvement in certain domains.

We propose an approach to solving Markov Decision Processes with non-Markovian rewards specified in Linear Temporal Logic interpreted over finite traces (LTL-f). Our approach integrates automata representations of LTL-f formulae into compiled MDPs that can be solved by off-the-shelf MDP planners, exploiting reward shaping to help guide search. Experiments with state-of-the-art UCT-based MDP planner PROST show automata-based reward shaping to be an effective method to guide search, producing solutions of superior quality, while maintaining policy optimality guarantees.

The proliferation of programmable devices, personal assistants, and autonomous systems presents fundamental challenges to the deployment of safe, predictable systems that can work together, interact seamlessly with humans, and that are taskable and instructable by people who may not know how to program. In this talk, we will revisit the classical problem of program synthesis through the lens of AI automated planning. We will present recent advances in AI automated planning principles and computational methods that support the synthesis of plans with goals and preferences specified in Linear Temporal Logic and Regular Expressions. Moving from automated planning in deterministic domains to planning in nondeterministic domains, we will explore the pathway to synthesizing programs that are taskable and instructable by exploiting state-of-the-art AI planning technology.

Many real-world planning problems are best modeled as infinite search space problems, using numeric fluents. Unfortunately, most planners and planning heuristics do not directly support such fluents. We propose a search space abstraction technique that compiles a planning problem with numeric fluents into a finite state propositional planning problem. To account for the loss of precision resulting from the abstraction, we leverage a policy repair technique used for non-deterministic planning. We evaluate our approach on a set of benchmarks and compare it to state-of-the-art planners that deal with numeric fluents.

Partial-order plans (POPs) are attractive because of their least-commitment nature, which provides enhanced plan flexibility at execution time relative to sequential plans. Current research on automated plan generation focuses on producing sequential plans, despite the appeal of POPs. In this paper we examine POP generation by relaxing or modifying the action orderings of a sequential plan to optimize for plan criteria that promote flexibility. Our approach relies on a novel partial weighted MaxSAT encoding of a sequential plan that supports the minimization of deordering or reordering of actions. Using a similar technique, we further demonstrate how to remove redundant actions from the plan, and how to combine this criterion with the objective of maximizing a POP's flexibility. Our partial weighted MaxSAT encoding allows us to compute a POP from a sequential plan effectively. We compare the efficiency of our approach to previous methods for POP generation via sequential-plan relaxation. Our results show that while an existing heuristic approach consistently produces the optimal deordering of a sequential plan, our approach has greater flexibility when we consider reordering the actions in the plan while also providing a guarantee of optimality. We also investigate and confirm the accuracy of the standard flex metric typically used to predict the true flexibility of a POP as measured by the number of linearizations it represents.

Many AI applications involve the interaction of multiple autonomous agents, requiring those agents to reason about their own beliefs, as well as those of other agents. However, planning involving nested beliefs is known to be computationally challenging. In this work, we address the task of synthesizing plans that necessitate reasoning about the beliefs of other agents. We plan from the perspective of a single agent with the potential for goals and actions that involve nested beliefs, non-homogeneous agents, co-present observations, and the ability for one agent to reason as if it were another. We formally characterize our notion of planning with nested belief, and subsequently demonstrate how to automatically convert such problems into problems that appeal to classical planning technology. Our approach represents an important first step towards applying the well-established field of automated planning to the challenging task of planning involving nested beliefs of multiple agents.

Reconfiguring a topology is an important management technique to sustain high efficiency and robustness of an overlay. But, the problem of transforming the overlay from an old topology to a newly refined topology, at runtime, has received relatively little attention. The key challenge is to minimize the disruption that can be caused by topology transformation operations. Excessive disruption can be costly and harmful and thus it may hamper the decision to migrate to a better topology. To address this issue, we solve a problem of finding an appropriate sequence of steps to transform a topology that incurs the least service disruption. We refer to this problem as an incremental topology transformation (ITT) problem. The ITT problem can be formulated as an automated planning problem and can be solved with numerous off-the-shelf planning techniques. However, we found that state-of-the-art domain-independent planning techniques did not scale to solve large ITT problem instances. This shortcoming motivated us to develop a suite of planners that use novel domain-specific heuristics to guide the search for a solution. We empirically evaluated our planners on a wide range of topologies. Our results illustrate that our planners offer a viable solution to a diversity of ITT problems. We envision that our approach could eventually provide a compelling addition to the arsenal of techniques currently employed by the administrators of distributed overlay networks.

Planning with sensing actions under partial observability is a computationally challenging problem that is fundamental to the realization of AI tasks in areas as diverse as robotics, game playing, and diagnostic problem solving. Recent work on generating plans for partially observable domains has advocated for online planning, claiming that offline plans are often too large to generate. Here we push the envelope on this challenging problem, proposing a technique for generating conditional (aka contingent) plans offline. The key to our planner's success is the reliance on state-of-the-art techniques for fully observable non-deterministic (FOND) planning. In particular, we use an existing compilation for converting a planning problem under partial observability and sensing to a FOND planning problem. With a modified FOND planner in hand, we are able to scale beyond previous techniques for generating conditional plans with solutions that are orders of magnitude smaller than previously possible in some domains.

In this paper we revisit the problem of generating query plans using AI automated planning with a view to leveraging significant recent advances in state-of-the-art planning techniques. Our efforts focus on the specific problem of cost-based join-order optimization for conjunctive relational queries, a critical component of production-quality query optimizers. We characterize the general query-planning problem as a delete-free planning problem, and query plan optimization as a context-sensitive cost-optimal planning problem. We propose algorithms that generate high-quality query plans, guaranteeing optimality under certain conditions. Our approach is general, supporting the use of a broad suite of domain-independent and domain-specific optimization criteria. Experimental results demonstrate the effectiveness of AI planning techniques for query plan generation and optimization.

Many practical planning problems necessitate the generation of a plan under incomplete information about the state of the world. In this paper we propose the notion of Assumption-Based Planning. Unlike conformant planning, which attempts to find a plan under all possible completions of the initial state, an assumption-based plan supports the assertion of additional assumptions about the state of the world, often resulting in high quality plans where no conformant plan exists. We are interested in this paradigm of planning for two reasons: 1) it captures a compelling form of \emph{commonsense planning}, and 2) it is of great utility in the generation of explanations, diagnoses, and counter-examples -- tasks which share a computational core with We formalize the notion of assumption-based planning, establishing a relationship between assumption-based and conformant planning, and prove properties of such plans. We further provide for the scenario where some assumptions are more preferred than others. Exploiting the correspondence with conformant planning, we propose a means of computing assumption-based plans via a translation to classical planning. Our translation is an extension of the popular approach proposed by Palacios and Geffner and realized in their T0 planner. We have implemented our planner, A0, as a variant of T0 and tested it on a number of expository domains drawn from the International Planning Competition. Our results illustrate the utility of this new planning paradigm.

In this paper we examine the general problem of generating preferred explanations for observed behavior with respect to a model of the behavior of a dynamical system. This problem arises in a diversity of applications including diagnosis of dynamical systems and activity recognition. We provide a logical characterization of the notion of an explanation. To generate explanations we identify and exploit a correspondence between explanation generation and planning. The determination of good explanations requires additional domain-specific knowledge which we represent as preferences over explanations. The nature of explanations requires us to formulate preferences in a somewhat retrodictive fashion by utilizing Past Linear Temporal Logic. We propose methods for exploiting these somewhat unique preferences effectively within state-of-the-art planners and illustrate the feasibility of generating (preferred) explanations via planning.

Partial-order plans (POPs) have the capacity to compactly represent numerous distinct plan linearizations and as a consequence are inherently robust. We exploit this robustness to do effective execution monitoring. We characterize the conditions under which a POP remains viable as the regression of the goal through the structure of a POP. We then develop a method for POP execution monitoring via a structured policy, expressed as an ordered algebraic decision diagram. The policy encompasses both state evaluation and action selection, enabling an agent to seamlessly switch between POP linearizations to accommodate unexpected changes during execution. We demonstrate the effectiveness of our approach by comparing it empirically and analytically to a standard technique for execution monitoring of sequential plans. On standard benchmark planning domains, our approach is 2 to 17 times faster and up to 2.5 times more robust than comparable monitoring of a sequential plan. On POPs that have few ordering constraints among actions, our approach is significantly more robust, with the ability to continue executing in up to an exponential number of additional states. 1

Our long-term goal is to build a query answering system that can answer questions on a wide variety of topics and explain the answers. In such a situation, a designer faces the challenge of how to specify the KR&R requirements that are needed to answer questions. In this paper, we introduce a categorization of KR&R methods, and apply it to specifying the requirements for answering questions in six different domains: Physics, Chemistry, Biology, Environmental Science, Microeconomics, and U.S. Government & Politics. Drawing from the corpus of about 500 questions that we analyzed, we consider an example question in each domain and show the analytical process that we used to derive the requirements in terms of the KR&R categorization. We analyze the effectiveness of the current KR&R categorization, and identify directions for future work suggesting how this categorization can be further evolved by community participation.

Requirements can differ in their importance. As such the priorities that stakeholders associate with requirements may vary from stakeholder to stakeholder and from one situation to the next. Differing priorities, in turn, imply different design decisions for the end system. While elicitation of requirements priorities is a well studied activity, though, the modeling and reasoning side of prioritization has not enjoyed equal attention. In this paper, we address this by extending a traditional goal modeling notation to support the representation of optional and preference requirements. In our extension, optional goals are distinguished from mandatory ones. Then, quantitative prioritizations of the former are constructed and used as criteria for evaluating alternative ways to achieve the latter. A state-of-the-art preference-based planner is utilized to efficiently search for alternatives that best satisfy the given preferences. This way, analysts can acquire a better understanding of the impact of high-level stakeholder preferences to low-level design decisions.

Branch-and-Bound search is a basic algorithm for solving combinatorial optimization problems. Here we introduce a new lower-bounding methodology that can be incorporated into any branch-and-bound solver, and demonstraint its use on the MaxSAT constraint optimization problem. The approach is to adapt a “minimum-height equivalent transformation” framework that was first developed in the context of computer vision. We present efficient algorithms to realize this framework within the MaxSAT domain, and demonstrate their feasibility by implementing them within the state-of-the-art maxsatz solver. We evaluate the solver on test sets from the 2009 MaxSAT competition; we observe a basic performance tradeoff whereby the (quadratic) time cost of computing the transformations may or may not be worthwhile in exchange for better bounds and more frequent pruning. For specific test sets, the trade-off does result in significant improvement in both prunings and overall run-time.

The analysis of stakeholder requirements is a critical aspect of software engineering. A common way of specifying stakeholder requirements is in terms of a hierarchy of goals whose AND/OR decomposition captures a family of software solutions that comply with the goals. In this paper, we extend this goal modeling framework to include the specification of optional user requirements and user preferences, aggregated together into weighted formulae to be optimized. We team this with an automated reasoning tool, adapted from state of the art research in artificial intelligence planning with preferences, in order to synthesize solutions that both comply with the goals and optimize stakeholder preferences and optional requirements.

Monitoring the satisfaction of software requirements and diagnosing what went wrong in case of failure is a hard problem that has received little attention in the Software and Requirement Engineering literature. To address this problem, we propose a framework adapted from artificial intelligence theories of action and diagnosis. Specifically, the framework monitors the satisfaction of software requirements and generates log data at a level of granularity that can be tuned adaptively at runtime depending on monitored feedback. When errors are found, the framework diagnoses the denial of the requirements and identifies problematic components. To support diagnostic reasoning, we transform the diagnostic problem into apropositional satisfiability (SAT) problem that can be solved by existing SAT solvers. We preprocess log data into a compact propositional encoding that better scales with problem size. The proposed theoretical framework has been implemented as a diagnosing component that will return sound and complete diagnoses accounting for observed aberrant system behaviors. Our solution is illustrated with two medium-sized publicly available case studies: a Web-based email client and an ATM simulation. Our experimental results demonstrate the feasibility of scaling our approach to medium-size software systems

The theme of this special issue is the formalization of commonsense reasoning, i.e. the kind of reasoning that people perform in their everyday lives. Its very name suggests that there is nothing much to it—everyone does it, so how hard can it be? It turns out however that commonsense reasoning is a rather intricate business, much harder to formalize than other more classical types of reasoning, such as mathematical reasoning. The main difficulty with commonsense reasoning is that, in contrast to expert reasoning (e.g. economic, legal, medical, etc.), much of the knowledge that is required for commonsense inferences is implicit. Take for example the following scenario: ‘John picked up the newspaper and walked to the kitchen. He made some coffee and started reading about last night's soccer match’. Based on this information alone, the average person would infer that John is now in the kitchen (and therefore he is not in the garden), drinking coffee and reading his newspaper, which is also in the kitchen, and which contains an article about a soccer match that took place the night before.

In this article we consider three different kinds of domain-dependent control knowledge (temporal, procedural and HTN-based) that are useful in planning. Our approach is declarative and relies on the language of logic programming with answer set semantics (AnsProlog*). AnsProlog* is designed to plan without control knowledge. We show how temporal, procedural and HTN-based control knowledge can be incorporated into AnsProlog* by the modular addition of a small number of domain-dependent rules, without the need to modify the planner. We formally prove the correctness of our planner, both in the absence and presence of the control knowledge. Finally, we perform some initial experimentation that demonstrates the potential reduction in planning time that can be achieved when procedural domain knowledge is used to solve planning problems with large plan length.

Two trends are emerging in the World Wide Web (WWW). The first is the proliferation of Web Services -- self-contained, Web-accessible software applications and associated distributed systems architectures. The second is the emergence of the "Semantic Web," the vision for a next-generation WWW that is computer interpretable. Today's Web was designed primarily for human use. To enable reliable, large-scale automated interoperation of Web services, their properties and capabilities must be understandable to a computer program. In this talk we briefy overview our ongoing work to develop a declarative language for describing Web services on the Semantic Web, contrasting it with emerging industrial Web service and Semantic Web standards. Our declarative representation of Web services enables automation of a wide variety of tasks including Web service discovery, invocation, interoperation, composition, simulation, verification and monitoring.To address the problem of automated Web service composition, we propose automated reasoning techniques based on the notion of generic procedures and customizing user constraint. To this end, we adapt and extend a logic programming language to enable programs that are generic, customizable and usable in the context of the Web. We combine these with deductive synthesis techniques to generate compositions of Web services. Further, we propose logical criteria for these generic procedures that define when they are knowledge self-sufficient and physically self-sufficient. To support information gathering combined with search, we propose a middle-ground interpreter that operates under an assumption of reasonable persistence of key information. Our implemented prototype system is currently interacting with services on the Web.Parts of this work were done in collaboration with Tran Cao Son and Honglei Zeng. The notion of semantic Web services is introduced in [3]. The origins of OWL-S, the OWL (Ontology Web Language) ontology for Web services are described as DAML-S in [1]. Up-to-date work on OWL-S can be found at [5]. Research on automated Web service composition can be found in [3, 2], with research on analysis, simulation and verification of Web services discussed in [4].

Two trends are emerging in the World Wide Web (WWW). The first is the proliferation of Web Services -- self-contained, Web-accessible software applications and associated distributed systems architectures. The second is the emergence of the the vision for a next-generation WWW that is computer interpretable. Today's Web was designed primarily for human use. To enable reliable, large-scale automated interoperation of Web services, their properties and capabilities must be understandable to a computer program. In this talk we briefy overview our ongoing work to develop a declarative language for describing Web services on the Semantic Web, contrasting it with emerging industrial Web service and Semantic Web standards. Our declarative representation of Web services enables automation of a wide variety of tasks including Web service discovery, invocation, interoperation, composition, simulation, verification and monitoring.To address the problem of automated Web service composition, we propose automated reasoning techniques based on the notion of generic procedures and customizing user constraint. To this end, we adapt and extend a logic programming language to enable programs that are generic, customizable and usable in the context of the Web. We combine these with deductive synthesis techniques to generate compositions of Web services. Further, we propose logical criteria for these generic procedures that define when they are knowledge self-sufficient and physically self-sufficient. To support information gathering combined with search, we propose a middle-ground interpreter that operates under an assumption of reasonable persistence of key information. Our implemented prototype system is currently interacting with services on the Web.Parts of this work were done in collaboration with Tran Cao Son and Honglei Zeng. The notion of semantic Web services is introduced in [3]. The origins of OWL-S, the OWL (Ontology Web Language) ontology for Web services are described as DAML-S in [1]. Up-to-date work on OWL-S can be found at [5]. Research on automated Web service composition can be found in [3, 2], with research on analysis, simulation and verification of Web services discussed in [4].

Web services-- Web-accessible programs and devices – are a key application area for the Semantic Web. With the proliferation of Web services and the evolution towards the Semantic Web comes the opportunity to automate various Web services tasks. Our objective is to enable markup and automated reasoning technology to describe, simulate, compose, test, and verify compositions of Web services. We take as our starting point the DAML-S DAML+OIL ontology for describing the capabilities of Web services. We define the semantics for a relevant subset of DAML-S in terms of a first-order logical language. With the semantics in hand, we encode our service descriptions in a Petri Net formalism and provide decision procedures for Web service simulation, verification and composition. We also provide an analysis of the complexity of these tasks under different restrictions to the DAML-S composite services we can describe. Finally, we present an implementation of our analysis techniques. This implementation takes as input a DAML-S description of a Web service, automatically generates a Petri Net and performs the desired analysis. Such a tool has broad applicability both as a back end to existing manual Web service composition tools, and as a stand-alone tool for Web service developers.

Integrating actions and state constraints is a central problem in knowledge representation. State constraints are commonly used to represent the relationship between objects in the world. When a representation of action is integrated, state constraints implicitly define indirect effects of actions and impose further preconditions on the performance of actions. Thus, a semantically correct integration of actions and state constraints must address the ramification and qualification problems, as well as the frame problem. In this paper we achieve such an integration for a syntactically restricted class of situation calculus theories. This paper presents two major technical contributions. The first contribution is an axiomatic closed-form solution to the frame, ramification and qualification problems for a common class of theories. The solution is presented in the form of an automatable procedure that compiles a syntactically restricted set of situation calculus ramification constraints and effect axioms into a set of successor state axioms. The second major contribution of this paper is an independent semantic justification for this closed-form solution. In particular, we present a semantic specification for a solution to the frame and ramification problems in terms of a prioritized minimization policy, and show that the successor state axioms of our closed-form solution adhere to this specification. Observing that our minimization policy is simply an instance of prioritized circumscription, we exploit results of Lifschitz (1985) on computing circumscription to show that computing the prioritized circumscription yields our successor state axioms. In the special case where there are no ramification constraints, computing the circumscription yields Reiter's (1991) earlier successor state axiom solution to the frame problem.

This paper describes a qualitative technique for interpreting graphical data. Given a set of numerical observations regarding the behaviour of a system, its attributes can be determined by plotting the data and qualitatively comparing the shape of the resulting graph with graphs of system behaviour models. Qualitative data modeling incorporates techniques from pattern recognition and qualitative reasoning to characterize observed data, generate hypothetical interpretations, and select models that best fit the shape of the data. Domain‐specific knowledge may be used to substantiate or refute the likelihood of hypothesized interpretations. The basic data modeling technique is domain independent and is applicable to a wide range of problems. It is illustrated here in the context of a knowledge‐based system for well test interpretation.