Multi-agent epistemic planning (MEP) is the task of generating action sequences that achieve goals specified over both the physical world and agents’ mental states. It plays an important role in research domains such as game theory, computational economics, and cognitive science. While dynamic epistemic logic (DEL) provides an expressive framework for MEP, it requires complete, model-based specifications of the initial state and action effects, and suffers from undecidability due to the unbounded nesting of beliefs. In this work, we propose a modal variant of the situation calculus that captures much of the expressive power of the DEL approach. Inspired by the cognitive concept Theory of Mind (ToM), we introduce action theories with hierarchical structures, allowing agents to reason about other agents' action theories up to bounded depths. We develop a regression method that reduces reasoning about future states to reasoning about the initial state. By preserving bounded-order ToM throughout the regression process, our approach ensures the decidability of the planning problem. Finally, we propose an algorithm to find the optimal solution, namely, to find the shortest action sequence that achieves the goal.

Belief-based programming is a probabilistic extension of the GOLOG program family where every action and sensing result can be noisy and every test condition refers to the agent’s subjective beliefs. Inherited from GOLOG programs, the action-centered feature makes belief programs fairly suitable for high-level robot control under uncertainty. An important step before deploying such a program is to verify whether it satisfies certain properties. At least two problems exist in verifying such programs: how to formally specify program properties and what is the complexity of the verification problem. In this paper, we propose a formalism for belief programs based on a modal logic of actions and beliefs which allows us to conveniently express PCTL-like temporal properties. We also investigate the decidability and undecidability of the verification problem.

The starting point of this paper is earlier work, where we proposed an epistemic logic which characterizes the beliefs of a knowledge-based agent in terms of increasing levels of complexity. At the lowest level, the agent is only able to draw simple conclusions from its knowledge base. Higher levels lead to more and more inferences and computing the beliefs at any particular level turns out to be tractable. What makes this logic arguably appealing is the fact that the underlying semantics is based on possible worlds. However, the work is still limited in that only beliefs about what is true in the world are considered, that is, an agent's beliefs about its own beliefs are ignored. In this paper we will close this gap and generalize the earlier work by proposing a model of limited belief where an agent is able to fully introspect on its own beliefs without sacrificing tractability.

Logical image understanding involves interpreting and reasoning about the relationships and consistency within an image's visual content. This capability is essential in applications such as industrial inspection, where logical anomaly detection is critical for maintaining high-quality standards and minimizing costly recalls. Previous research in anomaly detection (AD) has relied on prior knowledge for designing algorithms, which often requires extensive manual annotations, significant computing power, and large amounts of data for training. Autoregressive, multimodal Vision Language Models (AVLMs) offer a promising alternative due to their exceptional performance in visual reasoning across various domains. Despite this, their application to logical AD remains unexplored. In this work, we investigate using AVLMs for logical AD and demonstrate that they are well-suited to the task. Combining AVLMs with format embedding and a logic reasoner, we achieve SOTA performance on public benchmarks, MVTec LOCO AD, with an AUROC of 86.0% and an F1-max of 83.7% along with explanations of the anomalies. This significantly outperforms the existing SOTA method by 18.1% in AUROC and 4.6% in F1-max score.

It is known that a simple numeric planning problem (SNP) with one numeric variable is decidable but undecidable with three (Helmert 2002). A more recent result (Gnad et. al 2023) showed undecidability for two numeric and one propositional variable. In this paper, we show the decidability of SNP with exactly two numeric variables. For this, we first partition the state space into a finite number of regions and demonstrate the decidability of SNP when restricted to any of these regions. Afterwards, we develop a correct search algorithm that abstracts from these regions by tracking an infinite number of states following an arithmetic progression pattern. Finally, we prove termination of the search and draw conclusions about the reasons for undecidability for general SNP.

This work develops an approach to qualitative belief revision in a fully probabilistic setting. We begin with a logic where possible worlds are assigned probabilities. In this logic an agent may believe a formula is true even though the subjective probability of the formula is less than 1.0. Similarly, after revision by a formula ϕ, the agent will believe ϕ is true, even though the agent’s subjective probability of ϕ may be less than 1.0. We establish a correspondence with the hallmark AGM postulates for belief revision. Moreover, we use Jeffrey Conditionalisation to establish a link with iterated belief change. To this end, we develop an approach that satisfies appropriately modified Darwiche-Pearl postulates (with clear justification). Thus, we provide a connection between quantitative probabilistic approaches on the one hand and the qualitative formulation of belief change, on the other. This work holds potential for the development of practical belief revision systems by applying a (qualitative) approach to belief change in probabilistic, uncertain domains.

