abstractThis chapter is to provide a tutorial and pointers to results and related work on timed automata with a focus on semantical and algorithmic aspects of verification tools. We present the concrete and abstract semantics of timed automata (based on transition rules, regions and zones), decision problems, and algorithms for verification. A detailed description on DBM (Difference Bound Matrices) is included, which is the central data structure behind several verification tools for timed systems. As an example, we give a brief introduction to the tool Uppaal.
booktitleLectures on Concurrency and Petri Nets: Advances in Petri Nets
shorttitleTimed Automata
titleTimed Automata: Semantics, Algorithms and Tools

abstractWe consider $\mu$L, $\mu$La, and $\mu$Lp, three variants of the first-order $\mu$-calculus studied in verification of data-aware processes, that differ in the form of quantification on objects across states. Each of these three logics has a distinct notion of bisimulation. We show that the three notions collapse for generic dynamic systems, which include all state-based systems specified using a logical formalism, e.g., the situation calculus. Hence, for such systems, $\mu$L, $\mu$La, and $\mu$Lp have the same expressive power. We also show that, when the dynamic system stores only a bounded number of objects in each state (e.g., for bounded situation calculus action theories), a finite abstraction can be constructed that is faithful for $\mu$L (the most general variant), yielding decidability of verification. This contrasts with the undecidability for first-order ltl, and notably implies that first-order ltl cannot be captured by $\mu$L.
journaltitleInformation and Computation
shortjournalInformation and Computation
titleFirst-Order $\mu$-Calculus over Generic Transition Systems and Applications to the Situation Calculus
First-order -calculus,Infinite transition systems,Reasoning about actions,Situation calculus,State-bounded transition systems,Verification

booktitleProceedings of the 31st International Joint Conference on Artificial Intelligence (IJCAI)
titleVerification and Monitoring for First-Order LTL with Persistence-Preserving Quantification over Finite and Infinite Traces

abstractTemporally 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.
booktitleProceedings of the 31st AAAI Conference on Artificial Intelligence (AAAI)
shorttitleNon-Deterministic Planning with Temporally Extended Goals
titleNon-Deterministic Planning with Temporally Extended Goals: LTL over Finite and Infinite Traces

abstractLTL synthesis is the task of generating a strategy that satisfies a Linear Temporal Logic (LTL) specification interpreted over infinite traces. In this paper we examine the problem of LTLf synthesis, a variant of LTL synthesis where the specification of the behaviour of the strategy we generate is interpreted over finite traces – similar to the assumption we make in many planning problems, and important for the synthesis of business processes and other system interactions of finite duration. Existing approaches to LTLf synthesis transform LTLf into deterministic finite-state automata (DFA) and reduce the synthesis problem to a DFA game. Unfortunately, the DFA transformation is worst-case double-exponential in the size of the formula, presenting a computational bottleneck. In contrast, our approach exploits non-deterministic automata, and we reduce the synthesis problem to a non-deterministic planning problem. We leverage our approach not only for strategy generation but also to generate certificates of unrealizability – the first such method for LTLf. We employ a battery of techniques that exploit the structure of the LTLf specification to improve the efficiency of our transformation to automata. We combine these techniques with lazy determinization of automata and on-the-fly state abstraction. We illustrate the effectiveness of our approach on a set of established LTL synthesis benchmarks adapted to finite LTL.
booktitleTwenty-Eighth International Conference on Automated Planning and Scheduling (ICAPS)
titleFinite LTL Synthesis as Planning

Berlin, Heidelberg

abstractWe have shown that it is possible to automatically synthesize the synchronization skeleton of a concurrent program from a Temporal Logic specification. We believe that this approach may in the long run turn out to be quite practical. Since synchronization skeletons are, in general, quite small, the potentially exponential behavior of our algorithm need not be an insurmountable obstacle. Much additional research will be needed, however, to make the approach feasible in practice.
booktitleLogics of Programs
titleDesign and Synthesis of Synchronization Skeletons Using Branching Time Temporal Logic
Critical Section,Decision Procedure,Model Checker,Successor State,Temporal Logic

abstractTuring Lecture from the winners of the 2007 ACM A.M. Turing Award. In 1981, Edmund M. Clarke and E. Allen Emerson, working in the USA, and Joseph Sifakis working independently in France, authored seminal papers that founded what has become the highly successful field of model checking. This verification technology provides an algorithmic means of determining whether an abstract model—representing, for example, a hardware or software design—satisfies a formal specification expressed as a temporal logic (TL) formula. Moreover, if the property does not hold, the method identifies a counterexample execution that shows the source of the problem. The progression of model checking to the point where it can be successfully used for complex systems has required the development of sophisticated means of coping with what is known as the state explosion problem. Great strides have been made on this problem over the past 28 years by what is now a very large international research community. As a result many major hardware and software companies are beginning to use model checking in practice. Examples of its use include the verification of VLSI circuits, communication protocols, software device drivers, real-time embedded systems, and security algorithms. The work of Clarke, Emerson, and Sifakis continues to be central to the success of this research area. Their work over the years has led to the creation of new logics for specification, new verification algorithms, and surprising theoretical results. Model checking tools, created by both academic and industrial teams, have resulted in an entirely novel approach to verification and test case generation. This approach, for example, often enables engineers in the electronics industry to design complex systems with considerable assurance regarding the correctness of their initial designs. Model checking promises to have an even greater impact on the hardware and software industries in the future. —Moshe Y. Vardi, Editor-in-Chief
journaltitleCommunications of the ACM
shortjournalCommun. ACM
shorttitleModel Checking
titleModel Checking: Algorithmic Verification and Debugging

San Francisco, CA, USA

Morgan Kaufmann Publishers Inc.

booktitleProceedings of the 8th International Conference on Principles of Knowledge Representation and Reasoning (KR)
titleReasoning about Actions and Planning in LTL Action Theories

abstractThe authors describe an implemented integrated system allowing a mobile robot to plan its actions, taking into account temporal constraints, and to control their execution in real time. The general architecture has three levels, and the approach is related to hierarchical planning: the plan produced by the temporal planner is further refined at the control level, which in turn supervises its execution by a functional level. The framework of the French Mars Rover project VAP is used as an illustration of the various aspects discussed.$<>$
booktitleProceedings 1992 IEEE International Conference on Robotics and Automation (ICRA)
titleIntegrated Planning and Execution Control of Autonomous Robot Actions
pages26892696 vol.3
Bandwidth,Capacity planning,Context,Delay,Humans,Intelligent robots,Mars,Mobile robots,Refining,Robot control

Berlin, Heidelberg

abstractThe synthesis problem asks to construct a reactive finite-state system from an $\omega$-regular specification. Initial specifications are often unrealizable, which means that there is no system that implements the specification. A common reason for unrealizability is that assumptions on the environment of the system are incomplete. We study the problem of correcting an unrealizable specification $\phi$ by computing an environment assumption $\psi$ such that the new specification $\psi\rightarrow\phi$ is realizable. Our aim is to construct an assumption $\psi$ that constrains only the environment and is as weak as possible. We present a two-step algorithm for computing assumptions. The algorithm operates on the game graph that is used to answer the realizability question. First, we compute a safety assumption that removes a minimal set of environment edges from the graph. Second, we compute a liveness assumption that puts fairness conditions on some of the remaining environment edges. We show that the problem of finding a minimal set of fair edges is computationally hard, and we use probabilistic games to compute a locally minimal fairness assumption.
booktitleCONCUR 2008 - Concurrency Theory
titleEnvironment Assumptions for Synthesis

abstractModel checking is a computer-assisted method for the analysis of dynamical systems that can be modeled by state-transition systems. Drawing from research traditions in mathematical logic, programming languages, hardware design, and theoretical computer science, model checking is now widely used for the verification of hardware and software in industry. This chapter is an introduction and short survey of model checking. The chapter aims to motivate and link the individual chapters of the handbook, and to provide context for readers who are not familiar with model checking.
booktitleHandbook of Model Checking
titleIntroduction to Model Checking

abstractOne major limitation to the applicability of Reinforcement Learning (RL) to many practical domains is the large number of samples required to learn an optimal policy. To address this problem and improve learning efficiency, we consider a linear hierarchy of abstraction layers of the Markov Decision Process (MDP) underlying the target domain. Each layer is an MDP representing a coarser model of the one immediately below in the hierarchy. In this work, we propose a novel form of Reward Shaping where the solution obtained at the abstract level is used to offer rewards to the more concrete MDP, in such a way that the abstract solution guides the learning in the more complex domain. In contrast with other works in Hierarchical RL, our technique has few requirements in the design of the abstract models and it is also tolerant to modeling errors, thus making the proposed approach practical. We formally analyze the relationship between the abstract models and the exploration heuristic induced in the lower-level domain. Moreover, we prove that the method guarantees optimal convergence and we demonstrate its effectiveness experimentally.
booktitleProceedings of the 37th AAAI Conference on Artificial Intelligence
titleExploiting Multiple Abstractions in Episodic RL via Reward Shaping
ML: Reinforcement Learning Algorithms

abstractTheorem proving and model checking are powerful tools that can verify the logical correctness of today's ICs or find their hidden bugs. Today, the first computer-aided verification tools are becoming commercially available. They are based on methods that in many cases can reduce the complexity of verification (without sacrificing guaranteed correctness) to such a degree that it becomes computationally feasible. Among the most powerful of these methods are symbolic model-checking and homomorphic reduction, both of which represent a complex system in terms of a compact and computationally more tractable structure. Moreover, the two can be used together with a multiplicative reduction effect, since they work independently of one another. Of special importance is the fact that they each can be implemented automatically, so the task of reduction is programmed into the computer rather than presenting a burden to the design engineer.
journaltitleIEEE Spectrum
titleComputer-Aided Verification
Circuit synthesis,Circuit testing,Computer bugs,Computer errors,Costs,Error correction,Hardware,Software systems,Software testing,System testing

journaltitleJournal of the ACM
shortjournalJ. ACM

booktitleProceedings of the 11th Workshop on Nonmonotonic Reasoning
titleA Semantics for ADL as Progression in the Situation Calculus

AAAI Press

abstractReiter proposed a semantics for knowledge-based Golog programs with sensing where program execution can be conditioned on tests involving explicit references to what the agent knows and does not know. An important result of this work is that reasoning about knowledge after the execution of actions can be reduced to classical reasoning from an initial first-order theory. However, it is limited in that tests can only refer to what is known about the current state, knowledge about knowledge is not considered, and the reduction does not apply to formulas with quantifying-in. This is in large part due to the choice of the underlying formalism, which is Reiter's version of the situation calculus. In this paper we show that, by moving to a new situation calculus recently proposed by Lakemeyer and Levesque, we cannot only reconstruct Reiter's foundations for knowledge-based programs but we can significantly go beyond them, which includes removing the above restrictions and more.
booktitleProceedings of the 10th Conference on Principles of Knowledge Representation and Reasoning (KR)
titleFoundations for Knowledge-Based Programs Using ES

AAAI Press

booktitleProceedings of the 11th International Conference on Principles of Knowledge Representation and Reasoning (KR)
titleA Logic for Non-Terminating Golog Programs
Reasoning about Action

journaltitleProceedings of the 20th International Joint Conference on Artificial Intelligence (IJCAI)
titleTowards an Integration of Golog and Planning

journaltitleKI - Künstliche Intelligenz
titlePLATAS – Integrating Planning and the Action Language Golog

AAAI Press

abstractThe 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.
booktitleProceedings of the 28th AAAI Conference on Artificial Intelligence (AAAI)
titleExploring the Boundaries of Decidable Verification of Non-Terminating Golog Programs

RWTH Aachen University

titlePlanning and Verification in the Agent Language Golog
Artificial Intelligence,Knowledge Representation

AAAI Press

booktitleProceedings of the 30th International Joint Conference on Artificial Intelligence (IJCAI)
titleA Uniform Abstraction Framework for Generalized Planning

IOS Press