Belief-based programming is a probabilistic extension of the GOLOG program family where every action and sensing result can be noisy and every test condition refers to the agent’s subjective beliefs. Inherited from GOLOG programs, the action-centered feature makes belief programs fairly suitable for high-level robot control under uncertainty. An important step before deploying such a program is to verify whether it satisfies certain properties. At least two problems exist in verifying such programs: how to formally specify program properties and what is the complexity of the verification problem. In this paper, we propose a formalism for belief programs based on a modal logic of actions and beliefs which allows us to conveniently express PCTL-like temporal properties. We also investigate the decidability and undecidability of the verification problem.

In this paper, we first define numeric additive planning (NAP), a planning formulation equivalent to Hoffmann's Restricted Tasks over Integers. Then, we analyze the minimal number of action repetitions required for a solution, since planning turns out to be decidable as long as such numbers can be calculated for all actions. We differentiate between two kinds of repetitions and solve for one by integer linear programming and the other by search. Additionally, we characterize the differences between propositional planning and NAP regarding these two kinds. To achieve this, we define so-called multi-valued partial order plans, a novel compact plan representation. Finally, we consider decidable fragments of NAP and their complexity.

Many initiatives aim at answering the challenges of the fourth industrial revolution (Industry 4.0). A key aspect of these initiatives is the connectivity of the different industrial entities. Communication and information exchange between entities usually flows in two dimensions; a vertical one, that spans the different levels of abstraction within the company, and a horizontal one connecting the different entities in the supply chain. In contrast, the Internet of Production (IoP) presents the World Wide Lab (WWL) allowing an extra dimension of communication, which we call the cross-company dimension. Hence, the WWL integrates the different entities within and across potentially competing labs and companies. The WWL leverages and aggregates accessible production data fostering an exchange of information, that prevents redundant experimentation and increases quality of data-driven models by including data from diverse manufacturing settings. This paper discusses work done towards this vision and technical, economic, social, legal, and ethical challenges the WWL faces and provides a roadmap towards infrastructuring the WWL.

Belief-based programming is a probabilistic extension of the Golog programming language family, where every action and sensing could be noisy and every test refers to the subjective beliefs of the agent. Such characteristics make it rather suitable for robot control in a partial-observable uncertain environment. Recently, efforts have been made in providing formal semantics for belief programs and investigating the hardness of verifying belief programs. Nevertheless, a general algorithm that actually conducts the verification is missing. In this paper, we propose an algorithm based on symbolic dynamic programming to verify belief programs, an approach that generalizes the dynamic programming technique for solving (partially observable) Markov decision processes, i.e. (PO)MDP, by exploiting the symbolic structure in the solution of first-order (PO)MDPs induced by belief program execution.

The unification of logic and probability has been seen as a long-standing concern in philosophy and mathematical logic. In this paper, we propose a new general probabilistic modal logic of belief and only-believing in the situation calculus. Our logic can express both continuous and discrete degrees of belief. More importantly, expressing degrees of belief for arbitrary first-order formulas in a dynamic setting is possible for the first time, going well beyond previous proposals where fluents are assumed to be nullary or discrete. We show that our notion of belief retains many of the properties known from the previous related work.

Fast paced industry requirements call for fast and easy robot programming, especially for Small and Medium sized Enterprises (SME) that often lack robot programming experience. Even with the advancement of graphical activity representation languages such as Behaviour Trees (BTs), it can still be time consuming to program robots for new behaviors due to the shifting product specifications and the dynamic production environments. This paper presents an extension of BTs that offers more flexibility as well as higher reactivity and robustness by introducing Mixed Initiative Planning (MIP) to BTs using Dynamic Sequence Nodes (DSNs). DSNs reduce the human effort needed to design a BT as well as the number of nodes to achieve a certain task while maintaining robustness, readability, and modularity of the tree. Additionally, it introduces run-time optimization to BTs, as opposed to tree synthesis approaches that guarantee convergence but overlook performance.

A major challenge in AI is dealing with uncertain information. While probabilistic approaches have been employed to address this issue, in many situations probabilities may not be available or may be unsuitable. As an alternative, qualitative approaches have been introduced to express that one event is no more probable than another. We provide an approach where an agent may reason deductively about notions of likelihood, and may hold beliefs where the subjective probability for a belief is less than 1. Thus, an agent can believe that p holds (with probability <1); and if the agent believes that q is more likely than p, then the agent will also believe q. Our language allows for arbitrary nesting of beliefs and qualitative likelihoods. We provide a sound and complete proof system for the logic with respect to an underlying probabilistic semantics, and show that the language is equivalent to a sublanguage with no nested modalities.

The Industrial Internet-of-Things (IIoT) promises significant improvements for the manufacturing industry by facilitating the integration of manufacturing systems by Digital Twins. However, ecological and economic demands also require a cross-domain linkage of multiple scientific perspectives from material sciences, engineering, operations, business, and ergonomics, as optimization opportunities can be derived from any of these perspectives. To extend the IIoT to a trueInternet of Production, two concepts are required: first, a complex, interrelated network of Digital Shadows which combine domain-specific models with data-driven AI methods; and second, the integration of a large number of research labs, engineering, and production sites as a World Wide Lab which offers controlled exchange of selected, innovation-relevant data even across company boundaries. In this article, we define the underlying Computer Science challenges implied by these novel concepts in four layers:Smart human interfacesprovide access to information that has been generated bymodel-integrated AI. Given the large variety of manufacturing data, newdata modelingtechniques should enable efficient management of Digital Shadows, which is supported by aninterconnected infrastructure. Based on a detailed analysis of these challenges, we derive a systematized research roadmap to make the vision of the Internet of Production a reality.

Yiran Xing, Zai Shi, Zhao Meng, Gerhard Lakemeyer, Yunpu Ma, Roger Wattenhofer. Proceedings of the 59th Annual Meeting of the Association for Computational Linguistics and the 11th International Joint Conference on Natural Language Processing (Volume 1: Long Papers). 2021.

When faced with an execution failure, an intelligent robot should be able to identify the likely reasons for the failure and adapt its execution policy accordingly. This paper addresses the question of how to utilise knowledge about the execution process, expressed in terms of learned constraints, in order to direct the diagnosis and experience acquisition process. In particular, we present two methods for creating a synergy between failure diagnosis and execution model learning. We first propose a method for diagnosing execution failures of parameterised action execution models, which searches for action parameters that violate a learned precondition model. We then develop a strategy that uses the results of the diagnosis process for generating synthetic data that are more likely to lead to successful execution, thereby increasing the set of available experiences to learn from. The diagnosis and experience correction methods are evaluated for the problem of handle grasping, such that we experimentally demonstrate the effectiveness of the diagnosis algorithm and show that corrected failed experiences can contribute towards improving the execution success of a robot.

Plan execution on a mobile robot is inherently error-prone, as the robot needs to act in a physical world which can never be completely controlled by the robot. If an error occurs during execution, the true world state is unknown, as a failure may have unobservable consequences. One approach to deal with such failures is diagnosis, where the true world state is determined by identifying a set of faults based on sensed observations. In this paper, we present a novel approach to explanatory diagnosis, based on the assumption that most failures occur due to some robot hardware failure. We model the robot platform components with state machines and formulate action variants for the robots' actions, modelling different fault modes. We apply diagnosis as planning with a top-k planning approach to determine possible diagnosis candidates and then use active diagnosis to find out which of those candidates is the true diagnosis. Finally, based on the platform model, we recover from the occurred failure such that the robot can continue to operate. We evaluate our approach in a logistics robots scenario by comparing it to having no diagnosis and diagnosis without platform models, showing a significant improvement to both alternatives.

In a recent paper Belle and Lakemeyer proposed the logic DS, a probabilistic extension of a modal variant of the situation calculus with a model of belief based on weighted possible worlds. Among other things, they were able to precisely capture the beliefs of a probabilistic knowledge base in terms of the concept of only-believing. While intuitively appealing, the logic has a number of shortcomings. Perhaps the most severe is the limited expressiveness in that degrees of belief are restricted to constant rational numbers, which makes it impossible to express arbitrary belief distributions. In this paper we will address this and other shortcomings by extending the language and modifying the semantics of belief and only-believing. Among other things, we will show that belief retains many but not all of the properties of DS. Moreover, it turns out that only-believing arbitrary sentences, including those mentioning belief, is uniquely satisfiable in our logic. For an interesting class of knowledge bases we also show how reasoning about beliefs and meta-beliefs after performing noisy actions and sensing can be reduced to reasoning about the initial beliefs of an agent using a form of regression.