abstractWe consider the realistic case of a GOLOG agent that only possesses incomplete knowledge about the state of its environment and has to resort to sensing in order to gather additional information at runtime, and where the agent is controlled by a knowledge-based program in which test conditions explicitly refer to the agents knowledge (or lack thereof). In this paper, we propose a formalization of knowledge-based agents that extends earlier proposals by a form of non-monotonic reasoning that includes Reiter-style defaults. We present a reasoning mechanism that enables us to reduce projection queries about future states of the agents knowledge (including nesting of epistemic modalities) to classical Default Logic, and provide a corresponding Representation Theorem. We thus obtain the theoretical foundation for an implementation where reasoning subtasks can be handed to an embedded off-the-shelf reasoner for Default Logic, and that supports a (in some respects) more expressive epistemic action language than previous solutions.
booktitleProceedings of the 22nd European Conference on Artificial Intelligence (ECAI)
titleKnowledge-Based Programs with Defaults in a Modal Situation Calculus

AAAI Press

booktitleProceedings of the 24th International Conference on Automated Planning and Scheduling (ICAPS)
titleMUM: A Technique for Maximising the Utility of Macro-operators by Constrained Generation and Use

abstractThis work presents Drake, a dynamic executive for temporal plans with choice. Dynamic plan execution strategies allow an autonomous agent to react quickly to unfolding events, improving the robustness of the agent. Prior work developed methods for dynamically dispatching Simple Temporal Networks, and further research enriched the expressiveness of the plans executives could handle, including discrete choices, which are the focus of this work. However, in some approaches to date, these additional choices induce significant storage or latency requirements to make flexible execution possible. Drake is designed to leverage the low latency made possible by a preprocessing step called compilation, while avoiding high memory costs through a compact representation. We leverage the concepts of labels and environments, taken from prior work in Assumption-based Truth Maintenance Systems (ATMS), to concisely record the implications of the discrete choices, exploiting the structure of the plan to avoid redundant reasoning or storage. Our labeling and maintenance scheme, called the Labeled Value Set Maintenance System, is distinguished by its focus on properties fundamental to temporal problems, and, more generally, weighted graph algorithms. In particular, the maintenance system focuses on maintaining a minimal representation of non-dominated constraints. We benchmark Drake's performance on random structured problems, and find that Drake reduces the size of the compiled representation by a factor of over 500 for large problems, while incurring only a modest increase in run-time latency, compared to prior work in compiled executives for temporal plans with discrete choices.
journaltitleJournal of Artificial Intelligence Research
titleDrake: An Efficient Executive for Temporal Plans with Choice

abstractWe consider a finite-state system with a finite number of clocks, where the transitions may depend on the values of the clocks, and may reset some of the clocks. We address the complexity and provide algorithms for the following problems. Suppose that the system starts from a given current state with a given assignment of values to the clocks. Can a given target state ever appear in the history of the system? What is the earliest time it can appear? What is the latest time it can appear?
journaltitleFormal Methods in System Design
shortjournalForm Method Syst Des
titleMinimum and Maximum Delay Problems in Real-Time Systems
finite-state system,reachability analysis,shortest path,timers,verification

booktitleRobotics: Science and Systems XII
titleIncremental Task and Motion Planning: A Constraint-Based Approach

labelalphaDe +09
booktitleMulti-Agent Programming
titleIndiGolog: A High-Level Programming Language for Embedded Reasoning Agents