Task planning for mobile robots typically uses an abstract planning domain that ignores the low-level details of the specific robot platform. Therefore, executing a plan on an actual robot often requires additional steps to deal with the specifics of the robot platform. Such a platform can be modeled with timed automata and a set of temporal constraints that need to be satisfied during execution. In this paper, we describe how to transform an abstract plan into a platform-specific action sequence that satisfies all platform constraints. The transformation procedure first transforms the plan into a timed automaton, which is then combined with the platform automata while removing all transitions that violate any constraint. We then apply reachability analysis on the resulting automaton. From any solution trace one can obtain the abstract plan extended by additional platform actions such that all platform constraints are satisfied. We describe the transformation procedure in detail and provide an evaluation in two real-world robotics scenarios.

When an autonomous robot learns how to execute actions, it is of interest to know if and when the execution policy can be generalised to variations of the learning scenarios. This can inform the robot about the necessity of additional learning, as using incomplete or unsuitable policies can lead to execution failures. Generalisation is particularly relevant when a robot has to deal with a large variety of objects and in different contexts. In this paper, we propose and analyse a strategy for generalising parameterised execution models of manipulation actions over different objects based on an object ontology. In particular, a robot transfers a known execution model to objects of related classes according to the ontology, but only if there is no other evidence that the model may be unsuitable. This allows using ontological knowledge as prior information that is then refined by the robot’s own experiences. We verify our algorithm for two actions - grasping and stowing everyday objects - such that we show that the robot can deduce cases in which an existing policy can generalise to other objects and when additional execution knowledge has to be acquired.

For robots acting in human-centered environments, the ability to improve based on experience is essential for reliable and adaptive operation; however, particularly in the context of robot failure analysis, experience-based improvement is practically useful only if robots are also able to reason about and explain the decisions they make during execution. In this paper, we describe and analyse a representation of execution-specific knowledge that combines (i) a relational model in the form of qualitative attributes that describe the conditions under which actions can be executed successfully and (ii) a continuous model in the form of a Gaussian process that can be used for generating parameters for action execution, but also for evaluating the expected execution success given a particular action parameterisation. The proposed representation is based on prior, modelled knowledge about actions and is combined with a learning process that is supervised by a teacher. We analyse the benefits of this representation in the context of two actions - grasping handles and pulling an object on a table -such that the experiments demonstrate that the joint relational-continuous model allows a robot to improve its execution based on experience, while reducing the severity of failures experienced during execution.

In a recent paper Lakemeyer and Levesque proposed a first-order logic of limited belief to characterize the beliefs of a knowledge base (\KB). Among other things, they show that their model of belief is expressive, eventually complete, and tractable. This means, roughly, that a \KB\ may consist of arbitrary first-order sentences, that any sentence which is logically entailed by the \KB\ is eventually believed, given enough reasoning effort, and that reasoning is tractable under reasonable assumptions. One downside of the proposal is that epistemic states are defined in terms of sets of clauses, possibly containing variables, giving the logic a distinct syntactic flavour compared to the more traditional possible-world semantics found in the literature on epistemic logic. In this paper we show that the same properties as above can be obtained by defining epistemic states as sets of three-valued possible worlds. This way we are able to shed new light on those properties by recasting them using the more familiar notion of truth over possible worlds.

Action extraction from teleoperated robots can be a crucial step in the direction of full -or shared- autonomy of tasks where human experience is indispensable. This is especially important in tasks that seek dynamic goals, where a human operator needs more control on how the machine behaves to provide assistance or perform a task. Open-die forging is a basic metal-forming process that lacks non-destructive product quality measures. Human experience is therefore imperative. During the process, a robot-arm is operated to place the work-piece between the dies of the forge where it is striked several times to reach a specific geometry. In this paper, we apply a white-box computer vision technique to discretize open-die forging robot-arm teleoperation data into actions as a step in learning the operator's behavior.

One of the main objectives of production planning is to minimize the usage of resources and manufacturing-related costs while meeting the customer's requirements, such as delivery dates and quality. Production planners deal with various scheduling problems that are often NP-hard and can not be optimally solved by humans. Solving such problems often relies on methods from the Operations Research (OR) field. Recently, Neural Combinatorial Optimization (NCO) has emerged as a promising field of research that aims at tackling different optimization tasks using the latest advancements in machine learning, including deep reinforcement learning. These methods can be successfully used for short-term production planning because of their flexibility and speed. In this paper, we examine the applicability and scalability of neural combinatorial optimization methods in the context of production planning. We define an evaluation metric to investigate the stability and quality of the solutions. Furthermore, we develop an experimental setup allowing to compare various approaches for production scheduling with sequence-dependent setup costs under real-world production conditions. Although an optimality gap is observed when compared to established OR methods, our experiments demonstrate the superiority of NCO in terms of scheduling time.

In the production industry, the volume, variety, and velocity of data as well as the number of deployed protocols increase exponentially due to the influences of the Internet-of-Things (IoT) advances. While hundreds of isolated solutions exist to utilize these data, e.g., optimizing processes or monitoring machine conditions, the lack of a unified data handling and exchange mechanism hinders the implementation of approaches to improve the quality of decisions and processes in such an interconnected environment. The vision of anInternet of Productionpromises the establishment of aWorldwide Lab, where data from every process in the network can be utilized, even interorganizational and across domains. While numerous existing approaches consider interoperability from an interface and communication system perspective, fundamental questions of data and information interoperability remain insufficiently addressed. In this article, we identifytenkey issues, derived from three distinctive real-world use cases that hinder large-scale data interoperability for industrial processes. Based on these issues, we derive a set offivekey requirements for future (IoT) data layers, building upon the FAIR data principles. We propose to address them by creatingFactDAG, a conceptual data layer model for maintaining a provenance-based, directed acyclic graph of facts, inspired by successful distributed version-control and collaboration systems. Eventually, such a standardization should greatly shape the future of interoperability in an interconnected production industry.

In knowledge representation, obtaining a notion of belief which is tractable, expressive, and eventually complete has been a somewhat elusive goal. Expressivity here means that an agent should be able to hold arbitrary beliefs in a very expressive language like that of first-order logic, but without being required to perform full logical reasoning on those beliefs. Eventual completeness means that any logical consequence of what is believed will eventually come to be believed, given enough reasoning effort. Tractability in a first-order setting has been a research topic for many years, but in most cases limitations were needed on the form of what was believed, and eventual completeness was so far restricted to the propositional case. In this paper, we propose a novel logic of limited belief, which has all three desired properties.

When it comes to robotic agents operating in an uncertain world, a major concern in knowledge representation is to better relate high-level logical accounts of belief and action to the low-level probabilistic sensorimotor data. Perhaps the most general formalism for dealing with degrees of belief and, in particular, how such beliefs should evolve in the presence of noisy sensing and acting is the account by Bacchus, Halpern, and Levesque. In this paper, we reconsider that model of belief, and propose a new logical variant that has much of the expressive power of the original, but goes beyond it in novel ways. In particular, by moving to a semantical account of a modal variant of the situation calculus based on possible worlds with unbounded domains and probabilistic distributions over them, we are able to capture the beliefs of a fully introspective knowledge base with uncertainty by way of an only-believing operator. The paper introduces the new logic and discusses key properties as well as examples that demonstrate how the beliefs of a knowledge base change as a result of noisy actions.

Only knowing captures the intuitive notion that the beliefs of an agent are precisely those that follow from its knowledge base. It has previously been shown to be useful in characterizing knowledge-based reasoners, especially in a quantified setting. While this allows us to reason about incomplete knowledge in the sense of not knowing whether a formula is true or not, there are many applications where one would like to reason about the degree of belief in a formula. In this work, we propose a new general first-order account of probability and only knowing that admits knowledge bases with incomplete and probabilistic specifications. Beliefs and non-beliefs are then shown to emerge as a direct logical consequence of the sentences of the knowledge base at a corresponding level of specificity.