labelalphaDe +22
abstractManufacturing is transitioning from a mass production model to a service model in which facilities `bid' to produce products. To decide whether to bid for a complex, previously unseen product, a facility must be able to synthesize, on the fly, a process plan controller that delegates abstract manufacturing tasks in a supplied process recipe to the available manufacturing resources. Often manufacturing processes depend on the data and objects (parts) they produce and consume. To formalize this aspect we need to adopt a first-order representation of the state of the processes. First-order representations of the state are commonly considered in reasoning about action in AI, and here we show that we can leverage the wide literature on the Situation Calculus and ConGolog programs to formalize this kind of manufacturing. With such a formalization available, we investigate how to synthesize process plan controllers in this first-order state setting. We also identify two important decidable cases—finite domains and bounded action theories—for which we provide techniques to actually synthesize the controller.
journaltitleArtificial Intelligence
shortjournalArtificial Intelligence
titleSituation Calculus for Controller Synthesis in Manufacturing Systems with First-Order State Representation
Automated synthesis,Reasoning about actions,Situation calculus,Smart manufacturing

Berlin, Heidelberg

abstractIn this paper, we investigate the links between planning and plans execution. We propose a new approach (Propice-Plan) which integrates both activities. It implements supervision and execution capabilities, combined with different planning techniques:
booktitleRecent Advances in AI Planning
titlePropice-Plan: Toward a Unified Framework for Planning and Execution
Anticipation Module,Blast Furnace,Goal Node,Plan Execution,Planning Module

Association for Computing Machinery, Inc

journaltitleCommunications of the ACM
titleThe Humble Programmer

abstractTALplanner is a forward-chaining planner that utilizes domain-dependent knowledge to control search in the state space generated by action invocation. The domain-dependent control knowledge, background knowledge, plans, and goals are all represented using formulas in a temporal logic called tal, which has been developed independently as a formalism for specifying agent narratives and reasoning about them. In the Fifth International Artificial Intelligence Planning and Scheduling Conference planning competition, TALplanner exhibited impressive performance, winning the Outstanding Performance Award in the Domain-Dependent Planning Competition. In this article, we provide an overview of TALplanner
journaltitleAI Magazine
titleTALplanner: A Temporal Logic-Based Planner

abstractResearch with autonomous unmanned aircraft systems is reaching a new degree of sophistication where targeted missions require complex types of deliberative capability integrated in a practical manner in such systems. Due to these pragmatic constraints, integration is just as important as theoretical and applied work in developing the actual deliberative functionalities. In this article, we present a temporal logic-based task planning and execution monitoring framework and its integration into a fully deployed rotor-based unmanned aircraft system developed in our laboratory. We use a very challenging emergency services application involving body identification and supply delivery as a vehicle for showing the potential use of such a framework in real-world applications. TALplanner, a temporal logic-based task planner, is used to generate mission plans. Building further on the use of TAL (Temporal Action Logic), we show how knowledge gathered from the appropriate sensors during plan execution can be used to create state structures, incrementally building a partial logical model representing the actual development of the system and its environment over time. We then show how formulas in the same logic can be used to specify the desired behavior of the system and its environment and how violations of such formulas can be detected in a timely manner in an execution monitor subsystem. The pervasive use of logic throughout the higher level deliberative layers of the system architecture provides a solid shared declarative semantics that facilitates the transfer of knowledge between different modules.
journaltitleAutonomous Agents and Multi-Agent Systems
shortjournalAuton Agent Multi-Agent Syst
titleA Temporal Logic-Based Planning and Execution Monitoring Framework for Unmanned Aircraft Systems
Execution monitoring,Intelligent autonomous systems,Planning,Reasoning about action and change,Temporal action logic,Unmanned aircraft systems

abstractThe quality and the correctness of software are often the greatest concern in electronic systems. Formal verification tools can provide a guarantee that a design is free of specific flaws. This paper surveys algorithms that perform automatic static analysis of software to detect programming errors or prove their absence. The three techniques considered are static analysis with abstract domains, model checking, and bounded model checking. A short tutorial on these techniques is provided, highlighting their differences when applied to practical problems. This paper also surveys tools implementing these techniques and describes their merits and shortcomings.
journaltitleIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems
titleA Survey of Automated Techniques for Formal Software Verification
Algorithm design and analysis,Automatic programming,Automatic testing,Bounded model checking (BMC),Formal verification,Hardware,model checking,Performance analysis,predicate abstraction,Software algorithms,Software performance,Software quality,Software systems,software verification,static analysis

journaltitleArtificial Intelligence
titleConGolog, a Concurrent Programming Language Based on the Situation Calculus
cognitive robotics,reasoning about actions,semantics of programs,situation calculus

abstractIn this paper, we investigate bounded action theories in the situation calculus. A bounded action theory is one which entails that, in every situation, the number of object tuples in the extension of fluents is bounded by a given constant, although such extensions are in general different across the infinitely many situations. We argue that such theories are common in applications, either because facts do not persist indefinitely or because the agent eventually forgets some facts, as new ones are learned. We discuss various classes of bounded action theories. Then we show that verification of a powerful first-order variant of the $\mu$-calculus is decidable for such theories. Notably, this variant supports a controlled form of quantification across situations. We also show that through verification, we can actually check whether an arbitrary action theory maintains boundedness.
journaltitleArtificial Intelligence
shortjournalArtificial Intelligence
titleBounded Situation Calculus Action Theories
Knowledge representation,Reasoning about action,Situation calculus,Verification

abstractIn model checking, the state-explosion problem occurs when one checks a nonflat system, i.e., a system implicitly described as a synchronized product of elementary subsystems. In this paper, we investigate the complexity of a wide variety of model-checking problems for nonflat systems under the light of parameterized complexity, taking the number of synchronized components as a parameter. We provide precise complexity measures (in the parameterized sense) for most of the problems we investigate, and evidence that the results are robust.
journaltitleJournal of Computer and System Sciences
shortjournalJournal of Computer and System Sciences
titleA Parametric Analysis of the State-Explosion Problem in Model Checking
Bisimilarity,Model checking,Parameterized complexity,State-explosion problem,Temporal logics

Berlin, Heidelberg

abstractWe study the problem of control synthesis for a timed plant and an external timed specification, modelled as timed automata. Our main result is that the problem is decidable when we are given a priori the resources for the controller (the number of clocks, observational power of clocks, etc.) and when the specification is an $\omega$-regular timed language describing undesired behaviours. We also show that for deterministic specifications, if there is a controller at all, then there is one which uses the combined resources of the plant and specification. The decidability of other related problems is also investigated.
booktitleProceedings of the 19th Annual Symposium on Theoretical Aspects of Computer Science (STACS)
titleTimed Control Synthesis for External Specifications

abstractThis paper extends network-based methods of constraint satisfaction to include continuous variables, thus providing a framework for processing temporal constraints. In this framework, called temporal constraint satisfaction problem (TCSP), variables represent time points and temporal information is represented by a set of unary and binary constraints, each specifying a set of permitted intervals. The unique feature of this framework lies in permitting the processing of metric information, namely, assessments of time differences between events. We present algorithms for performing the following reasoning tasks: finding all feasible times that a given event can occur, finding all possible relationships between two given events, and generating one or more scenarios consistent with the information provided. We distinguish between simple temporal problems (STPs) and general temporal problems, the former admitting at most one interval constraint on any pair of time points. We show that the STP, which subsumes the major part of Vilain and Kautz's point algebra, can be solved in polynomial time. For general TCSPs, we present a decomposition scheme that performs the three reasoning tasks considered, and introduce a variety of techniques for improving its efficiency. We also study the applicability of path consistency algorithms as preprocessing of temporal problems, demonstrate their termination and bound their complexities. © 1991.
journaltitleArtificial Intelligence
titleTemporal Constraint Networks

Berlin, Heidelberg

abstractSolving real-world problems using symbolic planning often requires a simplified formulation of the original problem, since certain subproblems cannot be represented at all or only in a way leading to inefficiency. For example, manipulation planning may appear as a subproblem in a robotic planning context or a packing problem can be part of a logistics task. In this paper we propose an extension of PDDL for specifying semantic attachments. This allows the evaluation of grounded predicates as well as the change of fluents by externally specified functions. Furthermore, we describe a general schema of integrating semantic attachments into a forward-chaining planner and report on our experience of adding this extension to the planners FF and Temporal Fast Downward. Finally, we present some preliminary experiments using semantic attachments.
booktitleTowards Service Robots for Everyday Environments: Recent Advances in Designing Service Robots for Complex Tasks in Everyday Environments
titleSemantic Attachments for Domain-Independent Planning Systems
Callback Function,External Module,Logistics Domain,Module Call,Packing Problem

abstractWe show that the pointwise version of the logic MTL is strictly less expressive than the continuous version, over finitewords. The proof is constructive in that we exhibit a timed language, which is definable in the continuous semantics but is not definable in the pointwise semantics.
journaltitleInternational Journal on Software Tools for Technology Transfer
shortjournalInt J Softw Tools Technol Transfer
titleOn the Expressiveness of MTL in the Pointwise and Continuous Semantics
Metric Temporal Logic,Real-time logics

Stockholm, Sweden

AAAI Press

abstractWe study planning for LTLf and LDLf temporally extended goals in nondeterministic fully observable domains (FOND). We consider both strong and strong cyclic plans, and develop foundational automata-based techniques to deal with both cases. Using these techniques we provide the computational characterization of both problems, separating the complexity in the size of the domain specification from that in the size of the formula. Specifically we establish them to be EXPTIME-complete and 2EXPTIME-complete, respectively, for both problems. In doing so, we also show 2EXPTIME- hardness for strong cyclic plans, which was open.
booktitleProceedings of the 27th International Joint Conference on Artificial Intelligence (IJCAI)
titleAutomata-Theoretic Foundations of FOND Planning for LTLf and LDLf Goals

booktitleProceedings of the 6th International Conference on Knowledge Representation and Reasoning (KR)
titleExecution Monitoring of High-Level Robot Programs

abstractBy their very design, many robot control programs are non-terminating. This paper describes a situation calculus approach to expressing and proving properties of non-terminating programs expressed in Golog, a high level logic programming language for modeling and implementing dynamical systems. Because in this approach actions and programs are represented in classical (second-order) logic, it is natural to express and prove properties of Golog programs, including non-terminating ones, in the very same logic. This approach to program proofs has the advantage of logical uniformity and the availability of classical proof theory.
booktitleProceedings of the AAAI'97 Workshop on Robots, Softbots, Immobots: Theories of Action, Planning and Control
relatedstringReprinted as
titleNon-Terminating Processes in the Situation Calculus
68T27,Formal verification of GOLOG and CONGOLOG programs,Inductive definitions,Knowledge representation,Reasoning about actions,Situation calculus

Berlin, Heidelberg

abstractWe study an automata-theoretic approach to planning for temporally extended goals. Specifically, we devise techniques based on nonemptiness of Büchi automata on infinite words, to synthesize sequential and conditional plans in a generalized setting in which we have that: goals are general temporal properties of desired execution; dynamic systems are represented by finite transition systems; incomplete information on the initial situation is allowed; and states are only partially observable. We prove that the techniques proposed are optimal wrt the worst case complexity of the problem. Thanks to the scalability of the nonemptiness algorithms, the techniques presented here promise to be applicable to fairly large systems, notwithstanding the intrinsic complexity of the problem.
booktitleRecent Advances in AI Planning
titleAutomata-Theoretic Approach to Planning for Temporally Extended Goals

abstractIn this paper we look into the assumption of interpreting LTL over finite traces. In particular we show that LTLf, i.e., LTL under this assumption, is less expressive than what might appear at first sight, and that at essentially no computational cost one can make a significant increase in expressiveness while maintaining the same intuitiveness of LTLf. Indeed, we propose a logic, LDLf for Linear Dynamic Logic over finite traces, which borrows the syntax from Propositional Dynamic Logic (PDL), but is interpreted over finite traces. Satisfiability, validity and logical implication (as well as model checking) for LTLf. are PSPACE-complete as for LTLf. (and LTL).
booktitleProceedings of the 23rd International Joint Conference on Artificial Intelligence (IJCAI)
titleLinear Temporal Logic and Linear Dynamic Logic on Finite Traces

AAAI Press

booktitleProceedings of the 24th International Joint Conference on Artificial Intelligence (IJCAI)
titleSynthesis for LTL and LDL on Finite Traces

booktitleProceedings of the 25th International Joint Conference on Artificial Intelligence (IJCAI)
titleLTLf and LDLf Synthesis under Partial Observability

abstractAnswer set programming (ASP) is a knowledge representation and reasoning paradigm with high-level expressive logic-based formalism, and efficient solvers; it is applied to solve hard problems in various domains, such as systems biology, wire routing, and space shuttle control. In this paper, we present an application of ASP to housekeeping robotics. We show how the following problems are addressed using computational methods/tools of ASP: (1) embedding commonsense knowledge automatically extracted from the commonsense knowledge base ConceptNet, into high-level representation, and (2) embedding (continuous) geometric reasoning and temporal reasoning about durations of actions, into (discrete) high-level reasoning. We introduce a planning and monitoring algorithm for safe execution of plans, so that robots can recover from plan failures due to collision with movable objects whose presence and location are not known in advance or due to heavy objects that cannot be lifted alone. Some of the recoveries require collaboration of robots. We illustrate the applicability of ASP on several housekeeping robotics problems, and report on the computational efficiency in terms of CPU time and memory.
journaltitleIntelligent Service Robotics
shortjournalIntel Serv Robotics
shorttitleAnswer Set Programming for Collaborative Housekeeping Robotics
titleAnswer Set Programming for Collaborative Housekeeping Robotics: Representation, Reasoning, and Execution

abstractWe consider the computation tree logic (CTL) proposed in (Sci. Comput. Programming 2 (1982), 241–260) which extends the unified branching time logic (UB) of (“Proc. Ann. ACM Sympos. Principles of Programming Languages, 1981,” pp. 164–176) by adding an until operator. It is established that CTL has the small model property by showing that any satisfiable CTL formulae is satisfiable in a small finite model obtained from the small “pseudomodel” resulting from the Fischer-Ladner quotient construction. Then an exponential time algorithm is given for deciding satisfiability in CTL, and the axiomatization of UB given in ibid. is extended to a complete axiomatization for CTL. Finally, the relative expressive power of a family of temporal logics obtained by extending or restricting the syntax of UB and CTL is studied.
journaltitleJournal of Computer and System Sciences
shortjournalJournal of Computer and System Sciences
titleDecision Procedures and Expressiveness in the Temporal Logic of Branching Time

abstractThe differences between and appropriateness of branching versus linear time temporal logic for reasoning about concurrent programs are studied. These issues have been previously considered by Lamport. To facilitate a careful examination of these issues, a language, CTL*, in which a universal or existential path quantifier can prefix an arbitrary linear time assertion, is defined. The expressive power of a number of sublanguages is then compared. CTL* is also related to the logics MPL of Abrahamson and PL of Harel, Kozen, and Parikh. The paper concludes with a comparison of the utility of branching and linear time temporal logics.
journaltitleJournal of the ACM
title“Sometimes” and “Not Never” Revisited: On Branching versus Linear Time Temporal Logic

Berlin, Heidelberg

abstractWe present Unbeast v.0.6, a tool for synthesising finite-state systems from specifications written in linear-time temporal logic (LTL). We combine bounded synthesis, specification splitting and symbolic game solving with binary decision diagrams (BDDs), which allows tackling specifications that previous tools were typically unable to handle. In case of realizability of a given specification, our tool computes a prototype implementation in a fully symbolic way, which is especially beneficial for settings with many input and output bits.
booktitleTools and Algorithms for the Construction and Analysis of Systems (TACAS)
titleUnbeast: Symbolic Bounded Synthesis

abstractThis chapter discusses temporal and modal logic. The chapter describes a multiaxis classification of systems of temporal logic. The chapter describes the framework of linear temporal logic. In both its propositional and first-order forms, linear temporal logic has been widely employed in the specification and verification of programs. The chapter describes the competing framework of branching temporal logic, which has seen wide use. It also explains how temporal logic structures can be used to model concurrent programs using non-determinism and fairness. The chapter also discusses other modal and temporal logics in computer science. The chapter describes the formal syntax and semantics of Propositional Linear Temporal Logic (PLTL). The chapter also describes the formal syntax and semantics for two representative systems of propositional branching-time temporal logics.
booktitleFormal Models and Semantics
titleTemporal and Modal Logic

abstractPlanning systems for real-world applications need the ability to handle concurrency and numeric fluents. Nevertheless, the predominant approach to cope with concurrency followed by the most successful participants in the latest International Planning Competitions (IPC) is still to find a sequential plan that is rescheduled in a post-processing step. We present Temporal Fast Downward (TFD), a planning system for temporal problems that is capable of finding low-makespan plans by performing a heuristic search in a temporal search space. We show how the context-enhanced additive heuristic can be successfully used for temporal planning and how it can be extended to numeric fluents. TFD often produces plans of high quality and, evaluated according to the rating scheme of the last IPC, outperforms all state-of-the-art temporal planning systems.
booktitleNineteenth International Conference on Automated Planning and Scheduling (ICAPS)
titleUsing the Context-Enhanced Additive Heuristic for Temporal and Numeric Planning

IOS Press

abstractWe provide a systematic analysis of levels of integration between discrete high-level reasoning and continuous low-level feasibility checks to address hybrid planning problems in robotic applications. We identify four distinct strategies for such an
journaltitleAI Communications
titleA Systematic Analysis of Levels of Integration between High-Level Task Planning and Low-Level Feasibility Checks

abstractWe present a formal framework that combines high-level representation and causality-based reasoning with low-level geometric reasoning and motion planning. The frame-work features bilateral interaction between task and motion planning, and embeds geometric reasoning in causal reasoning, thanks to several advantages inherited from its underlying components. In particular, our choice of using a causality-based high-level formalism for describing action domains allows us to represent ramifications and state/transition constraints, and embed in such formal domain descriptions externally defined functions implemented in some programming language (e.g., C++). Moreover, given such a domain description, the causal reasoner based on this formalism (i.e., the Causal Calculator) allows us to compute optimal solutions (e.g., shortest plans) for elaborate planning/prediction problems with temporal constraints. Utilizing these features of high-level representation and reasoning, we can combine causal reasoning, motion planning and geometric planning to find feasible kinematic solutions to task-level problems. In our framework, the causal reasoner guides the motion planner by finding an optimal task-plan; if there is no feasible kinematic solution for that task-plan then the motion planner guides the causal reasoner by modifying the planning problem with new temporal constraints. Furthermore, while computing a task-plan, the causal reasoner takes into account geometric models and kinematic relations by means of external predicates implemented for geometric reasoning (e.g., to check some collisions); in that sense the geometric reasoner guides the causal reasoner to find feasible kinematic solutions. We illustrate an application of this framework to robotic manipulation, with two pantograph robots on a complex assembly task that requires concurrent execution of actions. A short video of this application accompanies the paper.
booktitle2011 IEEE International Conference on Robotics and Automation (ICRA)
titleCombining High-Level Causal Reasoning with Low-Level Geometric Reasoning and Motion Planning for Robotic Manipulation
action domain,bilateral interaction,C++ language,C++ programming language,causal calculator,causality-based high-level formalism,cause-effect analysis,Cognition,Collision avoidance,control engineering computing,geometric planning,high-level causal reasoning,kinematic relations,Kinematics,low-level geometric reasoning,manipulator kinematics,motion planning,optimal task-plan,path planning,Payloads,Planning,planning problem,robotic manipulation,Robots,spatial reasoning,state-transition constraint,task-level problem,Trajectory

abstractThis paper reports on the design and implementation of a real-time executive for a mobile rover that uses a model-based, declarative approach. The control system is based on the intelligent distributed execution architecture (IDEA), an approach to planning and execution that provides a unified representational and computational framework for an autonomous agent. The basic hypothesis of IDEA is that a large control system can be structured as a collection of interacting agents, each with the same fundamental structure. We show that planning and real-time response are compatible if the executive minimizes the size of the planning problem. We detail the implementation of this approach on an 'exploration rover (Gromit, an RWI ATRV Junior at NASA Ames) presenting different IDEA controllers of the same domain and comparing them with more classical approaches. We demonstrate that the approach is scalable to complex coordination of functional modules needed for autonomous navigation and exploration.
booktitle2004 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS)
titleModel-Based Executive Control through Reactive Planning for Autonomous Rovers
Buildings,Encoding,Engines,Mobile robots,Monitoring,NASA,Remuneration,Resource management,Robustness,Testing

abstractWe present a structure for transition systems with which the main decidability results on Petri nets can be generalized to structured transition systems. We define the reduced reachability tree of a structured transition system; it allows one to decide the finite reachability tree problem (also called the finite termination problem) and the finite reachability set problem. A general definition of the coverability set is given and the procedure of Karp and Miller is extended for well-structured transition systems. We show then that the coverability problem is a decidable problem in the framework of well-structured transition systems. Finally, we introduce structured set of terminal states and we show that the finite reachability tree problem and the finite reachability set problem are decidable. Coverability is an open problem for structured transition systems with a structured set of terminal states.
journaltitleInformation and Computation
shortjournalInformation and Computation
titleReduction and Covering of Infinite Reachability Trees

abstractIn recent years research in the planning community has moved increasingly toward s application of planners to realistic problems involving both time and many typ es of resources. For example, interest in planning demonstrated by the space res earch community has inspired work in observation scheduling, planetary rover ex ploration and spacecraft control domains. Other temporal and resource-intensive domains including logistics planning, plant control and manufacturing have also helped to focus the community on the modelling and reasoning issues that must be confronted to make planning technology meet the challenges of application. The International Planning Competitions have acted as an important motivating fo rce behind the progress that has been made in planning since 1998. The third com petition (held in 2002) set the planning community the challenge of handling tim e and numeric resources. This necessitated the development of a modelling langua ge capable of expressing temporal and numeric properties of planning domains. In this paper we describe the language, PDDL2.1, that was used in the competition. We describe the syntax of the language, its formal semantics and the validation of concurrent plans. We observe that PDDL2.1 has considerable modelling power — exceeding the capabilities of current planning technology — and presents a number of important challenges to the research community.
journaltitleJournal of Artificial Intelligence Research
titlePDDL2.1: An Extension to PDDL for Expressing Temporal Planning Domains

abstractIn this paper, we present the robot programming and planning language Readylog, a Golog dialect, which was developed to support the decision making of robots acting in dynamic real-time domains, such as robotic soccer. The formal framework of Readylog, which is based on the situation calculus, features imperative control structures such as loops and procedures, allows for decision-theoretic planning, and accounts for a continuously changing world. We developed high-level controllers in Readylog for our soccer robots in RoboCup's Middle-size league, but also for service robots and for autonomous agents in interactive computer games. For a successful deployment of Readylog on a real robot it is also important to account for the control problem as a whole, integrating the low-level control of the robot (such as localization, navigation, and object recognition) with the logic-based high-level control. In doing so, our approach can be seen as a step towards bridging the gap between the fields of robotics and knowledge representation.
journaltitleRobotics and Autonomous Systems
shortjournalRobotics and Autonomous Systems
titleLogic-Based Robot Control in Highly Dynamic Domains
cognitive robotics,Cognitive robotics,planning,Planning,reasoning about actions,Reasoning about actions,robocup,RoboCup

booktitleProceedings of the International Joint Conference on Artificial Intelligence (IJCAI)
titleRepresenting Flexible Temporal Behaviors in the Situation Calculus
abstract,golog,situation calculus,temporal

Berlin, Heidelberg

abstractWe present an effective controller synthesis method for real-time systems modeled as timed automata with safety requirements. Under the realistic assumption of partial observability, the problem is undecidable in general, and prohibitively expensive (2ExpTime-complete) if a bound on the granularity of the controller is set in advance. We investigate the synthesis of controllers from templates, given as timed automata with parametric control structure. Template-based synthesis is significantly cheaper (PSpace-complete) than standard synthesis and produces much simpler controllers. We present an efficient symbolic synthesis algorithm based on automatic abstraction refinement and report on encouraging experimental results from an implementation in the timed verification and synthesis tool synthia.
booktitleTools and Algorithms for the Construction and Analysis of Systems (TACAS)
titleTemplate-Based Controller Synthesis for Timed Systems
Controller Synthesis,Model Check,Partial Observability,Synthesis Algorithm,Time Automaton

abstractWell-structured transition systems (WSTSs) are a general class of infinite-state systems for which decidability results rely on the existence of a well-quasi-ordering between states that is compatible with the transitions. In this article, we provide an extensive treatment of the WSTS idea and show several new results. Our improved definitions allow many examples of classical systems to be seen as instances of WSTSs.
journaltitleTheoretical Computer Science
shortjournalTheoretical Computer Science
titleWell-Structured Transition Systems Everywhere!
Infinite systems,Verification,Well-quasi-ordering

booktitleAIPS Workshop on Online Planning and Scheduling
titleProgramming Hierarchical Task Networks in the Situation Calculus

Metaphysics Research Lab, Stanford University

booktitleThe Stanford Encyclopedia of Philosophy
editionSummer 2021
titleModal Logic

Cambridge, MA, USA

MIT Press

booktitleArtificial Intelligence and Mobile Robots: Case Studies of Successful Robot Systems
titleOn Three-Layer Architectures

titleA Concise Introduction to Models and Methods for Automated Planning

Berlin, Heidelberg

abstractWe propose an original approach to integrate symbolic task planning, and geometric motion and manipulation planning. We focus more particularly on one key aspect: the relation between the symbolic positions and their geometric counterparts. Indeed, we have developed an instantiation process that is able to propagate incrementally task-dependent as well as 3D environment-dependent constraints and to guide efficiently the search until valid geometric configurations are found that satisfy the plan at both levels. The overall process is discussed and illustrated through an implemented example.
booktitleProceedings of the 11th International Symposium on Robotics Research
titleaSyMov: A Planner That Deals with Intricate Symbolic and Geometric Problems
Collision Check,Geometric Problem,Geometric State,Motion Planning,Movable Object

abstractPreviously, the plan language cc-Golog was intro- duced for the purpose of specifying event-driven behavior typically found in robot controllers. So far, however, cc-Golog is usable only for project- ing the outcome of a plan and it is unclear how to actually execute plans on-line on a robot. In this paper, we provide such an execution model for cc- Golog and, in addition, showhowto interleave exe- cutionwith a new kind of time-bounded projection. Along the way we also demonstrate how a typical robot control architecture where a high-level con- troller communicates with low-level processes via messages can be directly modelled in cc-Golog.
booktitleProceedings of the 17th International Joint Conference on Artificial Intelligence (IJCAI)
titleOn-Line Execution of Cc-Golog Plans

abstractHigh-level robot controllers often need to specify event-driven behavior and they operate low-level processes which change the world in a continuous fashion. While non logic-based control languages have existed for some time to address these issues, this is not the case for logic-based languages. To remedy the situation, we show how to incorporate continuous change and event-driven behavior into the action language GOLOG. Besides proposing a suitable semantics for the new language, which we call cc-Golog, we show how a robot architecture where a high-level controller communicates via messages with low-level routines can be modeled naturally in this new dialect. Finally, we demonstrate how on-line execution and off-line projection can be combined in this language.
journaltitleLogic Journal of the IGPL
titleCc-Golog - an Action Language with Continuous Change
golog,reading list

journaltitleThe Language of the Fifth International Planning Competition
titlePlan Constraints and Preferences in PDDL3
typeTechnical Report

Chicago, IL

AAAI Press

abstractThis paper presents a temporal planner, called IxTeT. It focuses on the representation and control issues, arguing for a compromise between the expressiveness and the efficiency of the search. The representation relies on a point-based reified logic, associated to multi-valued domain attributes. Hierarchical planning operators offer an expressive description, with parallelism, durations, effects and conditions at various moments of the action. Time in the input scenario enables to take into account predicted forthcoming events and to plan in a dynamic world. A compilation procedure checks the consistency of the operators specified by the user. The control relies on the use of causal-links, A$\epsilon$, algorithm, and an extended least-commitment strategy. It uses two important procedures, called "feasibility" and "satisfiability", dealing respectively with goal decomposition and conflict resolution:
booktitleProceedings of the 2nd International Conference on Artificial Intelligence Planning Systems
titleRepresentation and Control in IxTeT, a Temporal Planner

abstractManipulation problems involving many objects present substantial challenges for motion planning algorithms due to the high dimensionality and multi-modality of the search space. Symbolic task planners can efficiently construct plans involving many entities but cannot incorporate the constraints from geometry and kinematics. In this paper, we show how to extend the heuristic ideas from one of the most successful symbolic planners in recent years, the FastForward (FF) planner, to motion planning, and to compute it efficiently. We use a multi-query roadmap structure that can be conditionalized to model different placements of movable objects. The resulting tightly integrated planner is simple and performs efficiently in a collection of tasks involving manipulation of many objects.
booktitleAlgorithmic Foundations of Robotics XI: Selected Contributions of the 11th International Workshop on the Algorithmic Foundations of Robotics
titleFFRob: An Efficient Heuristic for Task and Motion Planning
Goal Literals,Movable Objects,Relaxed Plan Graph,Robot Configuration,Symbolic Devices

Springer Netherlands

abstractThe situation calculus [8] is a methodology for expressing facts about action and change in formal languages of mathematical logic. It involves expressions for situations and actions (events), and the function Result that relates them to each other. The possibilities and limitations of this methodology have never been systematically investigated, and some of the commonly accepted views on this subject seem to be inaccurate.
booktitleAutomated Reasoning: Essays in Honor of Woody Bledsoe
titleWhat Are the Limitations of the Situation Calculus?
Concurrent Action,Dine Room,Frame Problem,Nonmonotonic Reasoning,Temporal Reasoning

Morgan Kaufmann Publishers

titleAutomated Planning - Theory and Practice

abstractPlanning is motivated by acting. Most of the existing work on automated planning underestimates the reasoning and deliberation needed for acting; it is instead biased towards path-finding methods in a compactly specified state-transition system. Researchers in this AI field have developed many planners, but very few actors. We believe this is one of the main causes of the relatively low deployment of automated planning applications. In this paper, we advocate a change in focus to actors as the primary topic of investigation. Actors are not mere plan executors: they may use planning and other deliberation tools, before and during acting. This change in focus entails two interconnected principles: a hierarchical structure to integrate the actor's deliberation functions, and continual online planning and reasoning throughout the acting process. In the paper, we discuss open problems and research directions toward that objective in knowledge representations, model acquisition and verification, synthesis and refinement, monitoring, goal reasoning, and integration.
journaltitleArtificial Intelligence
shortjournalArtificial Intelligence
shorttitleThe Actor's View of Automated Planning and Acting
titleThe Actor's View of Automated Planning and Acting: A Position Paper
Automated planning and acting

Cambridge University Press

titleAutomated Planning and Acting

Morgan Kaufmann

abstractThis paper shows how an extension of the resolution proof procedure can be used to construct problem solutions. The extended proof procedure can solve problems involving state transformations. The paper explores several alternate problem representations and provides a discussion of solutions to sample problems including the “Monkey and Bananas” puzzle and the “Tower of Hanoi” puzzle. The paper exhibits solutions to these problems obtained by QA3, a computer program based on these theorem-proving methods. In addition, the paper shows how QA3 can write simple computer programs and can solve practical problems for a simple robot.
booktitleProceedings of the 1st International Joint Conference on Artificial Intelligence (IJCAI)
titleApplication of Theorem Proving to Problem Solving

abstractInformally, abstraction can be described as the process of mapping a representation of a problem onto a new representation. The aim of this paper is to propose the beginnings of a theory of reasoning with abstraction which captures and generalizes most previous work in the area. The theory allows us to study the properties of abstraction mappings and provides the foundations for the mechanization of abstraction inside an abstract proof checker.
journaltitleArtificial Intelligence
shortjournalArtificial Intelligence
titleA Theory of Abstraction

Morgan Kaufmann

abstractSeveral researchers have used non-monotonic logic in attempts to abolish frame axioms that are specific to one domain in favor of a universal frame axiom. We argue that the universal frame axiom cannot work in a domain that allows incomplete descriptions of situations. Therefore domain-specific frame axioms are needed. We illustrate an approach to writing these axioms by considering frame axioms about motion, including the formalization of simple example.
booktitleThe Frame Problem in Artificial Intelligence
titleThe Case for Domain-Specific Frame Axioms

abstractA robot's actions are inherently stochastic, as its sensors are noisy and its actions do not always have the intended effects. For this reason, the agent language Golog has been extended to models with degrees of belief and stochastic actions. While this allows more precise robot models, the resulting programs are much harder to comprehend, because they need to deal with the noise, e.g., by looping until some desired state has been reached with certainty, and because the resulting action traces consist of a large number of actions cluttered with sensor noise. To alleviate these issues, we propose to use abstraction. We define a high-level and nonstochastic model of the robot and then map the high-level model into the lower-level stochastic model. The resulting programs are much easier to understand, often do not require belief operators or loops, and produce much shorter action traces.
booktitleKR Workshop on Explainable Logic-Based Knowledge Representation (XLoKR)
titleUsing Abstraction for Interpretable Robot Programs in Stochastic Domains

abstractAbstraction is a commonly used process to represent some low-level system by a more coarse specification with the goal to omit unnecessary details while preserving important aspects. While recent work on abstraction in the situation calculus has focused on non-probabilistic domains, we describe an approach to abstraction of probabilistic and dynamic systems. Based on a variant of the situation calculus with probabilistic belief, we define a notion of bisimulation that allows to abstract a detailed probabilistic basic action theory with noisy actuators and sensors by a possibly non-stochastic basic action theory. By doing so, we obtain abstract Golog programs that omit unnecessary details and which can be translated back to a detailed program for actual execution. This simplifies the implementation of noisy robot programs, opens up the possibility of using non-stochastic reasoning methods (e.g., planning) on probabilistic problems, and provides domain descriptions that are more easily understandable and explainable.
booktitleProceedings of the 22nd International Conference on Autonomous Agents and Multiagent Systems (AAMAS)
titleAbstracting Noisy Robot Programs
Computer Science - Artificial Intelligence

booktitleAnnual Conference on Artificial Intelligence
titleGOLEX - Bridging the Gap between Logic (GOLOG) and a Real Robot

journaltitleJournal of Artificial Intelligence Research
titleThe Fast Downward Planning System

Berlin, Heidelberg

abstractWe describe a prototype extension of the real-time model checking tool Uppaal  with symmetry reduction. The symmetric data type scalarset, which is also used in the Mur$\phi~$model checker, was added to Uppaal's system description language to support the easy static detection of symmetries. Our prototype tool uses state swaps, described and proven sound earlier by Hendriks, to reduce the space and memory consumption of Uppaal. Moreover, the reduction strategy is canonical, which means that the symmetries are optimally used. For all examples that we experimented with (both academic toy examples and industrial cases), we obtained a drastic reduction of both computation time and memory usage, exponential in the size of the scalar sets used.
booktitleFormal Modeling and Analysis of Timed Systems
titleAdding Symmetry Reduction to Uppaal
Canonical Representative,Model Check,Model Check Algorithm,Reachability Analysis,Symmetry Reduction

abstractHybrid automata model systems with both digital and analog components, such as embedded control programs. Many verification tasks for such programs can be expressed as reachability problems for hybrid automata. By improving on previous decidability and undecidability results, we identify a boundary between decidability and undecidability for the reachability problem of hybrid automata. On the positive side, we give an (optimal) PSPACE reachability algorithm for the case of initialized rectangular automata, where all analog variables follow independent trajectories within piecewise-linear envelopes and are reinitialized whenever the envelope changes. Our algorithm is based on the construction of a timed automaton that contains all reachability information about a given initialized rectangular automaton. The translation has practical significance for verification, because it guarantees the termination of symbolic procedures for the reachability analysis of initialized rectangular automata. The translation also preserves the$\omega$-languages of initialized rectangular automata with bounded nondeterminism. On the negative side, we show that several slight generalizations of initialized rectangular automata lead to an undecidable reachability problem. In particular, we prove that the reachability problem is undecidable for timed automata augmented with a single stopwatch.
journaltitleJournal of Computer and System Sciences
shortjournalJournal of Computer and System Sciences
titleWhat's Decidable about Hybrid Automata?

Berlin, Heidelberg

abstractWe summarize and reorganize some of the last decade's research on real-time extensions of temporal logic. Our main focus is on tableau constructions for model checking linear temporal formulas with timing constraints. In particular, we find that a great deal of real-time verification can be performed in polynomial space, but also that considerable care must be exercised in order to keep the real-time verification problem in polynomial space, or even decidable.
booktitleCONCUR'98 Concurrency Theory
shorttitleIt's about Time
titleIt's about Time: Real-time Logics Reviewed
Interval Trace,Model Check,Polynomial Space,Satisfiability Problem,Temporal Logic

IOS Press

abstractIn recent years, domain-independent planning has been applied to a rising number of real-world applications. Usually, the description language of choice is PDDL. However, PDDL is not suited to model all challenges imposed by real-world applications. Dornhege et al. proposed semantic attachments to allow the computation of Boolean fluents by external processes called modules during planning. To acquire state information from the planning system a module developer must perform manual requests through a callback interface which is both inefficient and error-prone. In this paper, we present the Object-oriented Planning Language OPL, which incorporates the structure and advantages of modern object-oriented programming languages. We demonstrate how a domain-specific module interface that allows to directly access the planner state using object member functions is automatically generated from an OPL planning task. The generated domain-specific interface allows for a safe and less error-prone implementation of modules. We show experimentally that this interface is more efficient than the PDDL-based module interface of TFD/M.
booktitleProceedings of the 20th European Conference on Artificial Intelligence
shorttitlePlanning with Semantic Attachments
titlePlanning with Semantic Attachments: An Object-Oriented View

booktitleProceedings of the 30th International Joint Conference on Artificial Intelligence (IJCAI)
titleUsing Platform Models for a Guided Explanatory Diagnosis Generation for Mobile Robots

Cornell University Press

titleKnowledge and Belief

abstractWe present a logic for stating properties such as, “after a request for service there is at least a 98% probability that the service will be carried out within 2 seconds”. The logic extends the temporal logic CTL by Emerson, Clarke and Sistla with time and probabilities. Formulas are interpreted over discrete time Markov chains. We give algorithms for checking that a given Markov chain satisfies a formula in the logic. The algorithms require a polynomial number of arithmetic operations, in size of both the formula and the Markov chain. A simple example is included to illustrate the algorithms.
journaltitleFormal Aspects of Computing
shortjournalFormal Aspects of Computing
titleA Logic for Reasoning about Time and Reliability
Automatic verification,CTL,Markov chains,Modal logic,Model checking,Probability,Real time,Soft deadlines

booktitleProceedings of the 11th Cognitive Robotics Workshop 2018 (CogRob)
titleA Logic for Specifying Metric Temporal Constraints for Golog Programs

abstractExecuting a Golog program on an actual robot typically requires additional steps to account for hardware or software details of the robot platform, which can be formulated as constraints on the program. Such constraints are often temporal, refer to metric time, and require modifications to the abstract Golog program. We describe how to formulate such constraints based on a modal variant of the Situation Calculus. These constraints connect the abstract program with the platform models, which we describe using timed automata. We show that for programs over finite domains and with fully known initial state, the problem of synthesizing a controller that satisfies the constraints while preserving the effects of the original program can be reduced to MTL synthesis. We do this by constructing a timed automaton from the abstract program and synthesizing an MTL controller from this automaton, the platform models, and the constraints. We prove that the synthesized controller results in execution traces which are the same as those of the original program, possibly interleaved with platform-dependent actions, that they satisfy all constraints, and that they have the same effects as the traces of the original program. By doing so, we obtain a decidable procedure to synthesize a controller that satisfies the specification while preserving the original program.
titleController Synthesis for Golog Programs over Finite Domains with Metric Temporal Constraints
venue17th International Conference on Principles of Knowledge Representation and Reasoning
Computer Science - Artificial Intelligence,Computer Science - Logic in Computer Science

abstractNonmonotonic formal systems have been proposed as an extension to classical first-order logic that will capture the process of human “default reasoning” or “plausible inference” through their inference mechanisms, just as modus ponens provides a model for deductive reasoning. But although the technical properties of these logics have been studied in detail and many examples of human default reasoning have been identified, for the most part these logics have not actually been applied to practical problems to see whether they produce the expected results. We provide axioms for a simple problem in temporal reasoning which has long been identified as a case of default reasoning, thus presumably amenable to representation in nonmonotonic logic. Upon examining the resulting nonmonotonic theories, however, we find that the inferences permitted by the logics are not those we had intended when we wrote the axioms, and in fact are much weaker. This problem is shown to be independent of the logic used; nor does it depend on any particular temporal representation. Upon analyzing the failure we find that the nonmonotonic logics we considered are inherently incapable of representing this kind of default reasoning. The first part of the paper is an expanded version of one that appeared in the 1986 AAAI proceedings. The second part reports on several responses to our result that have appeared since the original paper was published.
journaltitleArtificial Intelligence
shortjournalArtificial Intelligence
titleNonmonotonic Logic and Temporal Projection

Berlin, Heidelberg

abstractReal-time systems operate in “real,” continuous time and state changes may occur at any real-numbered time point. Yet many verification methods are based on the assumption that states are observed at integer time points only. What can we conclude if a real-time system has been shown “correct” for integral observations?
booktitleAutomata, Languages and Programming
titleWhat Good Are Digital Clocks?
Annual Symposium,Atomic Proposition,Linear Temporal Logic,Temporal Logic,Verification Method

abstractWe describe and evaluate the algorithmic techniques that are used in the FF planning system. Like the HSP system, FF relies on forward state space search, using a heuristic that estimates goal distances by ignoring delete lists. Unlike HSP's heuristic, our method does not assume facts to be independent. We introduce a novel search strategy that combines hill-climbing with systematic search, and we show how other powerful heuristic information can be extracted and used to prune the search space. FF was the most successful automatic planner at the recent AIPS-2000 planning competition. We review the results of the competition, give data for other benchmark domains, and investigate the reasons for the runtime performance of FF compared to HSP.
journaltitleJournal of Artificial Intelligence Research
titleThe FF Planning System: Fast Plan Generation through Heuristic Search

AAAI Press

abstractPlanning in an on-line robotics context has the specific requirement of a short planning duration. A property of typical contemporary scenarios is that (mobile) robots perform similar or even repeating tasks during operation. With these robot domains in mind, we propose database-driven macroplanning for STRIPS (DBMP/S) that learns macros – action sequences that frequently appear in plans – from experience for PDDL-based planners. Planning duration is improved over time by off-line processing of seed plans using a scalable database. The approach is indifferent about the specific planner by representing the resulting macros again as actions with preconditions and effects determined based on the actions contained in the macro. For some domains we have used separate planners for learning and execution exploiting their respective strengths. Initial results based on some IPC domains and a logistic robot scenario show significantly improved (over non-macro planners) or slightly better and comparable (to existing macro planners) performance.
booktitleProceedings of the 27th International Conference on Automated Planning and Scheduling (ICAPS)
shorttitleGenerating Macro Actions from a Plan Database
titleInitial Results on Generating Macro Actions from a Plan Database for Planning on Autonomous Mobile Robots
Robotics Special Track

abstractA macro operator is a planning operator that is generated from a sequence of actions. Macros have mostly been used for macro planning, where the planner considers the macro as a single action and expands it into the original sequence during execution, but they can also be applied to other problems, such as maintaining a plan library. There are several approaches to macro operator generation, which differ in restrictions on the original actions and in the way they represent macros. However, all existing approaches are either restricted to STRIPS domains, only work on grounded actions, or they do not synthesize macros but consider the original sequence instead. We study the synthesis of macro operators for ADL domains. We describe how to compute the parameterized preconditions and effects of a macro operator such that they are equivalent to the preconditions and effects of the respective action sequence and prove the correctness of the synthesized macro operators based on a Situation Calculus semantics for ADL. We use the synthesis method for ADL macro planning and evaluate it on a number of domains from the IPC. As a second application, we describe how macro operator synthesis can be useful for maintaining a plan library by computing the precondition and effects of the parameterized library plans.
booktitleProceedings of the 24th European Conference on Artificial Intelligence (ECAI)
titleMacro Operator Synthesis for ADL Domains

abstractIn this paper an attempt is made to explore the logical foundations of computer programming by use of techniques which were first applied in the study of geometry and have later been extended to other branches of mathematics. This involves the elucidation of sets of axioms and rules of inference which can be used in proofs of the properties of computer programs. Examples are given of such axioms and rules, and a formal proof of a simple theorem is displayed. Finally, it is argued that important advantage, both theoretical and practical, may follow from a pursuance of these topics.
journaltitleCommunications of the ACM
shortjournalCommun. ACM
titleAn Axiomatic Basis for Computer Programming
axiomatic method,formal language definition,machine-independent programming,program documentation,programming language design,theory of programming' proofs of programs

abstractTo 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 exe- cution 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.
booktitleProceedings of the 30th Conference on Artificial Intelligence (AAAI)
titleContinual Planning in Golog

abstractIn 2017, the RoboCup Logistics League (RCLL) has seen major changes to the playing field layout, which allows for more configuration variants that are now generated randomly and automatically, leading towards a more realistic smart factory scenario. The Carologistics team developed a new strategy for exploration and improved existing components with a particular focus on navigation and error handling in the behavior engine and high-level reasoning. We describe the major concepts of our approach with a focus on the improvements in comparison to last year, which enabled us to win the competition in 2017.
booktitleRoboCup 2017: Robot World Cup XXI
titleEnhancing Software and Hardware Reliability for a Successful Participation in the RoboCup Logistics League 2017

booktitleAAAI Spring Symposium: Integrating Representation, Reasoning, Learning, and Execution for Goal Directed Autonomy
titleConstraint-Based Online Transformation of Abstract Plans into Executable Robot Actions

abstractThe RoboCup Logistics League is a robotics competition in a Smart Factory scenario in which a team of robots has to assemble products for dynamically generated orders. In 2019, the Carologistics was able to win the competition with a redesigned manipulation system, improved navigation, and an incremental and distributed goal reasoning system. In this paper, we describe the major components of our approach that enabled us to win the competition, with a particular focus on this year's changes.
booktitleRoboCup 2019: Robot World Cup XXIII
titleWinning the RoboCup Logistics League with Fast Navigation, Precise Manipulation, and Robust Goal Reasoning

abstractProduction processes in smart factories moved away from a process-centered paradigm into a modular production paradigm, facing the variations in demanded product configurations and deadlines with a flexible production. The RoboCup Logistics League (RCLL) is a robotics competition in the context of in-factory logistics, in which a team of three autonomous mobile robots manufacture dynamically ordered products. The main challenges include task reasoning, multi-agent coordination, and robust execution in a dynamic environment. We present a multi-agent goal reasoning approach where agents continuously reason about which objectives to pursue rather than only planning for a fixed objective. We describe an incremental, distributed formulation of the RCLL problem implemented in the goal reasoning system CLIPS Executive. We elaborate what kind of goals we use in the RCLL, how we use goal trees to define an effective production strategy and how agents coordinate effectively by means of primitive lock actions as well as goal-level resource allocation. The system utilizes a PDDL model to describe domain predicates and actions, as well as to determine the executability and effects of actions during execution. Our agent is able to react to unexpected events, such as a broken machine or a failed action, by monitoring the execution of the plan, re-evaluating goals, and taking over goals which were previously pursued by another robot. We present a detailed evaluation of the system used on real robots
booktitleProceedings of the 13th International Conference on Agents and Artifical Intelligence (ICAART)
titleMulti-Agent Goal Reasoning with the CLIPS Executive in the RoboCup Logistics League

abstractPlanning with numeric state variables has been a challenge for many years, and was a part of the 3rd International Planning Competition (IPC-3). Currently one of the most popular and successful algorithmic techniques in STRIPS planning is to guide search by a heuristic function, where the heuristic is based on relaxing the planning task by ignoring the delete lists of the available actions. We present a natural extension of “ignoring delete lists” to numeric state variables, preserving the relevant theoretical properties of the STRIPS relaxation under the condition that the numeric task at hand is “monotonic”. We then identify a subset of the numeric IPC-3 competition language, “linear tasks”, where monotonicity can be achieved by pre-processing. Based on that, we extend the algorithms used in the heuristic planning system FF to linear tasks. The resulting system Metric-FF is, according to the IPC-3 results which we discuss, one of the two currently most efficient numeric planners.
journaltitleJournal of Artificial Intelligence Research
shorttitleThe Metric-FF Planning System
titleThe Metric-FF Planning System: Translating “Ignoring Delete Lists” to Numeric State Variables

RWTH Aachen University

titleContinual Planning and Execution Monitoring in the Agent Language Golog on a Mobile Robot

RWTH Aachen University

Aachen; Germany

titleGenerating Macro Actions from a Plan Database for Planning on Mobile Robots

abstractWe introduce TACoS, a tool for synthesizing controllers satisfying MTL specifications of undesired behavior with timing constraints. Our contribution extends an existing theoretical approach towards practical applications. The most notable features include: Online labeling to terminate early if a solution has been found, heuristic search to expand the most promising nodes first, search graph pruning to reduce the problem size by pruning irrelevant parts of the search graph, and re-using previously explored search nodes to further reduce the search graph. Finally, multi-threading support allows to make use of modern CPUs with many parallel threads. TACoS comes with a C++ library with minimal external dependencies and simple-to-use API. We evaluate our approach on a number of scenarios and investigate how each of the enhancements improves the performance. The tool is publicly available at https://github.com/morxa/tacos.
booktitleProceedings of the 19th International Conference on Software Engineering and Formal Methods (SEFM)
titleTACoS: A Tool for MTL Controller Synthesis

abstractWhile Golog is an expressive programming language to control the high-level behavior of a robot, it is often tedious to use on a real robotic system. On an actual robot, the user needs to consider low-level details, such as enabling and disabling hardware components, e.g., a camera to detect objects for grasping. In other words, high-level actions usually pose implicit temporal constraints on the low-level platform, which are typically independent of the concrete program to be executed. In this paper, we propose to make these constraints explicit by modeling them as MTL formulas, which enforce the execution of certain low-level platform operations in addition to the main program. Based on results from timed automata controller synthesis, we describe a method to synthesize a controller that executes both the high-level program and the low-level platform operations concurrently in order to satisfy the MTL specification. This allows the user to focus on the high-level behavior without the need to consider low-level operations. We present an extension to Golog by clocks together with the required theoretical foundations as well as decidability results.
titleControlling Golog Programs against MTL Constraints
Computer Science - Artificial Intelligence

abstractTACoS is a tool for synthesizing controllers against specifications of undesired behavior with timing constraints. Given a timed automaton and an MTL specification, the tool synthesizes a controller that guarantees that every possible execution of the system satisfies the given specification. TACoS comes with a C++ library with a simple-to-use API and can read from and write to human-readable text input and output. In this paper, we outline the approach of the tool and present two examples in further detail.
journaltitleScience of Computer Programming
shortjournalScience of Computer Programming
titleControlling Timed Automata against MTL Specifications with TACoS
Controller synthesis,Metric temporal logic,Timed automata

abstractWe introduce a new deductive approach to planning which is based on Horn clauses. Plans as well as situations are represented as terms and, thus, are first-class objects. We do neither need frame axioms nor state-literals. The only rule of inference is the SLDE-resolution rule, i.e. SLD-resolution, where the traditional unification algorithm has been replaced by anE-unification procedure. We exemplify the properties of our method such as forward and backward reasoning, plan checking, and the integration of general theories. Finally, we present the calculus and show that it is sound and complete.
journaltitleNew Generation Computing
shortjournalNew Gener Comput
titleA New Deductive Approach to Planning
Deductive Planning,Equational Reasoning,Logic Programming

Addison-Wesley Longman Publishing Co., Inc.

titleFormal Languages and Their Relation to Automata

ML Research Press

abstractProbabilistic programming languages are a flexible tool for specifying statistical models, but this flexibility comes at the cost of efficient analysis. It is currently difficult to compactly repre...
booktitleProceedings of the 35th International Conference on Machine Learning (PMLR)
titleSound Abstraction and Decomposition of Probabilistic Programs

abstractIn this paper, we introduce a new fragment of the first-order temporal language, called the monodic fragment, in which all formulas beginning with a temporal operator (Since or Until) have at most one free variable. We show that the satisfiability problem for monodic formulas in various linear time structures can be reduced to the satisfiability problem for a certain fragment of classical first-order logic. This reduction is then used to single out a number of decidable fragments of first-order temporal logics and of two-sorted first-order logics in which one sort is intended for temporal reasoning. Besides standard first-order time structures, we consider also those that have only finite first-order domains, and extend the results mentioned above to temporal logics of finite domains. We prove decidability in three different ways: using decidability of monadic second-order logic over the intended flows of time, by an explicit analysis of structures with natural numbers time, and by a composition method that builds a model from pieces in finitely many steps.
journaltitleAnnals of Pure and Applied Logic
shortjournalAnnals of Pure and Applied Logic
titleDecidable Fragments of First-Order Temporal Logics
Classical decision problem,Decidability,Decidable fragments,First-order temporal logic,Temporal databases,Undecidability

abstractAutonomous robots facing a diversity of open environments and performing a variety of tasks and interactions need explicit deliberation in order to fulfill their missions. Deliberation is meant to endow a robotic system with extended, more adaptable and robust functionalities, as well as reduce its deployment cost. The ambition of this survey is to present a global overview of deliberation functions in robotics and to discuss the state of the art in this area. The following five deliberation functions are identified and analyzed: planning, acting, monitoring, observing, and learning. The paper introduces a global perspective on these deliberation functions and discusses their main characteristics, design choices and constraints. The reviewed contributions are discussed with respect to this perspective. The survey focuses as much as possible on papers with a clear robotics content and with a concern on integrating several deliberation functions.
journaltitleArtificial Intelligence
shortjournalArtificial Intelligence
shorttitleDeliberation for Autonomous Robots
titleDeliberation for Autonomous Robots: A Survey

abstractIn this paper, we discuss Procedural Reasoning System (PRS) as Q hagh levlei Control and Supervision language adapted to autonomous robots to represent and execute procedures, scripts and plans in dynamic environments. We discuss the main reasons why PRS as well suited for this type of appldcation: (1) The semantics of its plan [procedure) representation, which is hportant for plan execution and ,goal refinement; (2) Its ability to construct and act on partial (rather than complete) plans; (3) Its ability to pursue goddirected tasks while at the same tame being responsive tQ changing patterns 5f events in bounded time; (4) Its facida'taes for munaging multiple tasks an real-time; (5) Its default mechanisms for handling stringent real-time demands of its environment; and (6) Its metadeve! [or reflective) reasoning capabalities. C-PRS' has; been used to implement an embedded control and supe,rvision system for autonomous mobile robots in two difierent experimentations that we briefly present [Eden arid Martha). We conclude with some suggestions to further develop C-PPZS and with a short review of related work.
booktitleProceedings of the IEEE International Conference on Robotics and Automation (ICRA)
titlePRS: A High Level Supervision and Control Language for Autonomous Mobile Robots

journaltitleProceedings of the 6th International Symposium on Artificial Intelligence, Robotics and Automation in Space (ISAIRAS)
titleA Reactive Model-Based Programming Language for Robotic Space Explorers

abstractWe present an approach to automatic synthesis of specifications given in linear time logic. The approach is based on a translation through universal co-Buchi tree automata and alternating weak tree automata (O. Kupferman and M. Vardi, 2005). By careful optimization of all intermediate automata, we achieve a major improvement in performance. We present several optimization techniques for alternating tree automata, including a game-based approximation to language emptiness and a simulation-based optimization. Furthermore, we use an incremental algorithm to compute the emptiness of nondeterministic Buchi tree automata. All our optimizations are computed in time polynomial in the size of the automaton on which they are computed. We have applied our implementation to several examples and show a significant improvement over the straightforward implementation. Although our examples are still small, this work constitutes the first implementation of a synthesis algorithm for full LTL. We believe that the optimizations discussed here form an important step towards making LTL synthesis practical
booktitle2006 Formal Methods in Computer Aided Design
titleOptimizations for LTL Synthesis
Automata,Automatic logic units,Computational modeling,Contracts,Costs,Debugging,Polynomials,Signal synthesis,Synthesizers,Writing

titleQuantifying In

abstractOver the last two decades, there has been an extensive study of logical formalisms on specifying and verifying real-time systems. Temporal logics have been an important research subject within this direction. Although numerous logics have been introduced for formal specification of real-time and complex systems, an up to date survey of these logics does not exist in the literature. In this paper we analyse various temporal formalisms introduced for specification, including propositional/first-order linear temporal logics, branching temporal logics, interval temporal logics, real-time temporal logics and probabilistic temporal logics. We give decidability, axiomatizability, expressiveness, model checking results for each logic analysed. We also provide a comparison of features of the temporal logics discussed.
journaltitleFrontiers of Computer Science
shortjournalFront. Comput. Sci.
titleA Survey on Temporal Logics for Specifying and Verifying Real-Time Systems
branching temporal logics,decidability,expressiveness,first-order linear temporal logics,interval temporal logics,model checking,probabilistic temporal logics,propositional temporal logics,real-time temporal logics

abstractThis paper is motivated by the need for a formal specification method for real-time systems. In these systemsquantitative temporal properties play a dominant role. We first characterize real-time systems by giving a classification of such quantitative temporal properties. Next, we extend the usual models for temporal logic by including a distance function to measure time and analyze what restrictions should be imposed on such a function. Then we introduce appropriate temporal operators to reason about such models by turning qualitative temporal operators into (quantitative) metric temporal operators and show how the usual quantitative temporal properties of real-time systems can be expressed in this metric temporal logic. After we illustrate the application of metric temporal logic to real-time systems by several examples, we end this paper with some conclusions.
journaltitleReal-Time Systems
titleSpecifying Real-Time Properties with Metric Temporal Logic

Cambridge University Press

abstractThe present paper attempts to state and prove a completeness theorem for the system S5 of [1], supplemented by first-order quantifiers and the sign of equality. We assume that we possess a denumerably infinite list of individual variables a, b, c, …, x, y, z, …, xm, ym, zm, … as well as a denumerably infinite list of n-adic predicate variables Pn, Qn, Rn, …, Pmn, Qmn, Rmn,…; if n=0, an n-adic predicate variable is often called a “propositional variable.” A formula Pn(x1, …,xn) is an n-adic prime formula; often the superscript will be omitted if such an omission does not sacrifice clarity.
journaltitleThe Journal of Symbolic Logic
titleA Completeness Theorem in Modal Logic

journaltitleZeitschrift für mathematische Logik und Grundlagen der Mathematik
titleSemantical Analysis of Modal Logic I: Normal Modal Propositional Calculi

abstractWe outline an approach for reasoning about events and time within a logic programming framework. The notion of event is taken to be more primitive than that of time and both are represented explicitly by means of Horn clauses augmented with negation by failure. The main intended applications are the updating of databases and narrative understanding. In contrast with conventional databases which assume that updates are made in the same order as the corresponding events occur in the real world, the explicit treatment of events allows us to deal with updates which provide new information about the past. Default reasoning on the basis of incomplete information is obtained as a consequence of using negation by failure. Default conclusions are automatically withdrawn if the addition of new information renders them inconsistent. Because events are differentiated from times, we can represent events with unknown times, as well as events which are partially ordered and concurrent.
journaltitleNew Generation Computing
shortjournalNew Gen. Comput.
titleA Logic-Based Calculus of Events
Database Updates,Default Reasoning,Event Calculus,Logic Programming,PROLOG,Temporal Logic

booktitleProceedings of the 17th International Joint Conference on Artificial Intelligence (IJCAI)
titleExecuting Reactive, Model-Based Programs through Graph-Based Temporal Planning

Berlin, Heidelberg

abstractGOLOG is a high-level programming language for the specification of complex actions. It combines the situation calculus with control structures known from conventional programming languages. Given a suitable axiomatization of what the world is like initially and how the primitive actions change the world, the GOLOG interpreter derives for each program a corresponding linear sequence of legally executable primitive actions, if one exists. Despite its expressive power, GOLOG's applicability is severely limited because the derivation of a linear sequence of actions requires that the outcome of each action is known beforehand. Sensing actions do not meet this requirement since their outcome can only be determined by executing them and not by reasoning about them. In this paper we extend GOLOG by incorporating sensing actions. Instead of producing a linear sequence of actions, the new interpreter yields a tree of actions. The idea is that a particular path in the tree represents a legal execution of primitive actions conditioned on the possible outcome of sensing actions along the way.
booktitleLogical Foundations for Cognitive Agents: Contributions in Honor of Ray Reiter
titleOn Sensing and Off-Line Interpreting in GOLOG
Frame Problem,Initial Situation,Linear Sequence,Primitive Action,Situation Calculus

New York, NY

abstractPnueli [15] has recently introduced the idea of using temporal logic [18] as the logical basis for proving correctness properties of concurrent programs. This has permitted an elegant unifying formulation of previous proof methods. In this paper, we attempt to clarify the logical foundations of the application of temporal logic to concurrent programs. In doing so, we will also clarify the relation between concurrency and nondeterminism, and identify some problems for further research.In this paper, we consider logics containing the temporal operators "henceforth" (or "always") and "eventually" (or "sometime"). We define the semantics of such a temporal logic in terms of an underlying model that abstracts the fundamental concepts common to almost all the models of computation which have been used. We are concerned mainly with the semantics of temporal logic, and will not discuss in any detail the actual rules for deducing theorems.We will describe two different temporal logics for reasoning about a computational model. The same formulas appear in both logics, but they are interpreted differently. The two interpretations correspond to two different ways of viewing time: as a continually branching set of possibilities, or as a single linear sequence of actual events. The temporal concepts of "sometime" and "not never" ("not always not") are equivalent in the theory of linear time, but not in the theory of branching time – hence, our title. We will argue that the logic of linear time is better for reasoning about concurrent programs, and the logic of branching time is better for reasoning about nondeterministic programs.The logic of linear time was used by Pnueli in [15], while the logic of branching time seems to be the one used by most computer scientists for reasoning about temporal concepts. We have found this to cause some confusion among our colleagues, so one of our goals has been to clarify the formal foundations of Pnueli's work.The following section gives an intuitive discussion of temporal logic, and Section 3 formally defines the semantics of the two temporal logics. In Section 4, we prove that the two temporal logics are not equivalent, and discuss their differences. Section 5 discusses the problems of validity and completeness for the temporal logics. In Section 6, we show that there are some important properties of the computational model that cannot be expressed with the temporal operators "henceforth" and "eventually", and define more general operators.
booktitleProceedings of the 7th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL)
shorttitle"Sometime" Is Sometimes "Not Never"
title"Sometime" Is Sometimes "Not Never": On the Temporal Logic of Programs

Annals of Mathematics

journaltitleAnnals of Mathematics
titleOn Fraisse's Order Type Conjecture

abstractThis paper proposes a new logic programming language called GOLOG whose interpreter automatically maintains an explicit representation of the dynamic world being modeled, on the basis of user supplied axioms about the preconditions and effects of actions and the initial state of the world. This allows programs to reason about the state of the world and consider the effects of various possible courses of action before committing to a particular behavior. The net effect is that programs may be written at a much higher level of abstraction than is usually possible. The language appears well suited for applications in high level control of robots and industrial processes, intelligent software agents, discrete event simulation, etc. It is based on a formal theory of action specified in an extended version of the situation calculus. A prototype implementation in Prolog has been developed.
journaltitleJournal of Logic Programming
titleGOLOG: A Logic Programming Language for Dynamic Domains

AAAI Press

abstractBased on weighted possible-world semantics, Belle and Lakemeyer recently proposed the logic DS, a probabilistic extension of a modal variant of the situation calculus with a model of belief. The lo...
booktitleProceedings of the 18th International Conference on Principles of Knowledge Representation and Reasoning (KR)
titleOn the Progression of Belief

abstractWe examine the computational complexity of testing and finding small plans in probabilistic planning domains with both flat and propositional representations. The complexity of plan evaluation and existence varies with the plan type sought; we examine totally ordered plans, acyclic plans, and looping plans, and partially ordered plans under three natural definitions of plan value. We show that problems of interest are complete for a variety of complexity classes: PL, P, NP, co-NP, PP, NPP̂P, co-NPP̂P, and PSPACE. In the process of proving that certain planning problems are complete for NPP̂P, we introduce a new basic NPP̂P-complete problem, E-MAJSAT, which generalizes the standard Boolean satisfiability problem to computations involving probabilistic quantities; our results suggest that the development of good heuristics for E-MAJSAT could be important for the creation of efficient algorithms for a wide variety of problems.
journaltitleJournal of Artificial Intelligence Research
titleThe Computational Complexity of Probabilistic Planning

New York, NY, USA

abstractMetric Temporal Logic MTL0,$\infty$ is a timed extension of linear temporal logic, LTL, with time intervals whose left endpoints are zero or whose right endpoints are infinity. Whereas the satisfiability and model-checking problems for MTL0,$\infty$ are both decidable, we note that the controller synthesis problem for MTL0,$\infty$ is unfortunately undecidable. As a remedy of this we propose an approximate method to the synthesis problem, which we demonstrate to be adequate and scalable to practical examples. We define a method for converting MTL0,$\infty$ formulas into (nondeterministic) Timed Game Büchi Automata and furthermore show how to construct determinized over- and underapproximation of a such. For the proposed method, we present a toolchain seamlessly integrating the needed components for practical MTL0,$\infty$ synthesis. Lastly we demonstrate on a pair of case-studies the applicability and scalability of the proposed method.
booktitleProceedings of the 24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software
titlePractical Controller Synthesis for MTL0,$\infty$
Controller Synthesis,Metric Temporal Logic,Timed Büchi Automata

abstractMany autonomous systems such as mobile robots, UAVs or spacecraft, have limited resource capacities and move in dynamic environments. Performing on-board mission plan- ning and execution in such a context requires deliberative capabilities to generate plans achieving mission goals while respecting deadlines and resource constraints, as well as run-time plan adaption mechanisms during execution. In this paper we propose a framework to integrate deliberative planning, plan repair and execution control in a dynamic environment with stringent temporal constraints. It is based on lifted partial order temporal planning techniques which produce flexible plans and allow, under certain conditions discussed in the paper, plan repair interleaved with plan ex- ecution. This framework has been implemented using the IXTET planner and used to control a robotic platform.
booktitleProceedings of the 19th National Conference on Artificial Intelligence (AAAI)
titleInterleaving Temporal Planning and Execution in Robotics Domains
constraints,Copyright © 2004 American Association for Artifici,IXTET,partial order planning,temporal

Morgan Kaufmann

abstractWe apply circumscription to formalizing reasoning about the effects of actions in the framework of situation calculus. An axiomatic description of causal connections between actions and changes allows us to solve the qualification problem and the frame problem using only simple forms of circumscription. The method is applied to the Hanks—McDermott shooting problem and to a blocks world in which blocks can be moved and painted.
booktitleThe Frame Problem in Artificial Intelligence
titleFormal Theories of Action

abstractThe situation calculus is a logical language for representing changes. It was first introduced by McCarthy in 1963 and was described in further details by McCarthy and Hayes in 1969. The basic concepts in the situation calculus are situations, actions, and fluents. Actions make the dynamic world change from one situation to another when performed by agents. Fluents are situation-dependent functions that describe the effects of actions; they are of two types: relational fluents and functional fluents. The former have only two values, which are true or false, whereas the latter can have a range of values. For instance, one may have a relational fluent called “handempty,” which is true in a situation if a robot's hand is not holding anything. One may also have a functional fluent called “battery level” whose value in a situation is an integer between 0 and 100 denoting the total battery power remaining on one's laptop computer. According to McCarthy and Hayes, a situation is the complete state of the universe at an instance of time. But for Reiter, a situation is the same as its history, which is the finite sequence of actions that has been performed since the initial situation S0. This chapter discusses Reiter's foundational axioms. Whatever the interpretation, a unique feature of the situation calculus is that situations are first-order objects that can be quantified over. This makes the situation calculus a powerful formalism for representing change and distinguishes it from other formalisms such as a dynamic logic.
booktitleFoundations of Artificial Intelligence
titleSituation Calculus

American Association for Artificial Intelligence

abstractGolog is a situation calculus-based logic programming language for high-level robotic control, This paper explores Hoare's axiomatic approach to program verification in the Golog context. We present a novel Hoare-style proof system for partial correctness of Golog programs. We prove total soundness of the proof system, and relative completeness of a subsystem of it for procedureless Golog programs. Examples are given to illustrate the use of the proof system.
booktitleProceedings of the 18th National Conference on Artificial Intelligence (AAAI)
titleA Hoare-Style Proof System for Robot Programs

RWTH Aachen University

titleProjection in a Probabilistic Epistemic Logic and Its Application to Belief-based Program Verification

Cambridge, MA, USA

MIT Press

abstractThis book describes in detail the relationship between symbolic representations of knowledge and abstract states of knowledge, exploring along the way the foundations of knowledge, knowledge bases, knowledge-based systems, and knowledge representation and reasoning.
titleThe Logic of Knowledge Bases

San Francisco, CA, USA

Morgan Kaufmann Publishers Inc.

booktitleProceedings of the 9th International Conference on Principles of Knowledge Representation and Reasoning (KR)
titleEvaluation-Based Reasoning with Disjunctive Information in First-Order Knowledge Bases

AAAI Press

abstractThe situation calculus, as proposed by McCarthy and Hayes, and developed over the last decade by Reiter and co-workers, is reconsidered. A new logical variant is proposed that captures much of the expressive power of the original, but where certain technical results are much more easily proven. This is illustrated using two existing non-trivial results: the regression theorem and the determinacy of knowledge theorem of Reiter. We also obtain a regression theorem for knowledge, and show how to reduce reasoning about knowledge and action to non-epistemic non-dynamic reasoning about the initial situation.
booktitleProceedings of the 9th International Conference on Principles of Knowledge Representation and Reasoning (KR)
titleSituations, Si! Situation Terms, No!

San Francisco, CA, USA

Morgan Kaufmann Publishers Inc.

abstractA basic reasoning problem in dynamic systems is the projection problem: determine if a formula holds after a sequence of actions has been performed. In this paper, we propose a tractable solution to the projection problem in the presence of incomplete first-order knowledge and contextdependent actions. Our solution is based on a type of progression, that is, we progress the initial knowledge base (KB) wrt the action sequence and answer the query against the resulting KB. The form of reasoning we propose is always logically sound and is also logically complete when the query is in a certain normal form and the agent has complete knowledge about the context of any context-dependent actions.
booktitleProceedings of the 19th International Joint Conference on Artificial Intelligence
titleTractable Reasoning with Incomplete First-Order Knowledge in Dynamic Systems with Context-Dependent Actions

abstractCognitive robotics is the study of the knowledge representation and reasoning problems faced by an autonomous robot (or an agent) in a dynamic and incompletely known world. This chapter presents the idea of knowledge representation and reasoning for the purpose of high-level robotic control to be central to cognitive robotics. This connects cognitive robotics not only to (traditional and less cognitive) robotics but also to other areas of artificial intelligence (AI) such as planning and agent-oriented programming. To illustrate the knowledge representation and reasoning issues relevant to high-level robotic control, the chapter discusses a Reiter's variant of the situation calculus. The situation calculus also deals with actions whose effects are deterministic—that is, where there is no doubt as to which fluents change and which do not. The chapter discusses some of the knowledge representation issues that arise in the context of cognitive robotics and describes problems in automated reasoning in the same setting.
booktitleFoundations of Artificial Intelligence
titleCognitive Robotics

San Francisco, CA, USA

Morgan Kaufmann Publishers Inc.

abstractIn a seminal paper, Lin and Reiter introduced the notion of progression for basic action theories in the situation calculus. Unfortunately, progression is not first-order definable in general. Recently, Vassos, Lakemeyer, and Levesque showed that in case actions have only local effects, progression is first-order representable. However, they could show computability of the first-order representation only for a restricted class. Also, their proofs were quite involved. In this paper, we present a result stronger than theirs that for local-effect actions, progression is always first-order definable and computable. We give a very simple proof for this via the concept of forgetting. We also show first-order definability and computability results for a class of knowledge bases and actions with non-local effects. Moreover, for a certain class of local-effect actions and knowledge bases for representing disjunctive information, we show that progression is not only first-order definable but also efficiently computable.
booktitleProceedings of the 21st International Joint Conference on Artificial Intelligence (IJCAI)
titleOn First-Order Definability and Computability of Progression for Local-Effect Actions and Beyond

abstractThe situation calculus, as proposed by McCarthy and Hayes, and developed over the last decade by Reiter and co-workers, is reconsidered. A new logical variant called ES is proposed that captures much of the expressive power of the original, but where certain technical results are much more easily proved. This is illustrated using two existing non-trivial results: the determinacy of knowledge theorem of Reiter and the regression theorem, which reduces reasoning about the future to reasoning about the initial situation. Furthermore, we show the correctness of our approach by embedding ES in Reiter's situation calculus.
journaltitleArtificial Intelligence
shortjournalArtificial Intelligence
titleA Semantic Characterization of a Useful Fragment of the Situation Calculus with Knowledge
Knowledge representation,Reasoning about action

AAAI Press

booktitleProceedings of the 30th International Joint Conference on Artificial Intelligence (IJCAI)
titleReasoning about Beliefs and Meta-Beliefs by Regression in an Expressive Probabilistic Action Logic

Berlin, Heidelberg

abstractIn this paper, we study model checking of timed automata (TAs), and more precisely we aim at finding efficient model checking for subclasses of TAs. For this, we consider model checking TCTL and TCTL $\leq$,$\geq$ over TAs with one clock or two clocks.
booktitleCONCUR 2004 - Concurrency Theory
titleModel Checking Timed Automata with One or Two Clocks
Classical Graph,Kripke Structure,Model Check,Reachability Problem,Time Automaton

Cambridge University Press

abstractA series of temporal reasoning tasks are identified which motivate the consideration and application of temporal logics in artificial intelligence. There follows a discussion of the broad issues involved in modelling time and constructing a temporal logic. The paper then presents a detailed review of the major approaches to temporal logics: first-order logic approaches, modal temporal logics and reified temporal logics. The review considers the most significant exemplars within the various approaches, including logics due to Russell, Hayes and McCarthy, Prior, McDermott, Allen, Kowalski and Sergot. The logics are compared and contrasted, particularly in their treatments of change and action, the roles they seek to fulfil and the underlying models of time on which they rest. The paper concludes with a brief consideration of the problem of granularity—a problem of considerable significance in temporal reasoning, which has yet to be satisfactorily treated in a temporal logic.
journaltitleThe Knowledge Engineering Review
titleA Review of Temporal Logics

Berlin, Heidelberg

abstractEfficient automatic model-checking algorithms for real-time systems have been obtained in recent years based on the state-region graph technique of Alur, Courcoubetis and Dill. However, these algorithms are faced with two potential types of explosion arising from parallel composition: explosion in the space of control nodes, and explosion in the region space over clock-variables.
booktitleFundamentals of Computation Theory
titleModel-Checking for Real-Time Systems
Atomic Proposition,Binary Decision Diagram,Label Transition System,Model Check,Parallel Composition

Berlin, Heidelberg

booktitleComputer Aided Verification (CAV)
titleUppaal: Status & Developments
Danish National Research Foundation,Formal Description Technique,Label Transition System,Reachability Analysis,Symbolic State

Springer, Berlin, Heidelberg

abstractAn extension of propositional temporal logic that includes operators referring to a bounded past is considered. An exponential time decision procedure and a complete axiomatic system are presented. A suggested normal form leads to a syntactic classification of safety...
booktitleLogics of Programs
titleThe Glory of the Past

abstractOne way to think about a STRIPS operator is as a mapping from databases to databases, in the following sense: suppose we want to know what the world would be like if an action, represented by the STRIPS operator $\alpha$, were done in some world, represented by the STRIPS database D0. To find out, simply perform the operator $\alpha$ on D0 (by applying $\alpha$'s elementary add and delete revision operators to D0). We describe this process as progressing the databaseD0 in response to the action $\alpha$. In this paper, we consider the general problem of progressing an initial database in response to a given sequence of actions. We appeal to the situation calculus and an axiomatization of actions which addresses the frame problem (Reiter (1991)). This setting is considerably more general than STRIPS. Our results concerning progression are mixed. The (surprising) bad news is that, in general, to characterize a progressed database we must appeal to second-order logic. The good news is that there are many useful special cases for which we can compute the progressed database in first-order logic; not only that, we can do so efficiently. Finally, we relate these results about progression to STRIPS-like systems by providing a semantics for such systems in terms of a purely declarative situation calculus axiomatization for actions and their effects. On our view, STRIPS operators provide a mechanism for computing the progression of an initial situation calculus database under the effects of an action. We illustrate this idea by describing two different STRIPS mechanisms, and proving their correctness with respect to their situation calculus specifications.
journaltitleArtificial Intelligence
shortjournalArtificial Intelligence
titleHow to Progress a Database
Progression,Regression,situation,Situation calculus,STRIPS,Strongest postconditions,Theories of actions

booktitleAAAI Spring Symposium on Integrating Robotics Research
titleHigh-Level Robotic Control: Beyond Planning

San Jose, California

AAAI Press

abstractWe propose a representation of Concurrent actions; rather than invent a new formalism, we model them within the standard situation calculus by introducing the notions of global actions and primitive actions, whose relationship is analogous to' that between situations and fluents. The result is a framework in which situations and actions play quite symmetric roles. The rich structure of actions gives rise to' a new problem, which, due to' this symmetry between actions and situations, is analogous to' the traditional frame problem. In [Lin and Shoham 1991] we provided a solution to' the frame problem based on a formal adequacy criterion called "epistemological completeness." Here we show how to' solve the new problem based on the same adequacy criterion.
booktitleProceedings of the 10th National Conference on Artificial Intelligence (AAAI)
titleConcurrent Actions in the Situation Calculus

Berlin, Heidelberg

abstractA notion of alternating timed automata is proposed. It is shown that such automata with only one clock have decidable emptiness problem. This gives a new class of timed languages which is closed under boolean operations and which has an effective presentation. We prove that the complexity of the emptiness problem for alternating timed automata with one clock is non-primitive recursive. The proof gives also the same lower bound for the universality problem for nondeterministic timed automata with one clock thereby answering a question asked in a recent paper by Ouaknine and Worrell.
booktitleFoundations of Software Science and Computational Structures
titleAlternating Timed Automata
Boolean Operation,Channel System,Label Transition System,Reachability Problem,Transition Rule

abstractThere is a strong demand for robots to work in environments, such as aircraft manufacturing, where they share tasks with humans and must quickly adapt to each other's needs. To do so, a robot must both infer the intent of humans, and must adapt accordingly. The literature to date has made great progress on these two tasks - recognition and adaptation - but largely as separate research activities. In this paper, we present a unified approach to these two problems, in which recognition and adaptation occur concurrently and holistically.  Key to our approach is a task representation that uses choice to represent alternative plans for both the human and robot, allowing a single set of algorithms to simultaneously achieve recognition and adaptation. To achieve such fluidity, a labeled propagation mechanism is used where decisions made by the human and robot during execution are propagated to relevant future open choices, as determined by causal link analysis, narrowing the possible options that the human would reasonably take (hence achieving intent recognition) as well as the possible actions the robot could consistently take (adaptation). This paper introduces Pike, an executive for human-robot teamwork that quickly adapts and infers intent based on the preconditions of actions in the plan, temporal constraints, unanticipated disturbances, and choices made previously (by either robot or human).  We evaluate Pike's performance and demonstrate it on a household task in a human-robot team testbed.
booktitleProceedings of the 24th International Conference on Automated Planning and Scheduling (ICAPS)
titleConcurrent Plan Recognition and Execution for Human-Robot Teams

abstractWe pursue the fine analysis of the quasi-orderings $\preccurlyeq\exists\forall$ and $\preccurlyeq\forall\exists$ on the power set of a quasi-ordering (Q,$\preccurlyeq$). We set X$\preccurlyeq\exists\forall$Y if every x$\in$X is majorized in $\preccurlyeq$ by some y$\in$Y, and X$\preccurlyeq\forall\exists$Y if every y$\in$Y is minorized in $\preccurlyeq$ by some x$\in$X. We show that both these quasi-orderings are $\alpha$-wqo if and only if the original quasi-ordering is ($\alpha$ $\cdot$ $\omega$)-wqo. For $\preccurlyeq\forall\exists$ this holds also restricted to finite subsets, thus providing an example of a finitary operation on quasi-orderings which does not preserve wqo but preserves bqo.
titleFine Analysis of the Quasi-Orderings on the Power Set
better quasi-ordering,well quasi-ordering,$\alpha$-wqo

European Association for Theoretical Computer Science

abstractWe positively answer the old question whether temporal logic with past is more succinct than pure-future temporal logic. Surprisingly, the proof is quite simple and elementary, although the question has been open for twenty years.
journaltitleBulletin- European Association for Theoretical Computer Science
titleTemporal Logic with Past Is Exponentially More Succinct

booktitleIROS Workshop on Bringing Constraint-Based Robot Programming to Real-World Applications (CobaRoP)
titleConstraint-Based Plan Transformation in a Safe and Usable GOLOG Language

abstractWe present golog++, a high-level agent programming and interfacing framework that offers a temporal constraint language to explicitly model layer-penetrating contingencies in low-level platform behavior. It can be used to maintain a clear separation between an agent's domain model and certain quirks of its execution platform that affect problem solving behavior. Our system reasons about the execution of an abstract (i.e. exclusively domain-bound) plan on a particular execution platform. This way, we avoid compounding the complexity of the planning problem while improving the modularity of both golog and the user code. On a run-through example from the well-known blocksworld domain, we demonstrate the entire process from domain modeling and platform modeling to plan transformation and platform-specific plan execution.
booktitleProceedings of the 13th International Conference on Agents and Artifical Intelligence (ICAART)