To solve ever more complex and longer tasks, mobile robots need to generate more elaborate plans and must handle dynamic environments and incomplete knowledge. We address this challenge by integrating two seemingly different approaches — PDDL-based planning for efficient plan generation and Golog for highly expressive behavior specification — in a coherent framework that supports continual planning. The latter allows to interleave plan generation and execution through assertions, which are placeholder actions that are dynamically expanded into conditional sub-plans (using classical planners) once a replanning condition is satisfied. We formalize and implement continual planning in Golog which was so far only supported in PDDL-based systems. This enables combining the execution of generated plans with regular Golog programs and execution monitoring. Experiments on autonomous mobile robots show that the approach supports expressive behavior specification combined with efficient sub-plan generation to handle dynamic environments and incomplete knowledge in a unified way.

Mobile robots should perform a growing number of tasks and react to time-critical events. Thus, the ability to interrupt a task and resume it later is crucial. While interleaved execution occurs often in robotics, existing approaches do not consider the fact that interrupting a task and resuming an interrupted task often requires intermediate steps. In this paper we present an approach to interruptible task execution with resumption. We propose INTRGOLOG which extends INDIGOLOG by task interruption and resumption through introducing new constructs to determine and fulfill the requirements of tasks. Our experiments on a service robot and in simulation show that the ability to switch to another task enables a robot to react in a swift and reliable fashion to new events.

In a series of papers, Liu, Lakemeyer, and Levesque address the problem of decidable reasoning in expressive first-order knowledge bases. Here, we extend their ideas to accommodate conditional beliefs, as in “if she is Australian, then she presumably eats Kangaroo meat.” Perhaps the most prevalent semantics of a conditional belief is to evaluate the consequent in the most-plausible worlds consistent with the premise. In this paper, we devise a technique to approximate this notion of plausibility, and complement it with Liu, Lakemeyer, and Levesque's weak inference. Based on these ideas, we develop a logic of limited conditional belief, and provide soundness, decidability, and (for the propositional case) tractability results.

Robot sensors are usually subject to error. Since in many practical scenarios a probabilistic error model is not available, sensor readings are often dealt with in a hard-coded, heuristic fashion. In this paper, we propose a logic to address the problem from a KR perspective. In this logic, the epistemic effect of sensing actions is deferred to so-called fusion actions, which may resolve discrepancies and inconsistencies of recent sensing results. Moreover, a local closed-world assumption can be applied dynamically. When needed, this assumption can be revoked and fusions can be undone using a form of forgetting.

In this paper, we report on our entry for the AI Birds competition, where we designed, implemented, and evaluated an agent for the physics puzzle computer game Angry Birds. Our agent uses search and simulation to find appropriate parameters for launching birds. While there are other methods that focus on qualitative reasoning about physical systems we try to combine simulation and adjustable abstractions to efficiently traverse the possibly infinite search space. The agent features a hierarchical search scheme where different levels of abstractions are used. At any level, it uses simulation to rate subspaces that should be further explored in more detail on the next levels. We evaluate single components of our agent and we also compare the overall performance of different versions of our agent. We show that our approach yields a competitive solution on the standard set of levels.

A fundamental task in reasoning about action and change is projection, which refers to determining what holds after a number of actions have occurred. A powerful method for solving the projection problem is regression, which reduces reasoning about the future to reasoning about the initial state. In particular, regression has played an important role in the situation calculus and its epistemic extensions. Recently, a modal variant of the situation calculus was proposed, which allows an agent to revise its beliefs based on so-called belief conditionals as part of its knowledge base. In this paper, we show how regression can be extended to reduce beliefs about the future to initial beliefs in the presence of belief conditionals. Moreover, we show how any remaining belief operators can be eliminated as well, thus reducing the belief projection problem to ordinary first-order entailments.

The RoboCup Logistics League (RCLL) has seen major rule changes increasing the complexity, e.g. by raising the number of product variants from 3 to almost 250, and introducing new challenges like the handling of physical processing machines. We describe various aspects of our system that allowed to improve the performance in 2015 and our efforts to advance the league as a whole. These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

In the RoboCup Logistics League (RCLL), games are governed by a semi-autonomous referee box. It also records tremendous amounts of data about state changes of the game or communication with the robots. In this paper, we analyze the data of the 2014 competition by means of Key Performance Indicators (KPI). KPIs are used in industrial environments to evaluate the performance of production systems. Applying adapted KPIs to the RCLL provides interesting insights about the strategies of the robot teams. When aiming for more realistic industrial properties with a 24/7 production, where teams perform shifts (without intermediate environment reset), KPIs could be a means to score the game. This could be tried first in a simulation sub-league. These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

The action programming language GOLOG has been found useful for the control of autonomous agents such as mobile robots. In scenarios like these, tasks are often open-ended so that the respective control programs are non-terminating. Before deploying such programs on a robot, it is often desirable to verify that they meet certain requirements. For this purpose, Claßen and Lakemeyer recently introduced algorithms for the verification of temporal properties of GOLOG programs. However, given the expressiveness of GOLOG, their verification procedures are not guaranteed to terminate. In this paper, we show how decidability can be obtained by suitably restricting the underlying base logic, the effect axioms for primitive actions, and the use of actions within GOLOG programs. Moreover, we show that dropping any of these restrictions immediately leads to undecidability of the verification problem.

Recently Shapiro et al. explored the notion of iterated belief revision within Reiter's version of the situation calculus. In particular, they consider a notion of belief defined as truth in the most plausible situations. To specify what an agent is willing to believe at different levels of plausibility they make use of so-called belief conditionals, which themselves neither refer to situations or plausibilities explicitly. Reasoning about such belief conditionals turns out to be complex because there may be too many models satisfying them and negative belief conditionals are also needed to obtain the desired conclusions. In this paper we show that, by adopting a notion of only-believing, these problems can be overcome. The work is carried out within a modal variant of the situation calculus with a possible-world semantics which features levels of plausibility. Among other things, we show that only-believing a knowledge base together with belief conditionals always leads to a unique model, which allows characterizing the beliefs of an agent, after any number of revisions, in terms of entailments within the logic.

The idea of "only knowing" a collection of sentences, as proposed by Levesque, has been previously shown to be very useful in characterizing knowledge-based agents: in terms of a specification, a precise and perspicuous account of the beliefs and non-beliefs is obtained in a monotonic setting. Levesque's logic is based on a first-order modal language with quantifying-in, thus allowing for de re versus de dicto distinctions, among other things. However, the logic and its recent dynamic extension only deal with the case of a single agent. In this work, we propose a first-order multiagent framework with knowledge, actions, sensing and only knowing, that is shown to inherit all the features of the single agent version. Most significantly, we prove reduction theorems by means of which reasoning about knowledge and actions in the framework simplifies to non-epistemic, non-dynamic reasoning about the initial situation.

During operation of robots large amounts of data are produced and processed for instance in perception, actuation, or decision making. Nowadays this data is typically volatile and disposed right after use. But this data can be valuable and useful later. Therefore we propose a database system that taps into common robot middleware to record any and all data produced at run-time. We present two examples using this data in fault analysis and performance evaluation and describe real-world experiments run on the domestic service robot HERB.

Building on a general theory of action by Reiter and his colleagues, Bacchus et al. give an account for formalizing degrees of belief and noisy actions in the situation calculus. Unfortunately, there is no clear solution to the projection problem for the formalism. And, while the model has epistemic features, it is not obvious what the agent's knowledge base should look like. Also, reasoning about uncertainty essentially resorts to second-order logic. In recent work, Gabaldon and Lakemeyer remedy these shortcomings somewhat, but here too the utility seems to be restricted to queries (with action operators) about the initial theory. In this paper, we propose a fresh amalgamation of a modal fragment of the situation calculus and uncertainty, where the idea will be to update the initial knowledge base, containing both ordinary and (certain kinds of) probabilistic beliefs, when noisy actions are performed. We show that the new semantics has the right properties, and study a special case where updating probabilistic beliefs is computable. Our ideas are closely related to the Lin and Reiter notion of progression.

In a seminal paper, Lin and Reiter introduced the notion of progression of basic action theories. Unfortunately, progression is second-order in general. Recently, Liu and Lakemeyer improve on earlier results and show that for the local-effect and normal actions case, progression is computable but may lead to an exponential blow-up. Nevertheless, they show that for certain kinds of expres-sive first-order knowledge bases with disjunctive infor-mation, called proper+, it is efficient. However, answer-ing queries about the resulting state is still undecidable. In this paper, we continue this line of research and extend proper+ KBs to include functions. We prove that their progression wrt local-effect, normal actions, and range-restricted theories, is first-order definable and efficiently computable. We then provide a new logically sound and complete decision procedure for certain kinds of queries.

Approaches to reasoning about knowledge in imperfect information games typically involve an exhaustive description of the game, the dynamics characterized by a tree and the incompleteness in knowledge by information sets. Such specifications depend on a modeler's intuition, are tedious to draft and vague on where the knowledge comes from. Also, formalisms proposed so far are essentially propositional, which, at the very least, makes them cumbersome to use in realistic scenarios. In this paper, we propose to model imperfect information games in a new multi-agent epistemic variant of the situation calculus. By using the concept of only-knowing, the beliefs and non-beliefs of players after any sequence of actions, sensing or otherwise, can be characterized as entailments in this logic. We show how de re vs. de dicto belief distinctions come about in the framework. We also obtain a regression theorem for multi-agent beliefs, which reduces reasoning about beliefs after actions to reasoning about beliefs in the initial situation.

The agent programming language GOLOG and the underlying Situation Calculus have become popular means for the modelling and control of autonomous agents such as mobile robots. Although such agents' tasks are typically open-ended, little attention has been paid so far to the analysis of non-terminating GOLOG control programs. Recently we therefore introduced a logic that allows to express properties of Golog programs using operators from temporal logics while retaining the full first-order expressiveness of the Situation Calculus. Combining ideas from classical symbolic model checking with first-order theorem proving we presented a verification method for a restricted subclass of temporal properties. In this paper, we extend this work by considering arbitrary temporal formulas. Our algorithm is inspired by classical 𝒞𝒯ℒ* model checking, but introduces techniques to cope with arbitrary first-order quantification.

High-level behaviour specification of an intelligent autonomous agent or robot is a non-trivial task. Various approaches exist some of which try to combine different paradigms like programming and planning. In this paper, we show how to integrate fuzzy logic controllers into the logic-based programming language Golog. Golog already allows for combining programming and planning. By adding the instrument of fuzzy controllers we provide the means to have a natural specification of rules for tasks that require a high amount of reactivity. Since the facilities already present in Golog remain, we add to an already powerful framework thus expanding the applicability of Golog for high-level behaviour specification of a robot or agent.

Levesque proposed a generalization of a database called a proper knowledge base (KB), which is equivalent to a possibly infinite consistent set of ground literals. In contrast to databases, proper KBs do not make the closed-world assumption and hence the entailment problem becomes undecidable. Levesque then proposed a limited but efficient inference method V for proper KBs, which is sound and, when the query is in a certain normal form, also logically complete. He conjectured that for every first-order query there is an equivalent one in normal form. In this note, we show that this conjecture is false. In fact, we show that any class of formulas for which V is complete must be strictly less expressive than full first-order logic. Moreover, in the propositional case it is very unlikely that a formula always has a polynomial-size normal form.

Recently, viewpoint resolution methods which make conflicts productive have gained popularity in requirements engineering for organizational information systems. However, when extending such methods beyond organizational boundaries to social networks, sociological research indicates that a delicate balance of trust in individuals, confidence in the network as a whole, and watchful distrust becomes a key success factor. We capture these relationships in the so-called TCD (Trust-Confidence-Distrust) approach and demonstrate how this approach can be supported by a dynamic requirements engineering environment that combines the structural analysis of strategic dependencies and rationales, with the interaction between planning, tracing, and communicative action. An example drawn from an ongoing case study in entrepreneurship networks illustrates our approach.

Levesque introduced a notion of ‘only knowing’, with the goal of capturing certain types of non‐monotonic reasoning. Levesque's logic dealt with only the case of a single agent. Recently, both Halpern and Lakemeyer independently attempted to extend Levesque's logic to the multi‐agent case. Although there are a number of similarities in their approaches, there are some significant differences. In this paper, we re‐examine the notion of only knowing, going back to first principles. In the process, we simplify Levesque's completeness proof, and point out some problems with the earlier definitions. This leads us to reconsider what the properties of only knowing ought to be. We provide an axiom system that captures our desiderata, and show that it has a semantics that corresponds to it. The axiom system has an added feature of interest: it includes a modal operator for satisfiability, and thus provides a complete axiomatization for satisfiability in the logic K45.