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)
titlePortable High-Level Agent Programming with Golog++

booktitleProceedings of the Symposium on Mechanization of Thought Processes
titlePrograms with Common Sense

abstractThis chapter discusses the mathematical theory of computation. Computation essentially explores how machines can be made to carry out intellectual processes. Any intellectual process that can be carried out mechanically can be performed by a general purpose digital computer. There are three established directions of mathematical research that are relevant to the science of computation—namely, numerical analysis, theory of computability, and theory of finite automata. The chapter explores what practical results can be expected from a suitable mathematical theory. Further, the chapter presents several descriptive formalisms with a few examples of their use and theories that enable to prove the equivalence of computations expressed in these formalisms. A few mathematical results about the properties of the formalisms are also presented.
booktitleStudies in Logic and the Foundations of Mathematics
titleA Basis for a Mathematical Theory of Computation

Stanford University

titleSituations, Actions, and Causal Laws
typeTechnical Report

abstractHumans and intelligent computer programs must often jump to the conclusion that the objects they can determine to have certain properties or relations are the only objects that do. Circumscription formalizes such conjectural reasoning.
journaltitleArtificial Intelligence
shortjournalArtificial Intelligence
titleCircumscription—A Form of Non-Monotonic Reasoning

Morgan Kaufmann

abstractArtificial intelligence (AI) problem has been divided into two parts—an epistemological part and a heuristic part. This chapter further explains this division, explains some of the epistemological problems, and presents some new results and approaches. The epistemological part of AI studies what kinds of facts about the world are available to an observer with given opportunities to observe, how these facts can be represented in the memory of a computer, and what rules permit legitimate conclusions to be drawn from these facts. It leaves aside the heuristic problems of how to search spaces of possibilities and how to match patterns. Considering epistemological problems separately has the following advantages. (1) The same problems of what information is available to an observer and what conclusions can be drawn from information arise in connection with a variety of problem solving tasks. (2) A single solution of the epistemological problems can support a wide variety of heuristic approaches to a problem. (3) AI is a very difficult scientific problem, so there are great advantages in finding parts of the problem that can be separated out and separately attacked.
booktitleReadings in Artificial Intelligence
titleEpistemological Problems of Artificial Intelligence

abstractWe present a new and more symmetric version of the circumscription method of non-monotonic reasoning first described by McCarthy [9] and some applications to formalizing common-sense knowledge. The applications in this paper are mostly based on minimizing the abnormality of different aspects of various entities. Included are non-monotonic treatments of “is-a” hierarchies, the unique names hypothesis, and the frame problem. The new circumscription may be called formula circumscription to distinguish it from the previously defined domain circumscription and predicate circumscription. A still more general formalism called prioritized circumscription is briefly explored.
journaltitleArtificial Intelligence
shortjournalArtificial Intelligence
titleApplications of Circumscription to Formalizing Common-Sense Knowledge

The AIPS-98 Planning Competition Committee

titlePDDL - The Planning Domain Definition Language

abstractThe 1998 Planning Competition at the AI Planning Systems Conference was the first of its kind. Its goal was to create planning domains that a wide variety of planning researchers could agree on to make comparison among planners more meaningful, measure overall progress in the field, and set up a framework for long-term creation of a repository of problems in a standard notation. A rules committee for the competition was created in 1997 and had long discussions on how the contest should go. One result of these discussions was the pddl notation for planning domains. This notation was used to set up a set of planning problems and get a modest problem repository started. As a result, five planning systems were able to compete when the contest took place in June 1998. All these systems solved problems in the strips framework, with some slight extensions. The attempt to find domains for other forms of planning foundered because of technical and organizational problems. In spite of this problem, the competition achieved its goals partially in that it con-firmed that substantial progress had occurred in some subfields of planning, and it allowed qualitative comparison among different planning algorithms. It is urged that the competition continue to take place and to evolve.
journaltitleAI Magazine
titleThe 1998 AI Planning Systems Competition

titleA Reactive Plan Language
typeTechnical Report

abstractThis paper presents a general model for temporal reasoning that is capable of handling both qualitative and quantitative information. This model allows the representation and processing of many types of constraints discussed in the literature to date, including metric constraints (restricting the distance between time points) and qualitative, disjunctive constraints (specifying the relative position of temporal objects). Reasoning tasks in this unified framework are formulated as constraint satisfaction problems and are solved by traditional constraint satisfaction techniques, such as backtracking and path consistency. New classes of tractable problems are characterized, involving qualitative networks augmented by quantitative domain constraints, some of which can be solved in polynomial time using arc and path consistency.
journaltitleArtificial Intelligence
shortjournalArtificial Intelligence
titleCombining Qualitative and Quantitative Constraints in Temporal Reasoning

journaltitleMachine Intelligence
relatedstringReprinted as
titleSome Philosophical Problems from the Standpoint of Artificial Intelligence

William Kaufmann Inc.

abstractA simulation relation between programs is defined which is quasi-ordering. Mutual simulation is then an equivalence relation, and by dividing out by it we abstract from a program such details as how the sequencing is controlled and how data is represented. The equivalence classes are approxiamtions to the algorithms which are realized, or expressed, by their member programs. A technique is given and illustrated for proving simulation and equivalence of programs; there is an analogy with Floyd”s technique for proving correctness of programs. Finally, necessary and sufficient conditions for simulation are given.
booktitleProceedings of the 2nd International Joint Conference on Artificial Intelligence (IJCAI)
titleAn Algebraic Definition of Simulation between Programs.

abstractThis paper shows how the Situation Calculus can be extended to deal both with `narratives' and with domains containing real-valued parameters, whose actual values may vary continuously between the occurrences of actions. In particular, a domain is represented where action occurrences may be `triggered' at instants in time when certain parameters reach particular values. Its formalisation requires the integration of several types of default reasoning. Hence Baker's circumscriptive solution to the frame problem is extended to re ect the assumptions that by default a given action does not occur at a given time point, that by default a given set of parameter values does not trigger a given action, and that by default a given action occurrence does not result in a discontinuity for a given parameter. Regarding the minimisation of discontinuities, the example illustrates how circumstances can arise where, at a particular time point, discontinuities in some parameters can be `traded' for discontinuities in others. It is argued that, in general, in such cases extra domain-speci c information will be necessary in order to eliminate anomalous models of the domain.
booktitleProceedings of the 12th European Conference on Artificial Intelligence (ECAI)
titleA Case Study in Reasoning about Actions and Continuous Change

Englewood Cliffs, N.J

titleComputation: Finite and Infinite Machines

Morgan Kaufmann

abstractThis paper discusses the problems of representing and reasoning with information about knowledge and action. The first section discusses the importance of having systems that understand the concept of knowledge, and how knowledge is related to action. Section 2 points out some of the special problems that are involved in reasoning about knowledge, and section 3 presents a logic of knowledge based on the idea of possible worlds. Section 4 integrates this with a logic of actions and gives an example of reasoning in the combined system. Section 5 makes some concluding comments.
booktitleReadings in Artificial Intelligence
titleReasoning about Knowledge and Action

booktitleProceedings of the 2nd National Conference on Artificial Intelligence (AAAI)
titleThe Role of Logic in Knowledge Representation and Commonsense Reasoning

booktitleFormal Theories of the Commonsense World
titleA Formal Theory of Knowledge and Action

Berlin, Heidelberg

abstractThis paper presents algorithms for the automatic synthesis of real-time controllers by finding a winning strategy for certain games defined by the timed-automata of Alur and Dill. In such games, the outcome depends on the players' actions as well as on their timing. We believe that these results will pave the way for the application of program synthesis techniques to the construction of real-time embedded systems from their specifications.
booktitleSTACS 95
titleOn the Synthesis of Discrete Controllers for Timed Systems

abstractA narrative is a course of real events about which we might have incomplete information. Formalisms for reasoning about action may be broadly divided into those which are narrative-based, such as the event calculus of Kowalski and Sergot, and those which reason on the level of hypothetical sequences of actions, in particular the situation calculus. This paper bridges the gap between these types of formalism by supplying a technique for linking incomplete narrative descriptions to situation calculus domain formulae written in the usual style using a Result function. Particular attention is given to actions with duration and overlapping actions. By illuminating the relationship between these two different styles of representation, the paper moves us one step closer to a full understanding of the space of all possible formalisms for reasoning about action.
journaltitleJournal of Logic and Computation
shortjournalJournal of Logic and Computation
titleNarratives in the Situation Calculus

booktitleProceedings of the 11th Cognitive Robotics Workshop 2018 (CogRob)
titleGolog++: An Integrative System Design

AAAI Press

booktitleProceedings of the 3rd International Conference on Artificial Intelligence Planning Systems (AIPS)
titleA Procedural Knowledge Approach to Task-Level Control

Cambridge University Press

abstractLet A be the set of all ascending finite sequences (with at least one term) of positive integers. Let s, t $\in$ A. Write s $\vartriangleleft$ t if there exist m, n, x1, …, xn such that m $<$ n and x1 $<$ … $<$ xn and s is x1, …, xm and t is x2, x3, …, xn. Call a subset S of A a P-block if, for every infinite ascending sequence x1, x2, … of positive integers, there exists an m such that x1, …, xm belongs to S. A quasi-ordered set Q (i.e. a set on which a reflexive and transitive relation $\leq$ is defined) is better-quasi-ordered if, for every P-block S and every function f:S → Q, there exist s, t $\in$ S such that s $\vartriangleleft$ t and f(s) $\leq$ f(t). It is proved that any set of (finite or infinite) trees is better-quasi-ordered if T1 $\leq$ T2 means that the tree T1 is homeomorphic to a subtree of the tree T2. This establishes a conjecture of J. B.Kruskal that, if T1, T2, … is an infinite sequence of trees, then there exist i, j such that i $<$ j and Ti $\leq$ Tj.
journaltitleMathematical Proceedings of the Cambridge Philosophical Society
titleOn Well-Quasi-Ordering Infinite Trees

abstractThe SHOP2 planning system received one of theawards for distinguished performance in the 2002 International Planning Competition. This paper describes the features of SHOP2 which enabled it to excel in the competition, especially those aspects of SHOP2 that deal with temporal and metric planning domains. 1.
journaltitleJournal of Artificial Intelligence Research
titleSHOP2 : An HTN Planning System

abstractWe describe a new problem solver called STRIPS that attempts to find a sequence of operators in a space of world models to transform a given initial world model in which a given goal formula can be proven to be true. STRIPS represents a world model as an arbitrary collection in first-order predicate calculus formulas and is designed to work with models consisting of large numbers of formula. It employs a resolution theorem prover to answer questions of particular models and uses means-ends analysis to guide it to the desired goal-satisfying model. © 1971.
journaltitleArtificial intelligence
titleSTRIPS: A New Approach to the Application of Theorem Proving to Problem Solving
heuristic search,Problem solving,robot planning,theorem proving

abstractThe high-level decision making process of an autonomous robot can be seen as an hierarchically organised entity, where strategical decisions are made on the topmost layer, while the bottom layer serves as driver for the hardware. In between is a layer with monitoring and reporting functionality. In this paper we propose a behaviour engine for this middle layer which, based on formalism of hybrid state machines (HSMs), bridges the gap between high-level strategic decision making and low-level actuator control. The behaviour engine has to execute and monitor behaviours and reports status information back to the higher level. To be able to call the behaviours or skills hierarchically, we extend the model of HSMs with dependencies and sub-skills. These Skill-HSMs are implemented in the lightweight but expressive Lua scripting language which is well-suited to implement the behaviour engine on our target platform, the humanoid robot Nao.
booktitleRoboCup 2009: Robot Soccer World Cup XIII
titleA Lua-based Behavior Engine for Controlling the Humanoid Robot Nao

abstractIntegrating planning and execution which treats either component as a black box may lead to disparate representations of the domain or information currently known. Consistency and bidirectional information flow are then hard to ensure. However, the separation of these concerns is still useful from an integration point of view. In this paper, we discuss the integration of planning systems using the Planning Domain Definition Language (PDDL) with an executive based on the CLIPS rule-based production system. In particular, we describe how we achieved one common and unified domain model used by both systems and some additions we add for the execution model. We also show how the execution model enables effective execution monitoring and selective replanning.
booktitleICAPS Workshop on Integrated Planning, Acting, and Execution (IntEx)
titleCLIPS-based Execution for PDDL Planners

booktitleProceedings of the 29th International Conference on Automated Planning and Scheduling (ICAPS)
titleGoal Reasoning in the CLIPS Executive for Integrated Planning and Execution

Berlin, Heidelberg

titleIsabelle/HOL: A Proof Assistant for Higher-Order Logic

journaltitleLernende Automaten
titleGPS, a Program That Simulates Human Thought

Berlin, Heidelberg

abstractWe study the decidability and complexity of verification problems for timed automata over time intervals of fixed, bounded length. One of our main results is that time-bounded language inclusion for timed automata is 2EXPSPACE-Complete. We also investigate the satisfiability and model-checking problems for Metric Temporal Logic (MTL), as well as monadic first- and second-order logics over the reals with order and the + 1 function (FO( $<$ , + 1) and MSO( $<$ , + 1) respectively). We show that, over bounded time intervals, MTL satisfiability and model checking are EXPSPACE-Complete, whereas these problems are decidable but non-elementary for the predicate logics. Nevertheless, we show that MTL and FO( $<$ , + 1) are equally expressive over bounded intervals, which can be viewed as an extension of Kamp's well-known theorem to metric logics.
booktitleCONCUR 2009 - Concurrency Theory
titleTime-Bounded Verification
Linear Temporal Logic,Linear Temporal Logic Formula,Model Check,Predicate Logic,Temporal Logic

abstractWe consider the language inclusion problem for timed automata: given two timed automata A and B, are all the timed traces accepted by B also accepted by A? While this problem is known to be undecidable, we show here that it becomes decidable if A is restricted to having at most one clock. This is somewhat surprising, since it is well-known that there exist timed automata with a single clock that cannot be complemented. The crux of our proof consists in reducing the language inclusion problem to a reachability question on an infinite graph; we then construct a suitable well-quasi-order on the nodes of this graph, which ensures the termination of our search algorithm. We also show that the language inclusion problem is decidable if the only constant appearing among the clock constraints of A is zero. Moreover, these two cases are essentially the only decidable instances of language inclusion, in terms of restricting the various resources of timed automata.
booktitleProceedings of the 19th Annual IEEE Symposium on Logic in Computer Science (LICS)
shorttitleOn the Language Inclusion Problem for Timed Automata
titleOn the Language Inclusion Problem for Timed Automata: Closing a Decidability Gap
Algorithm design and analysis,Artificial intelligence,Automata,automata theory,clock constraints,Clocks,computational linguistics,Computational modeling,Computer science,Contracts,decidability,decidability gap,Government,infinite graph,language inclusion,Mathematics,reachability,reachability analysis,Real time systems,search algorithm,timed automata,well-quasiorder

abstractMetric temporal logic (MTL) is a prominent specification formalism for real-time systems. In this paper, we show that the satisfiability problem for MTL over finite timed words is decidable, with non-primitive recursive complexity. We also consider the model-checking problem for MTL: whether all words accepted by a given Alur-Dill timed automaton satisfy a given MTL formula. We show that this problem is decidable over finite words. Over infinite words, we show that model checking the safety fragment of MTL-which includes invariance and time-bounded response properties-is also decidable. These results are quite surprising in that they contradict various claims to the contrary that have appeared in the literature. The question of the decidability of MTL over infinite words remains open.
booktitle20th Annual IEEE Symposium on Logic in Computer Science (LICS)
titleOn the Decidability of Metric Temporal Logic
Abstracts,Alur-Dill timed automaton,Automata,Constraint theory,decidability,finite automata,Laboratories,Logic,Mathematics,metric temporal logic,model-checking problem,Real time systems,Safety,satisfiability problem,temporal logic,Timing,Turing machines

Berlin, Heidelberg

abstractMetric Temporal Logic (MTL) is a real-time extension of Linear Temporal Logic that was proposed fifteen years ago and has since been extensively studied. Since the early 1990s, it has been widely believed that some very small fragments of MTL are undecidable (i.e., have undecidable satisfiability and model-checking problems). We recently showed that, on the contrary, some substantial and important fragments of MTL are decidable [19,20]. However, until now the question of the decidability of full MTL over infinite timed words remained open.
booktitleFoundations of Software Science and Computation Structures
titleOn Metric Temporal Logic and Faulty Turing Machines
Global State,Linear Temporal Logic,Linear Temporal Logic Formula,Temporal Logic,Turing Machine

Berlin, Heidelberg

abstractMetric Temporal Logic (MTL) is a widely-studied real-time extension of Linear Temporal Logic. In this paper we consider a fragment of MTL, called Safety MTL, capable of expressing properties such as invariance and time-bounded response. Our main result is that the satisfiability problem for Safety MTL is decidable. This is the first positive decidability result for MTL over timed $\omega$-words that does not involve restricting the precision of the timing constraints, or the granularity of the semantics; the proof heavily uses the techniques of infinite-state verification. Combining this result with some of our previous work, we conclude that Safety MTL is fully decidable in that its satisfiability, model checking, and refinement problems are all decidable.
booktitleTools and Algorithms for the Construction and Analysis of Systems (TACAS)
titleSafety Metric Temporal Logic Is Fully Decidable
Clock Constraint,Extra Delay,Linear Temporal Logic,Model Check,Temporal Logic

abstractMetric Temporal Logic (MTL) is a prominent specification formalism for real-time systems. In this paper, we show that the satisfiability problem for MTL over finite timed words is decidable, with non-primitive recursive complexity. We also consider the model-checking problem for MTL: whether all words accepted by a given Alur-Dill timed automaton satisfy a given MTL formula. We show that this problem is decidable over finite words. Over infinite words, we show that model checking the safety fragment of MTL–which includes invariance and time-bounded response properties–is also decidable. These results are quite surprising in that they contradict various claims to the contrary that have appeared in the literature.
journaltitleLogical Methods in Computer Science
titleOn the Decidability and Complexity of Metric Temporal Logic over Finite Words

abstractMetric Temporal Logic (MTL) is a widely-studied real-time extension of Linear Temporal Logic. In this paper we survey results about the complexity of the satisfiability and model checking problems for fragments of MTL with respect to different semantic models.We show that these fragments have widely differing complexities: from polynomial space to non-primitive recursive and even undecidable. However we show that the most commonly occurring real-time properties, such as invariance and bounded response, can be expressed in fragments of MTL for which model checking, if not satisfiability, can be decided in polynomial or exponential space.
journaltitleFormal Modeling and Analysis of Timed Systems (FORMATS)
titleSome Recent Results in Metric Temporal Logic

abstractClassical planning has been notably successful in synthesizing finite plans to achieve states where propositional goals hold. In the last few years, classical planning has also been extended to incorporate temporally extended goals, expressed in temporal logics such as LTL, to impose restrictions on the state sequences generated by finite plans. In this work, we take the next step and consider the computation of infinite plans for achieving arbitrary LTL goals. We show that infinite plans can also be obtained efficiently by calling a classical planner once over a classical planning encoding that represents and extends the composition of the planning domain and the Buchi automaton representing the goal. This compilation scheme has been implemented and a number of experiments are reported.
booktitleTwenty-Second International Joint Conference on Artificial Intelligence (IJCAI)
titleComputing Infinite Plans for LTL Goals Using a Classical Planner

Berlin, Heidelberg

abstractWe compare the expressiveness of variants of Metric Temporal Logic (MTL) obtained by adding the past operators `S' and `SI'. We consider these variants under the “pointwise” and “continuous” interpretations over both finite and infinite models. Among other results, we show that for each of these variants the continuous version is strictly more expressive than the pointwise version. We also prove a counter-freeness result for MTL which helps to carry over some results from [3] for the case of infinite models to the case of finite models.
booktitleFormal Modeling and Analysis of Timed Systems
titleOn the Expressiveness of MTL with Past Operators
Past Operator,Periodic Sequence,Regular Language,Stability Point,Temporal Logic

journaltitleProceedings of the 1st International Conference on Principles of Knowledge Representation and Reasoning (KR)
titleADL: Exploring the Middle Ground between STRIPS and the Situation Calculus

Berlin, Heidelberg

abstractWe present Synthia, a new tool for the verification and synthesis of open real-time systems modeled as timed automata. The key novelty of Synthia is the underlying abstraction refinement approach [5] that combines the efficient symbolic treatment of timing information by difference bound matrices (DBMs) with the usage of binary decision diagrams (BDDs) for the discrete parts of the system description. Our experiments show that the analysis of both closed and open systems greatly benefits from identifying large relevant and irrelevant system parts on coarse abstractions early in the solution process. Synthia is licensed under the GNU GPL and available from our website.
booktitleComputer Aided Verification (CAV)
titleSynthia: Verification and Synthesis for Timed Automata
Abstract Game,Clock Zone,Initial Abstraction,Original Game,Time Automaton

University of Toronto

titleTemporal Reasoning in the Situation Calculus

abstractA unified approach to program verification is suggested, which applies to both sequential and parallel programs. The main proof method suggested is that of temporal reasoning in which the time dependence of events is the basic concept. Two formal systems are presented for providing a basis for temporal reasoning. One forms a formalization of the method of intermittent assertions, while the other is an adaptation of the tense logic system Kb, and is particularly suitable for reasoning about concurrent programs.
booktitleProceedings of the 18th Annual Symposium on Foundations of Computer Science (FOCS)
titleThe Temporal Logic of Programs

New York, NY

abstractWe consider the synthesis of a reactive module with input x and output y, which is specified by the linear temporal formula @@@@(x, y). We show that there exists a program satisfying @@@@ iff the branching time formula ($\forall$x) ($\exists$y) A@@@@(x, y) is valid over all tree models. For the restricted case that all variables range over finite domains, the validity problem is decidable, and we present an algorithm for constructing the program whenever it exists. The algorithm is based on a new procedure for checking the emptiness of Rabin automata on infinite trees in time exponential in the number of pairs, but only polynomial in the number of states. This leads to a synthesis algorithm whose complexity is double exponential in the length of the given specification.
booktitleProceedings of the 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL)
titleOn the Synthesis of a Reactive Module

Cambridge, MA

MIT Press

booktitleProceedings of the 10th International Conference on Logic Programming (ICLP)
titleTemporal Reasoning in Logic Programming : A Case for the Situation Calculus
1 introduction and motivation,calculus,event calculus,knowledge representation,situation,temporal reasoning

journaltitleAnnals of Mathematics and Artificial Intelligence
titleReasoning about Time in the Situation Calculus

journaltitleJournal of the ACM
titleSome Contributions to the Metatheory of the Situation Calculus

Berlin, Heidelberg

abstractThe aim of this paper is to illustrate by an example, the alternating bit protocol, the use of CESAR, an interactive system for aiding the design of distributed applications.
booktitleInternational Symposium on Programming
titleSpecification and Verification of Concurrent Systems in CESAR
Algorithmic Description,Execution Sequence,High Level Language,Propositional Variable,Temporal Logic

Boston, MA

abstractHybrid systems are digital real-time systems embedded in analog environments. A paradigmatic example of a hybrid system is a digital embedded control program for an analog plant environment, like a furnace or an airplane: the controller state moves discretely between control modes, and in each control mode, the plant state evolves continuously according to physical laws. Those systems combine discrete and continuous dynamics. Those aspects have been studied in computer science and in control theory. Computer scientists have introduced hybrid automata [28], a formal model that combines discrete control graphs, usually called finite state automata, with continuously evolving variables. A hybrid automaton exhibits two kinds of state changes: discrete jump transitions occur instantaneously, and continuous flow transitions occur when time elapses.
booktitleHandbook of Networked and Embedded Control Systems
titleAn Introduction to Hybrid Automata
Discrete Change,Hybrid Automaton,Hybrid System,Reachability Problem,Safety Property

Berlin, Heidelberg

abstractThe relationship between two well established formalisms for temporal reasoning is first investigated, namely between Allen's interval algebra (or Allen's temporal logic, abbreviated ATL) and linear temporal logic (LTL). A discrete variant of ATL is defined, called Allen linear temporal logic (ALTL), whose models are $\omega$-sequences of timepoints. It is shown that any ALTL formula can be linearly translated into an equivalent LTL formula, thus enabling the use of LTL techniques on ALTL requirements. This translation also implies the NP-completeness of ATL satisfiability. Then the problem of monitoring ALTL requirements is investigated, showing that it reduces to checking satisfiability; the similar problem for unrestricted LTL is known to require exponential space. An effective monitoring algorithm for ALTL is given, which has been implemented and experimented with in the context of planning applications.
booktitleComputer Aided Verification (CAV)
titleAllen Linear (Interval) Temporal Logic – Translation to LTL and Monitor Synthesis
Atomic Proposition,Linear Temporal Logic,State Machine,Temporal Logic,Temporal Reasoning

abstractWe consider a class of knowledge-based Golog programs with sense actions. These programs refer explicitly to an agent's knowledge, and are designed to execute on-line, and under a dynamic closed-world assumption on knowledge. On-line execution of sense actions dynamically updates the background axioms with sentences asserting knowledge of the sense actions' outcomes. We formalize what all this might mean, and show that under suitable assumptions the knowledge modality in such programs can be implemented by provability. This leads to an on-line Golog interpreter for such programs, which we demonstrate on a knowledge-based program with sensing for the blocks world.
journaltitleACM Transactions on Computational Logic
shortjournalACM Trans. Comput. Logic
titleOn Knowledge-Based Programming with Sensing in the Situation Calculus
dynamic closed-world assumption,sensing and knowledge,situation calculus,situation calculus programming languages,theorem-proving

MIT Press

titleKnowledge in Action: Logical Foundations for Specifying and Implementing Dynamical Systems

Academic Press

booktitleArtificial Intelligence and Mathematical Theory of Computation: Papers in Honor of John McCarthy
titleThe Frame Problem in the Situation Calculus: A Simple Solution (Sometimes) and a Completeness Result for Goal Regression

San Francisco, CA

Morgan Kaufmann Publishers Inc.

booktitleProceedings of the 5th International Conference on Principles of Knowledge Representation and Reasoning (KR)
titleNatural Actions, Concurrency and Continuous Time in the Situation Calculus

abstractFinite automata are considered in this paper as instruments for classifying finite tapes. Each one-tape automaton defines a set of tapes, a two-tape automaton defines a set of pairs of tapes, et cetera. The structure of the defined sets is studied. Various generalizations of the notion of an automaton are introduced and their relation to the classical automata is determined. Some decision problems concerning automata are shown to be solvable by effective algorithms; others turn out to be unsolvable by algorithms.
journaltitleIBM Journal of Research and Development
titleFinite Automata and Their Decision Problems

abstractComplex systems can be modelled at various levels of detail. Ideally, causal models of the same system should be consistent with one another in the sense that they agree in their predictions of the effects of interventions. We formalise this notion of consistency in the case of Structural Equation Models (SEMs) by introducing exact transformations between SEMs. This provides a general language to consider, for instance, the different levels of description in the following three scenarios: (a) models with large numbers of variables versus models in which the `irrelevant' or unobservable variables have been marginalised out; (b) micro-level models versus macro-level models in which the macro-variables are aggregate features of the micro-variables; (c) dynamical time series models versus models of their stationary behaviour. Our analysis stresses the importance of well specified interventions in the causal modelling process and sheds light on the interpretation of cyclic SEMs.
booktitleProceedings of the 33rd Annual Conference on Uncertainty in Artificial Intelligence (UAI)
titleCausal Consistency of Structural Equation Models
Computer Science - Artificial Intelligence,Computer Science - Machine Learning,Statistics - Machine Learning,Statistics - Methodology

journaltitleJournal of Artificial Intelligence Research
shorttitleThe LAMA Planner
titleThe LAMA Planner: Guiding Cost-Based Anytime Planning with Landmarks

Springer Netherlands

abstractThe frame problem originally surfaced within McCarthy's Situation Calculus [McCarthy68], when [McCarthy&Hayes69] applied it to reasoning about goal achievement. To illustrate their approach, they considered the problem of initiating a telephone conversation. They began by writing down plausible axioms which seemed to characterize the preconditions and effects of looking up a person's telephone number and dialling that number. However, they found that they were still unable to prove that the plan “look up the number and dial it” would work, even if all the initial conditions were right (i.e., that the caller had a telephone and a telephone book, that the intended party was home, etc.). For example, the axioms provided no assurance that looking up the number would not make the caller's telephone disappear, thus voiding a precondition for dialling.
booktitleKnowledge Representation and Defeasible Reasoning
titleMonotonic Solution of the Frame Problem in the Situation Calculus
Concurrent Action,Default Rule,Frame Problem,Plan Step,Primitive Action

Cambridge University Press

abstractAbstraction is a well-known approach to simplify a complex problem by over-approximating it with a deliberate loss of information. It was not considered so far in Answer Set Programming (ASP), a convenient tool for problem solving. We introduce a method to automatically abstract ASP programs that preserves their structure by reducing the vocabulary while ensuring an over-approximation (i.e., each original answer set maps to some abstract answer set). This allows for generating partial answer set candidates that can help with approximation of reasoning. Computing the abstract answer sets is intuitively easier due to a smaller search space, at the cost of encountering spurious answer sets. Faithful (non-spurious) abstractions may be used to represent projected answer sets and to guide solvers in answer set construction. For dealing with spurious answer sets, we employ an ASP debugging approach to help with abstraction refinement, which determines atoms as badly omitted and adds them back in the abstraction. As a show case, we apply abstraction to explain unsatisfiability of ASP programs in terms of blocker sets, which are the sets of atoms such that abstraction to them preserves unsatisfiability. Their usefulness is demonstrated by experimental results.
journaltitleTheory and Practice of Logic Programming
titleOmission-Based Abstraction for Answer Set Programs
abstraction,answer set programming,inconsistency explanation,knowledge representation and nonmonotonic reasoning

Berlin, Heidelberg

Springer Berlin Heidelberg

abstractThis article presents the event calculus, a logic-based formalism for representing actions and their effects. A circumscriptive solution to the frame problem is deployed which reduces to monotonic predicate completion. Using a number of benchmark examples from the literature, the formalism is shown to apply to a variety of domains, including those featuring actions with indirect effects, actions with non-deterministic effects, concurrent actions, and continuous change.
booktitleArtificial Intelligence Today: Recent Trends and Developments
titleThe Event Calculus Explained
Concurrent Action,Continuous Change,Effect Constraint,Frame Problem,State Constraint

abstractThis paper proposes a method for handling the frame problem for knowledge-producing actions. An example of a knowledge-producing action is a sensing operation performed by a robot to determine whether or not there is an object of a particular shape within its grasp. The work is an extension of Reiter's approach to the frame problem for ordinary actions and Moore's work on knowledge and action. The properties of our specification are that knowledge-producing actions do not affect fluents other than the knowledge fluent, and actions that are not knowledge-producing only affect the knowledge fluent as appropriate. In addition, memory emerges as a side-effect: if something is known in a certain situation, it remains known at successor situations, unless something relevant has changed. Also, it will be shown that a form of regression examined by Reiter for reducing reasoning about future situations to reasoning about the initial situation now also applies to knowledge-producing actions.
journaltitleArtificial Intelligence
shortjournalArtificial Intelligence
titleKnowledge, Action, and the Frame Problem
Action,Frame problem,Knowledge,Situation calculus

abstractThis paper proposes a solution to the frame problem for knowledgeproducing actions. An example of a knowledge-producing action is a sense operation performed by a robot to determine whether or not there is an object of a particular shape within its grasp. The work is an extension of Reiter's solution to the frame problem for ordinary actions and Moore's work on knowledge and action.
booktitleProceedings of the 11th National Conference on Artificial Intelligence (AAAI)
titleThe Frame Problem and Knowledge-Producing Actions

abstractWe propose a domain independent execution monitoring technique for a class of restartable logic-based temporal programs. The execution of a temporal program is interleaved with monitoring. Given a remaining part of a program, an execution trace, and the current time, if at this time no plan satisfying temporal constraints can be generated from the remaining program, the monitor backtracks (if possible) to a previous computation state of the restartable program where a new plan and an appropriate schedule can be constructed. We provide a declarative framework and its implementation on a mobile robot.
booktitleProceedings of the 16th International Joint Conference on Artificial Intelligence (IJCAI)
titleExecution Monitoring of High-Level Temporal Programs.

abstractThe need for combined task and motion planning in robotics is well understood. Solutions to this problem have typically relied on special purpose, integrated implementations of task planning and motion planning algorithms. We propose a new approach that uses off-the-shelf task planners and motion planners and makes no assumptions about their implementation. Doing so enables our approach to directly build on, and benefit from, the vast literature and latest advances in task planning and motion planning. It uses a novel representational abstraction and requires only that failures in computing a motion plan for a high-level action be identifiable and expressible in the form of logical predicates at the task level. We evaluate the approach and illustrate its robustness through a number of experiments using a state-of-the-art robotics simulator and a PR2 robot. These experiments show the system accomplishing a diverse set of challenging tasks such as taking advantage of a tray when laying out a table for dinner and picking objects from cluttered environments where other objects need to be re-arranged before the target object can be reached.
booktitle2014 IEEE International Conference on Robotics and Automation (ICRA)
titleCombined Task and Motion Planning through an Extensible Planner-Independent Interface Layer
cluttered environments,extensible planner-independent interface layer,Generators,Grasping,Grippers,Indexes,motion planners,motion planning algorithms,off-the-shelf task planners,path planning,picking objects,Planning,PR2 robot,robotics simulator,Robots,task planning,Trajectory,tray

abstractThis article describes REBA, a knowledge representation and reasoning architecture for robots that is based on tightly-coupled transition diagrams of the domain at two different levels of granularity. An action language is extended to support non-boolean fluents and non-deterministic causal laws, and used to describe the domain's transition diagrams, with the fine-resolution transition diagram being defined as a refinement of the coarse-resolution transition diagram. The coarse-resolution system description, and a history that includes prioritized defaults, are translated into an Answer Set Prolog (ASP) program. For any given goal, inference in the ASP program provides a plan of abstract actions. To implement each such abstract action, the robot automatically zooms to the part of the fine-resolution transition diagram relevant to this action. The zoomed fine-resolution system description, and a probabilistic representation of the uncertainty in sensing and actuation, are used to construct a partially observable Markov decision process (POMDP). The policy obtained by solving the POMDP is invoked repeatedly to implement the abstract action as a sequence of concrete actions. The fine-resolution outcomes of executing these concrete actions are used to infer coarse-resolution outcomes that are added to the coarse-resolution history and used for subsequent coarse-resolution reasoning. The architecture thus combines the complementary strengths of declarative programming and probabilistic graphical models to represent and reason with non-monotonic logic-based and probabilistic descriptions of uncertainty and incomplete domain knowledge. In addition, we describe a general methodology for the design of software components of a robot based on these knowledge representation and reasoning tools, and provide a path for proving the correctness of these components. The architecture is evaluated in simulation and on a mobile robot finding and moving target objects to desired locations in indoor domains, to show that the architecture supports reliable and efficient reasoning with violation of defaults, noisy observations and unreliable actions, in complex domains.
journaltitleJournal of Artificial Intelligence Research
titleREBA: A Refinement-Based Architecture for Knowledge Representation and Reasoning in Robotics
Knowledge representation,logic programming,probabilistic reasoning,Qualitative reasoning,Reasoning about actions and change,Robotics

booktitleProceedings of the 7th IARP Workshop on Technical Challenges for Dependable Robots
titleSelf-Maintenance for Autonomous Robots Controlled by ReadyLog

abstractReasoning and planning for mobile robots is a challenging problem, as the world evolves over time and thus the robot's goals may change. One technique to tackle this problem is goal reasoning, where the agent not only reasons about its actions, but also about which goals to pursue. While goal reasoning for single agents has been researched extensively, distributed, multi-agent goal reasoning comes with additional challenges, especially in a distributed setting. In such a context, some form of coordination is necessary to allow for cooperative behavior. Previous goal reasoning approaches share the agent's world model with the other agents, which already enables basic cooperation. However, the agent's goals, and thus its intentions, are typically not shared. In this paper, we present a method to tackle this limitation. Extending an existing goal reasoning framework, we propose enabling cooperative behavior between multiple agents through promises, where an agent may promise that certain facts will be true at some point in the future. Sharing these promises allows other agents to not only consider the current state of the world, but also the intentions of other agents when deciding on which goal to pursue next. We describe how promises can be incorporated into the goal life cycle, a commonly used goal refinement mechanism. We then show how promises can be used when planning for a particular goal by connecting them to timed initial literals (TILs) from PDDL planning. Finally, we evaluate our prototypical implementation in a simplified logistics scenario.
booktitleICAPS Workshop on Planning and Robotics (PlanRob)
titleTowards Using Promises for Multi-Agent Cooperation in Goal Reasoning

New York, NY

abstractOne of the field in which models of abstraction have been proposed is Artificial Intelligence (AI). This chapter has two parts: one presents an overview of the formal models, either syntactic or semantic, mostly based on logical approaches, whereas the other one describes the use of abstraction in AI, starting from ABSTRIP, and spanning planning, knowledge representation, Constraint Satisfaction Problems, and Multi-Agent Systems.
booktitleAbstraction in Artificial Intelligence and Complex Systems
titleAbstraction in Artificial Intelligence
Abstract Space,Constraint Satisfaction Problem,Predicate Abstraction,Soft Constraint,Temporal Abstraction

SAGE Publications Ltd STM

abstractAutonomous service robots will have to understand vaguely described tasks, such as ?set the table? or ?clean up?. Performing such tasks as intended requires robots to fully, precisely, and appropriately parameterize their low-level control programs. We propose knowledge processing as a computational resource for enabling robots to bridge the gap between vague task descriptions and the detailed information needed to actually perform those tasks in the intended way. In this article, we introduce the KnowRobknowledge processing system that is specifically designed to provide autonomous robots with the knowledge needed for performing everyday manipulation tasks. The system allows the realization of ?virtual knowledge bases?: collections of knowledge pieces that are not explicitly represented but computed on demand from the robot?s internal data structures, its perception system, or external sources of information. This article gives an overview of the different kinds of knowledge, the different inference mechanisms, and interfaces for acquiring knowledge from external sources, such as the robot?s perception system, observations of human activities, Web sites on the Internet, as well as Web-based knowledge bases for information exchange between robots. We evaluate the system?s scalability and present different integrated experiments that show its versatility and comprehensiveness.
journaltitleThe International Journal of Robotics Research
titleKnowRob: A Knowledge Processing Infrastructure for Cognition-Enabled Robots

Cambridge, MA

MIT Press

abstractProbablistic robotics is a growing area in the subject, concerned with perception and control in the face of uncertainty and giving robots a level of robustness in real-world situations. This book introduces techniques and algorithms in the field.
titleProbabilistic Robotics
SLAM localisation mapping robot topoi

Cambridge University Press

abstractFLUX is a programming method for the design of agents that reason logically about their actions and sensor information in the presence of incomplete knowledge. The core of FLUX is a system of Constraint Handling Rules, which enables agents to maintain an internal model of their environment by which they control their own behavior. The general action representation formalism of the fluent calculus provides the formal semantics for the constraint solver. FLUX exhibits excellent computational behavior due to both a carefully restricted expressiveness and the inference paradigm of progression.
journaltitleTheory and Practice of Logic Programming
titleFLUX: A Logic Programming Method for Reasoning Agents
agents,artificial intelligence,cognitive robotics

journaltitleLinköping Electronic Articles in Computer and Information Science
titleIntroduction to the Fluent Calculus

abstractSuccessor state axioms provide a solution to the famous Frame Problem as far as the representational aspect is concerned. Solving in classical, monotonic logic the additional inferential Frame Problem, on the other hand, was the major motivation for the development of the Fluent Calculus a decade or so ago. Yet the expressiveness of the latter in comparison to the Situation Calculus remained a largely open question until today. In this note, we derive a novel version of the Fluent Calculus by gradually applying the principle of reification to successor state axioms in order to address the inferential Frame Problem without losing the representational merits. Our approach results in a fully mechanic method for the generation of state update axioms from any collection of Situation Calculus-style effect axioms for deterministic actions, provided the actions do not have potentially infinitely many effects. The axiomatization thus obtained is proved essentially equivalent to the corresponding axiomatization which uses successor state axioms.
journaltitleArtificial Intelligence
shortjournalArtificial Intelligence
shorttitleFrom Situation Calculus to Fluent Calculus
titleFrom Situation Calculus to Fluent Calculus: State Update Axioms as a Solution to the Inferential Frame Problem
Cognitive robotics,Frame problem

Berlin, Heidelberg

abstractThe discussion of the relative merits of linear-versus branching-time frameworks goes back to early 1980s. One of the beliefs dominating this discussion has been that “while specifying is easier in LTL (linear-temporal logic), verification is easier for CTL (branching-temporal logic)”. Indeed, the restricted syntax of CTL limits its expressive power and many important behaviors (e.g., strong fairness) can not be specified in CTL. On the other hand, while model checking for CTL can be done in time that is linear in the size of the specification, it takes time that is exponential in the specification for LTL. Because of these arguments, and for historical reasons, the dominant temporal specification language in industrial use is CTL.In this paper we argue that in spite of the phenomenal success of CTL-based model checking, CTL suffers from several fundamental limitations as a specification language, all stemming from the fact that CTL is a branching-time formalism: the language is unintuitive and hard to use, it does not lend itself to compositional reasoning, and it is fundamentally incompatible with semi-formal verification. These inherent limitations severely impede the functionality of CTL-based model checkers. In contrast, the linear-time framework is expressive and intuitive, supports compositional reasoning and semi-formal verification, and is amenable to combining enumerative and symbolic search methods. While we argue in favor of the linear-time framework, we also we argue that LTL is not expressive enough, and discusswhat would be the “ultimate” temporal specification language.
booktitleTools and Algorithms for the Construction and Analysis of Systems (TACAS)
shorttitleBranching vs. Linear Time
titleBranching vs. Linear Time: Final Showdown
Atomic Proposition,Linear Temporal Logic,Model Check,Symbolic Model Check,Temporal Logic

abstractSpace mission operations require flexible, efficient and reliable plan execution. In typical operations command sequences (which are a simple subset of general executable plans) are generated on the ground, either manually or with assistance from automated planning, and sent to the spacecraft. For more advanced operations more expressive executable plans may be used; the plans might also be generated automatically on board the spacecraft. In all these cases, the executable plans are received by a software system that executes the plan. This software system, often called an executive, must ensure that the execution of the commands and response of the fault protection system conforms to pre-planned behaviour. This paper presents a language, called PLEXIL, that is designed specifically for flexible and reliable command execution. It is designed to be portable, lightweight, predictable, and verifiable, and at the same time it is more expressive than command sequencing languages currently used on space missions.
booktitleProceedings of the 8th International Symposium on Artificial Intelligence, Robotics and Automation in Space (iSAIRAS)
titlePlan Execution Interchange Language (Plexil) for Executable Plans and Command Sequences

booktitleProceedings of the 30th International Joint Conference on Artificial Intelligence (IJCAI)
titleTransforming Robotic Plans with Timed Automata to Solve Temporal Platform Constraints

booktitleProceedings of the 20th European Conference on Artificial Intelligence (ECAI)
titleProgression of Situation Calculus Action Theories with Incomplete Information
cognitive robotics,reasoning about actions and change

Morgan Kaufmann

abstractIn the synthesis of a plan or computer program, the problem of achieving several goals simultaneously presents special difficulties, since a plan to achieve one goal may interfere with attaining the others. This paper develops the following strategy: to achieve two goals simultaneously, develop a plan to achieve one of them and then modify that plan to achieve the second as well. A systematic program modification technique is presented to support this strategy. The technique requires the introduction of a special “skeleton model” to represent a changing world that can accommodate modifications in the plan. This skeleton model also provides a novel approach to the “frame problem.” The strategy is illustrated by its application to three examples. Two examples involve synthesizing the following programs: interchanging the values of two variables and sorting three variables. The third entails formulating tricky blocks-world plans. The strategy has been implemented in a simple QLISP program. It is argued that skeleton modelling is valuable as a planning technique apart from its use in plan modification, particularly because it facilitates the representation of “influential actions” whose effects may be far reaching. The second part of the paper is a critical survey of contemporary planning literature, which compares our approach with other techniques for facing the same problems. The following is the outline of contents.
booktitleReadings in Artificial Intelligence
titleAchieving Several Goals Simultaneously

Loch Awe, Scotland

booktitleProceedings of the International Workshop on Principles of Diagnosis (DX)
titleUnifying Model-Based and Reactive Programming within a Model-Based Executive
diagnosis,model-based reasoning,reactive systems

abstractProgramming complex embedded systems involves reasoning through intricate system interactions along lengthy paths between sensors, actuators, and control processors. This is a challenging, time-consuming, and error-prone process requiring significant interaction between engineers and software programmers. Furthermore, the resulting code generally lacks modularity and robustness in the presence of failure. Model-based programming addresses these limitations, allowing engineers to program reactive systems by specifying high-level control strategies and by assembling commonsense models of the system hardware and software. In executing a control strategy, model-based executives reason about the models "on the fly," to track system state, diagnose faults, and perform reconfigurations. This paper develops the reactive model-based programming language (RMPL) and its executive, called Titan. RMPL provides the features of synchronous, reactive languages, with the added ability of reading and writing to state variables that are hidden within the physical plant being controlled. Titan executes an RMPL program using extensive component-based declarative models of the plant to track states, analyze anomalous situations, and generate novel control sequences. Within its reactive control loop, Titan employs propositional inference to deduce the system's current and desired states, and it employs model-based reactive planning to move the plant from the current to the desired state.
journaltitleProceedings of the IEEE
titleModel-Based Programming of Intelligent Embedded Systems and Robotic Space Explorers
Embedded system,Intelligent actuators,Intelligent robots,Intelligent sensors,Intelligent systems,Orbital robotics,Robot programming,Robot sensing systems,Sensor systems,Space exploration

San Francisco, CA, USA

Morgan Kaufmann Publishers Inc.

abstractA new generation of reactive, model-based executives are emerging that make extensive use of componentbased declarative models to analyze anomalous situations and generate novel sequences for the internal control of complex autonomous systems. Burton, a generative, model-based planner offers a core element that bridges the gap between current and target states within the reactive loop. Burton is a sound, complete, reactive planner that generates a single control action of a valid plan in average case constant time, and compensates for anomalies at every step. Burton will not generate irreversible, potentially damaging sequences, except to effect repairs. We present model compilation, causal analysis, and online policy construction methods that are key to Burton's performance.
booktitleProceedings of the 15th International Joint Conference on Artifical Intelligence
titleA Reactive Planner for a Model-Based Executive

AAAI Press

abstractThe high-level action programming language Golog is a useful means for modeling the behavior of autonomous agents such as mobile robots. It relies on a representation given in terms of a logic-based action theory in the Situation Calculus (SC). To guarantee that the possibly non-terminating execution of a Golog program leads to the desired behavior of the agent, it is desirable to (automatically) verify that it satisfies certain requirements given in terms of temporal formulas. However, due to the high (first-order) expressiveness of the Golog language, the verification problem is in general undecidable. In this paper we show that for a fragment of the Golog language defined on top of the decidable logic C, the verification problem for linear time temporal properties becomes decidable, which extends earlier results to a more expressive fragment of the input formalism. Moreover, we justify the involved restrictions on program constructs and action theory by showing that relaxing any of these restrictions instantly renders the verification problem undecidable again.
booktitleProceedings of the AAAI 2014 Spring Symposium: Knowledge Representation and Reasoning in Robotics (KRR)
titleOn the Decidability of Verifying LTL Properties of Golog Programs

IOS Press

abstractGolog is a high-level action programming language for controlling autonomous agents such as mobile robots. It is defined on top of a logic-based action theory expressed in the Situation Calculus. Before a program is deployed onto an actual robot and executed in the physical world, it is desirable, if not crucial, to verify that it meets certain requirements (typically expressed through temporal formulas) and thus indeed exhibits the desired behaviour. However, due to the high (first-order) expressiveness of the language, the corresponding verification problem is in general undecidable. In this paper, we extend earlier results to identify a large, non-trivial fragment of the formalism where verification is decidable. In particular, we consider properties expressed in a first-order variant of the branching-time temporal logic CTL*. Decidability is obtained by (1) resorting to the decidable first-order fragment C as underlying base logic, (2) using a fragment of Golog with ground actions only, and (3) requiring the action theory to only admit local effects.
booktitleProceedings of the Twenty-First European Conference on Artificial Intelligence (ECAI 2014)
titleVerifying CTL* Properties of Golog Programs over Local-Effect Actions

AAAI Press

abstractThe Golog action programming language is a powerful means to express high-level behaviours in terms of programs over actions defined in a Situation Calculus theory. In particular for physical systems, verifying that the program satisfies certain desired temporal properties is often crucial, but undecidable in general, the latter being due to the languages high expressiveness in terms of first-order quantification, range of action effects, and program constructs. So far, approaches to achieve decidability involved restrictions where action effects either had to be context-free (i.e. not depend on the current state), local (i.e. only affect objects mentioned in the actions parameters), or at least bounded (i.e. only affect a finite number of objects). In this paper, we introduce two new, more general classes of action theories that allow for context-sensitive, non-local, unbounded effects, i.e. actions that may affect an unbounded number of possibly unnamed objects in a state-dependent fashion. We contribute to the further exploration of the boundary between decidability and undecidability for Golog, showing that for our new classes of action theories in the two-variable fragment of first-order logic, verification of CTL* properties of programs over ground actions is decidable.
booktitleProceedings of the 30th AAAI Conference on Artificial Intelligence (AAAI)
titleDecidable Verification of Golog Programs over Non-Local Effect Actions

[category=contributions,type=unpublished,heading=subbibliography,title=Poster Presentations]

Missing 'biblatex' package
The bibliography requires the 'biblatex' package.

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

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.
journaltitleAnnals of Mathematics and Artificial Intelligence
relatedstringReprint of
shortjournalAnn Math Artif Intell
titleNon-Terminating Processes in the Situation Calculus
68T27,Formal verification of GOLOG and CONGOLOG programs,Inductive definitions,Knowledge representation,Reasoning about actions,Situation calculus

journaltitleMachine Intelligence
relatedstringReprinted as
titleSome Philosophical Problems from the Standpoint of Artificial Intelligence

Morgan Kaufmann

abstractA computer program capable of acting intelligently in the world must have a general representation of the world in terms of which its inputs are interpreted. Designing such a program requires commitments about what knowledge is and how it is obtained. Thus, some of the major traditional problems of philosophy arise in artificial intelligence. More specifically, we want a computer program that decides what to do by inferring in a formal language that a certain strategy will achieve its assigned goal. This requires formalizing concepts of causality, ability, and knowledge. Such formalisms are also considered in philosophical logic. The first part of the paper begins with a philosophical point of view that seems to arise naturally once we take seriously the idea of actually making an intelligent machine. We go on to the notions of metaphysically and epistemo-logically adequate representations of the world and then to an explanation of can, causes, and knows in terms of a representation of the world by a system of interacting automata. A proposed resolution of the problem of freewill in a deterministic universe and of counterfactual conditional sentences is presented. The second part is mainly concerned with formalisms within which it can be proved that a strategy will achieve a goal. Concepts of situation, fluent, future operator, action, strategy, result of a strategy and knowledge are formalized. A method is given of constructing a sentence of first-order logic which will be true in all models of certain axioms if and only if a certain strategy will achieve a certain goal. The formalism of this paper represents an advance over McCarthy (1963) and Green (1969) in that it permits proof of the correctness of strategies that contain loops and strategies that involve the acquisition of knowledge; and it is also somewhat more concise. The third part discusses open problems in extending the formalism of part 2. The fourth part is a review of work in philosophical logic in relation to problems of artificial intelligence and a discussion of previous efforts to program `general intelligence' from the point of view of this paper.
booktitleReadings in Artificial Intelligence
titleSome Philosophical Problems from the Standpoint of Artificial Intelligence

abstractOver the past few years increasing research effort has been directed towards the automatic verification of infinite-state systems. This paper is concerned with identifying general mathematical structures which can serve as sufficient conditions for achieving decidability. We present decidability results for a class of systems (called well-structured systems) which consist of a finite control part operating on an infinite data domain. The results assume that the data domain is equipped with a preorder which is a well quasi-ordering, such that the transition relation is “monotonic” (a simulation) with respect to the preorder. We show that the following properties are decidable for well-structured systems: •Reachability: whether a certain set of control states is reachable. Other safety properties can be reduced to the reachability problem. •Eventuality: whether all executions eventually reach a given set of control states (represented as AFp in CTL). •Simulation: whether there exists a simulation between a finite automaton and a well-structured system. The simulation problem will be shown to be decidable in both directions. We also describe how these general principles subsume several decidability results from the literature about timed automata, relational automata, Petri nets, and lossy channel systems.
journaltitleInformation and Computation
shortjournalInformation and Computation
titleAlgorithmic Analysis of Programs with Well Quasi-ordered Domains

abstractOver the last few years there has been an increasing research effort directed towards the automatic verification of infinite state systems. This paper is concerned with identifying general mathematical structures which can serve as sufficient conditions for achieving decidability. We present decidability results for a class of systems (called well-structured systems), which consist of a finite control part operating on an infinite data domain. The results assume that the data domain is equipped with a well-ordered and well-founded preorder such that the transition relation is "monotonic" (is a simulation) with respect to the preorder. We show that the following properties are decidable for well-structured systems: reachability; eventuality; and simulation. We also describe how these general principles subsume several decidability results from the literature about timed automata, relational automata, Petri nets, and lossy channel systems.
booktitleProceedings of the 11th Annual IEEE Symposium on Logic in Computer Science (LICS)
titleGeneral Decidability Theorems for Infinite-State Systems
Automata,Automatic control,Computer science,Control systems,Councils,Information management,Mathematics,Petri nets,Safety,State-space methods

Cambridge University Press

abstractIn this paper, we give a step by step introduction to the theory of well quasi-ordered transition systems. The framework combines two concepts, namely (i) transition systems which are monotonic wrt. a well-quasi ordering; and (ii) a scheme for symbolic backward reachability analysis. We describe several models with infinite-state spaces, which can be analyzed within the framework, e.g., Petri nets, lossy channel systems, timed automata, timed Petri nets, and multiset rewriting systems. We will also present better quasi-ordered transition systems which allow the design of efficient symbolic representations of infinite sets of states.
journaltitleBulletin of Symbolic Logic
titleWell (and Better) Quasi-Ordered Transition Systems

Berlin, Heidelberg

abstractIn an earlier work [AČJYK00] we presented a general framework for verification of infinite-state transition systems, where the transition relation is monotonic with respect to a well quasi-ordering on the set of states. In this paper, we investigate extending the framework from the context of transition systems to that of games. We show that monotonic games are in general undecidable. We identify a subclass of monotonic games, called downward closed games. We provide algorithms for analyzing downward closed games subject to winning conditions which are formulated as safety properties.
booktitleComputer Science Logic
titleDeciding Monotonic Games
Broadcast Protocol,Cache Coherence,Model Check,Safety Problem,Transition System

howpublishedLecture Notes
titleModeling and Analysis of Hybrid Systems

abstractThis research extends CTL model-checking to the analysis of real-time systems, whose correctness depends on the magnitudes of the timing delays. For specifications, the syntax of CTL is extended to allow quantitative temporal operators. The formulas of the resulting logic, TCTL, are interpretation over continuous computation trees, trees in which paths are maps from the set of nonnegative reals to system states. To model finite-state systems the notion of timed graphs is introduced-state-transition graphs extended with a mechanism that allows the expression of constant bounds on the delays between the state transition. As the main result, an algorithm is developed for model checking, that is, for determining the truth of a TCTL formula with respect to a timed graph. It is argued that choosing a dense domain, instead of a discrete domain, to model time does not blow up the complexity of the model-checking problem. On the negative side, it is shown that the denseness of the underlying time domain makes TCTL II/sub 1//sup 1/-hard. The question of deciding whether a given TCTL formula is implementable by a timed graph is also undecidable.$<>$
booktitleProceedings of the 5th Annual IEEE Symposium on Logic in Computer Science (LICS)
titleModel-Checking for Real-Time Systems
Computer bugs,Computer science,Contracts,Control systems,Delay,Digital systems,Logic,Real time systems,Timing,Tree graphs

abstractWe propose timed (finite) automata to model the behavior of real-time systems over time. Our definition provides a simple, and yet powerful, way to annotate state-transition graphs with timing constraints using finitely many real-valued clocks. A timed automaton accepts timed words–infinite sequences in which a real-valued time of occurrence is associated with each symbol. We study timed automata from the perspective of formal language theory: we consider closure properties, decision problems, and subclasses. We consider both nondeterministic and deterministic transition structures, and both Büchi and Muller acceptance conditions. We show that nondeterministic timed automata are closed under union and intersection, but not under complementation, whereas deterministic timed Muller automata are closed under all Boolean operations. The main construction of the paper is an (PSPACE) algorithm for checking the emptiness of the language of a (nondeterministic) timed automaton. We also prove that the universality problem and the language inclusion problem are solvable only for the deterministic automata: both problems are undecidable ($\Pi$11-hard) in the nondeterministic case and PSPACE-complete in the deterministic case. Finally, we discuss the application of this theory to automatic verification of real-time requirements of finite-state systems.
journaltitleTheoretical Computer Science
shortjournalTheoretical Computer Science
titleA Theory of Timed Automata

booktitleProceedings of the 30th International Joint Conference on Artificial Intelligence (IJCAI)
shorttitleBest-Effort Synthesis
titleBest-Effort Synthesis: Doing Your Best Is Not Harder Than Giving Up

journaltitleJournal of the ACM
titleThe Benefits of Relaxing Punctuality

abstractWe introduce event-recording automata. An event-recording automaton is a timed automaton that contains, for every event a, a clock that records the time of the last occurrence of a. The class of event-recording automata is, on one hand, expressive enough to model (finite) timed transition systems and, on the other hand, determinizable and closed under all boolean operations. As a result, the language-inclusion problem is decidable for event-recording automata. We present a translation from timed transition systems to event-recording automata, which leads to an algorithm for checking if two timed transition systems have the same set of timed behaviors. We also consider event-predicting automata, which contain clocks that predict the time of the next occurrence of an event. The class of event-clock automata, which contain both event-recording and event-predicting clocks, is a suitable specification language for real-time properties. We provide an algorithm for checking if a timed automaton meets a specification that is given as an event-clock automaton.
journaltitleTheoretical Computer Science
shortjournalTheoretical Computer Science
shorttitleEvent-Clock Automata
titleEvent-Clock Automata: A Determinizable Class of Timed Automata
Automata theory,Formal verification,Real-time systems,Timed automata

Berlin, Heidelberg

abstractWe survey logic-based and automata-based languages and techniques for the specification and verification of real-time systems. In particular, we discuss three syntactic extensions of temporal logic: time-bounded operators, freeze quantification, and time variables. We also discuss the extension of finite-state machines with clocks and the extension of transition systems with time bounds on the transitions. All of the resulting notations can be interpreted over a variety of different models of time and computation, including linear and branching time, interleaving and true concurrency, discrete and continuous time. For each choice of syntax and semantics, we summarize the results that are known about expressive power, algorithmic finite-state verification, and deductive verification.
booktitleReal-Time: Theory in Practice
shorttitleLogics and Models of Real Time
titleLogics and Models of Real Time: A Survey
finite-state machines,real time,semantics,Temporal logic,transition systems,verification

abstractModels of the dynamics of cellular interaction networks have become increasingly larger in recent years. Formal verification based on model checking provides a powerful technology to keep up with this increase in scale and complexity. The application of modelchecking approaches is hampered, however, by the difficulty for nonexpert users to formulate appropriate questions in temporal logic.
journaltitleJournal of the ACM
titleA Really Temporal Logic

abstractPresents a model-checking procedure and its implementation for the automatic verification of embedded systems. The system components are described as hybrid automata-communicating machines with finite control and real-valued variables that represent continuous environment parameters such as time, pressure and temperature. The system requirements are specified in a temporal logic with stop-watches, and verified by symbolic fixpoint computation. The verification procedure-implemented in the Cornell Hybrid Technology tool, HyTech-applies to hybrid automata whose continuous dynamics is governed by linear constraints on the variables and their derivatives. We illustrate the method and the tool by checking safety, liveness, time-bounded and duration requirements of digital controllers, schedulers and distributed algorithms.
journaltitleIEEE Transactions on Software Engineering
titleAutomatic Symbolic Verification of Embedded Systems
Automata,Automatic control,Control systems,Digital control,Distributed control,Embedded system,Logic,Pressure control,Safety,Temperature control

Berlin, Heidelberg

abstractWe consider a housekeeping domain with multiple cleaning robots and represent it in the action language +C+\mathcal {C}+. With such a formalization of the domain, a plan can be computed using the causal reasoner CCalc for each robot to tidy some part of the house. However, to find a plan that characterizes a feasible trajectory that does not collide with obstacles, we need to consider geometric reasoning as well. For that, we embed motion planning in the domain description using external predicates. For safe execution of feasible plans, we introduce a planning and monitoring algorithm so that the robots can recover from plan execution failures due to heavy objects that cannot be lifted alone. The coordination of robots to help each other is considered for such a recovery. We illustrate the applicability of this algorithm with a simulation of a housekeeping domain.
booktitleLogic Programming and Nonmonotonic Reasoning
titleCausal Reasoning for Planning and Coordination of Multiple Housekeeping Robots
Causal Reasoning,Geometric Reasoning,Goal Position,Heavy Object,Living Room

journaltitleCommunications of the ACM
titleMaintaining Knowledge about Temporal Intervals

abstractA formalism for reasoning about actions is proposed that is based on a temporal logic. It allows a much wider range of actions to be described than with previous approaches such as the situation calculus. This formalism is then used to characterize the different types of events, processes, actions, and properties that can be described in simple English sentences. In addressing this problem, we consider actions that involve non-activity as well as actions that can only be defined in terms of the beliefs and intentions of the actors. Finally, a framework for planning in a dynamic world with external events and multiple agents is suggested.
journaltitleArtificial Intelligence
shortjournalArtificial Intelligence
titleTowards a General Theory of Action and Time

Berlin, Heidelberg

abstractWe introduce the framework of hybrid automata as a model and specification language for hybrid systems. Hybrid automata can be viewed as a generalization of timed automata, in which the behavior of variables is governed in each state by a set of differential equations. We show that many of the examples considered in the workshop can be defined by hybrid automata. While the reachability problem is undecidable even for very restricted classes of hybrid automata, we present two semidecision procedures for verifying safety properties of piecewiselinear hybrid automata, in which all variables change at constant rates. The two procedures are based, respectively, on minimizing and computing fixpoints on generally infinite state spaces. We show that if the procedures terminate, then they give correct answers. We then demonstrate that for many of the typical workshop examples, the procedures do terminate and thus provide an automatic way for verifying their properties.
booktitleHybrid Systems
shorttitleHybrid Automata
titleHybrid Automata: An Algorithmic Approach to the Specification and Verification of Hybrid Systems
Acceptance Condition,Hybrid Automaton,Hybrid System,Mutual Exclusion,Reachability Problem

Berlin, Heidelberg

abstractModel checking is emerging as a practical tool for automated debugging of complex reactive systems such as embedded controllers and network protocols (see [23] for a survey). Traditional techniques for model checking do not admit an explicit modeling of time, and are thus, unsuitable for analysis of real-time systems whose correctness depends on relative magnitudes of different delays. Consequently, timed automata [7] were introduced as a formal notation to model the behavior of real-time systems. Its definition provides a simple way to annotate state-transition graphs with timing constraints using finitely many real-valued clock variables. Automated analysis of timed automata relies on the construction of a finite quotient of the infinite space of clock valuations. Over the years, the formalism has been extensively studied leading to many results establishing connections to circuits and logic, and much progress has been made in developing verification algorithms, heuristics, and tools. This paper provides a survey of the theory of timed automata, and their role in specification and verification of real-time systems.
booktitleComputer Aided Verification (CAV)
titleTimed Automata

Berlin, Heidelberg

booktitleAutomata, Languages and Programming
titleRealizable and Unrealizable Specifications of Reactive Systems
Finite Automaton,Parallel Composition,Safety Property,Transition System,Winning Strategy

Berlin, Heidelberg

abstractFinite automata and regular languages have been useful in a wide variety of problems in computing, communication and control, including formal modeling and verification. Traditional automata do not admit an explicit modeling of time, and consequently, timed automata [2] were introduced as a formal notation to model the behavior of real-time systems. Timed automata accept timed languages consisting of sequences of events tagged with their occurrence times. Over the years, the formalism has been extensively studied leading to many results establishing connections to circuits and logic, and much progress has been made in developing verification algorithms, heuristics, and tools. This paper provides a survey of the theoretical results concerning decision problems of reachability, language inclusion and language equivalence for timed automata and its variants, with some new proofs and comparisons. We conclude with a discussion of some open problems.
booktitleFormal Methods for the Design of Real-Time Systems
shorttitleDecision Problems for Timed Automata
titleDecision Problems for Timed Automata: A Survey
Clock Constraint,Hybrid Automaton,Reachability Problem,Regular Language,Time Automaton

abstractMany existing algorithms for model checking of infinite-state systems operate on constraints which are used to represent (potentially infinite) sets of states. A general powerful technique which can be employed for proving termination of these algorithms is that of well quasi-orderings. Several methodologies have been proposed for derivation of new well quasi-ordered constraint systems. However, many of these constraint systems suffer from a "constraint explosion problem", as the number of the generated constraints grows exponentially with the size of the problem. We demonstrate that a refinement of the theory of well quasi-orderings, called the theory of better quasi-orderings is more appropriate for symbolic model checking, since it allows inventing constraint systems which are both well quasi-ordered and compact. We apply our methodology to derive new constraint systems for verification of systems with unboundedly many clocks, broadcast protocols, lossy channel systems, and integral relational automata. The new constraint systems are exponentially more succinct than existing ones, and their well quasi-ordering cannot be shown by previous methods in the literature.
booktitleProceedings of the 15th Annual IEEE Symposium on Logic in Computer Science (LICS)
shorttitleBetter Is Better than Well
titleBetter Is Better than Well: On Efficient Verification of Infinite-State Systems
algorithm termination,Automata,automata theory,better quasi-orderings,broadcast protocols,Broadcasting,clocks,Clocks,constraint explosion problem,constraint handling,Constraint theory,Explosions,infinite-state systems verification,integral relational automata,lossy channel systems,model checking,Petri nets,Power system modeling,program verification,Protocols,symbolic model checking,temporal logic,Termination of employment,timed Petri nets,well quasi-ordered constraint systems

abstractVerification is the problem of checking whether the behavior of a closed system satisfies a given property. The system is closed in the sense that its behavior is fully specified. Synthesis is the problem of finding a way to “close” an open system, so that the behavior of the closed system satisfies a given property. The system is open in the sense that its behavior is under-specified: it can be modified (restricted) during the synthesis process. Closing a system usually means coupling it with a controller which observes the behavior of the system so far and restricts it by disabling or forcing some actions. The controller is state-feedback when its decisions depend solely on the current state of the system. In this paper, we present two tools for (state-feedback) controller synthesis of timed systems. Our model is based on timed automata [4] with discrete actions annotated as controllable or uncontrollable. Controllable actions can be restricted, while uncontrollable cannot. Following the approaches of [23, 7, 3] we associate urgency with actions rather than states. We are interested in controllers ensuring two types of properties, namely, invariance or inevitability. Invariance means that all behaviors of the closed system remain within a given set of states. Inevitability means that all behaviors of the closed system reach a given set of states. We present our model and define the synthesis problems in Section 2. The first tool we present is called SynthKro. It is a module of the tool suite Kronos [12, 8]. SynthKro is based on the notion of controllable states, which are computed using a backward fixpoint iteration of special symbolic predecessor operators [29, 16, 19, 5]. The tool SynthKro, its algorithms and experimental results are presented in Section 3. The second tool we present is called FlySynth. It is based on an on-the-fly synthesis algorithm [25] which works on finite graphs with edges marked controllable or uncontrollable. The algorithm is on-the-fly in the sense that it can find a controller (or say that none exists) without necessarily exploring the entire state space. FlySynth can also be used also for controller synthesis of timed systems, in two ways: either by interpreting the timed automaton model in discrete time and using an appropriate abstraction to make the resulting semantic graph finite, or by interpreting the timed automaton in dense time and using the timeabstracting bisimulation quotient graph [26]. In both cases, we show how timed transitions are interpreted as controllable or uncontrollable. The tool FlySynth, its algorithms and experimental results are presented in Section 4.
booktitleProceedings of the 2nd Workshop on Real-Time Tools
titleTools for Controller Synthesis of Timed Systems

Springer, Berlin, Heidelberg

abstractWe consider the control problem for timed automata against specifications given as MTL formulas. The logic MTL is a linear-time timed temporal logic which extends LTL with timing constraints on modalities, and recently, its model-checking has been proved decidable in several cases. We investigate these decidable fragments of MTL (full MTL when interpreted over finite timed words, and Safety-MTL when interpreted over infinite timed words), and prove two kinds of results. (1) We first prove that, contrary to model-checking, the control problem is undecidable. Roughly, the computation of a lossy channel system could be encoded as a model-checking problem, and we prove here that a perfect channel system can be encoded as a control problem. (2) We then prove that if we fix the resources of the controller (by resources we mean clocks and constants that the controller can use), the control problem becomes decidable. This decidability result relies on properties of well (and better) quasi-orderings.
booktitleCONCUR 2006 - Concurrency Theory
titleController Synthesis for MTL Specifications
Control Problem,Controller Synthesis,Temporal Logic,Undesired Behaviour,Winning Strategy

abstractPlanning with preferences involves not only finding a plan that achieves the goal, it requires finding a preferred plan that achieves the goal, where preferences over plans are specified as part of the planner's input. In this paper we provide a technique for accomplishing this objective. Our technique can deal with a rich class of preferences, including so-called temporally extended preferences (TEPs). Unlike simple preferences which express desired properties of the final state achieved by a plan, TEPs can express desired properties of the entire sequence of states traversed by a plan, allowing the user to express a much richer set of preferences. Our technique involves converting a planning problem with TEPs into an equivalent planning problem containing only simple preferences. This conversion is accomplished by augmenting the inputed planning domain with a new set of predicates and actions for updating these predicates. We then provide a collection of new heuristics and a specialized search algorithm that can guide the planner towards preferred plans. Under some fairly general conditions our method is able to find a most preferred plan—i.e., an optimal plan. It can accomplish this without having to resort to admissible heuristics, which often perform poorly in practice. Nor does our technique require an assumption of restricted plan length or make-span. We have implemented our approach in the HPlan-P planning system and used it to compete in the 5th International Planning Competition, where it achieved distinguished performance in the Qualitative Preferences track.
journaltitleArtificial Intelligence
shortjournalArtificial Intelligence
titleA Heuristic Search Approach to Planning with Temporally Extended Preferences
PDDL3,Planning with preferences,Temporally extended preferences

Berlin, Heidelberg

abstractTPTL and MTL are two classical timed extensions of LTL. In this paper, we positively answer a 15-year-old conjecture that TPTL is strictly more expressive than MTL. But we show that, surprisingly, the TPTL formula proposed in [4] for witnessing this conjecture can be expressed in MTL. More generally, we show that TPTL formulae using only the F modality can be translated into MTL.
booktitleFSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science
titleOn the Expressiveness of TPTL and MTL
Atomic Proposition,Clock Valuation,Linear Temporal Logic,Model Check,Temporal Logic

abstractIn this paper, we show the decidability of a new subclass of linear hybrid automata. These automata are planar, that is, consist of two state variables, monotonic along some direction in the plane and have identity resets, that is, the values of the continuous variables are not reset to a different value on a discrete transition. Our proof uses a combination of a tree construction capturing the edge-to-edge reachability and a finite bisimulation construction. Our class strictly contains the class of two dimensional piecewise constant derivative systems for which decidability of the reachability problem is known. We investigate a number of problems related to infinite runs of weighted timed automata (with a single weight variable), subject to lower-bound constraints on the accumulated weight. Closing an open problem from Bouyer et al. (2008), we show that the existence of an infinite lower-bound-constrained run is—for us somewhat unexpectedly—undecidable for weighted timed automata with four or more clocks. This undecidability result assumes a fixed and known initial credit. We show that the related problem of existence of an initial credit for which there exists a feasible run is decidable in PSPACE. We also investigate the variant of these problems where only bounded-duration runs are considered, showing that this restriction makes our original problem decidable in NEXPTIME. We prove that the universal versions of all those problems (i.e, checking that all the considered runs satisfy the lower-bound constraint) are decidable in PSPACE. Finally, we extend this study to multi-weighted timed automata: the existence of a feasible run becomes undecidable even for bounded duration, but the existence of initial credits remains decidable (in PSPACE). Timed automata are a popular formalism to model real-time systems. They were introduced two decades ago to support formal verification. Since then they have also been used for other purposes and a large number of variants has been introduced to be able to deal with the many different kinds of requirements of real-time system development. This survey attempts to introduce a massive and complicated theoretical research area to a reader in an easy and compact manner. One objective of this paper is to inform a reader about the theoretical properties (or capabilities) of timed automata which are (or might be) useful for real-time model driven development. To achieve this goal, this paper presents a survey on semantics, decision problems, and variants of timed automata. The other objective of this paper is to inform a reader about the current state of the art of timed automata in practice. To achieve the second aim, this article presents a survey on timed automata's implementability and tools. Even though many attempts have been made to define the boundary between decidable and undecidable hybrid systems, the affair is far from being resolved. More and more low dimensional systems are being shown to be undecidable with respect to reachability, and many open problems in between are being discovered. In this paper, we present various two-dimensional hybrid systems for which the reachability problem is undecidable. We show their undecidability by simulating Minsky machines. Their proximity to the decidability frontier is understood by inspecting the most parsimonious constraints necessary to make reachability over these automata decidable. We also show that for other two-dimensional systems, the reachability question remains unanswered, by proving that it is as hard as the reachability problem for piecewise affine maps on the real line, which is a well known open problem. We investigate extensions of Alur and Dill's timed automata, based on the possibility to update the clocks in a more elaborate way than simply reset them to zero. We call these automata updatable timed automata. They form an undecidable class of models, in the sense that emptiness checking is not decidable. However, using an extension of the region graph construction, we exhibit interesting decidable subclasses. In a surprising way, decidability depends on the nature of the clock constraints which are used, diagonal-free or not, whereas these constraints play identical roles in timed automata. We thus describe in a quite precise way the thin frontier between decidable and undecidable classes of updatable timed automata. We also study the expressive power of updatable timed automata. It turns out that any updatable automaton belonging to some decidable subclass can be effectively transformed into an equivalent timed automaton without updates but with silent transitions. The transformation suffers from an enormous combinatorics blow-up which seems unavoidable. Therefore, updatable timed automata appear to be a concise model for representing and analyzing large classes of timed systems. Context-free languages of infinite words have recently found increasing interest. Here, we will present a second-order logic with the same expressive power as Büchi or Muller pushdown automata for infinite words. This extends fundamental logical characterizations of Büchi, Elgot, Trakhtenbrot for regular languages of finite and infinite words and a more recent logical characterization of Lautemann, Schwentick and Thérien for context-free languages of finite words to $\omega$-context-free languages. For our argument, we will investigate Greibach normal forms of $\omega$-context-free grammars as well as a new type of Büchi pushdown automata which can alter their stack by at most one element and without $\epsilon$-transitions. We show that they suffice to accept all $\omega$-context-free languages. This enables us to use similar results recently developed for infinite nested words. Simon's congruence, denoted by $\sim$n$<$math$><$msub is="true"$><$mrow is="true"$><$mo is="true"$>\sim<$/mo$><$/mrow$><$mrow is="true"$><$mi is="true"$>$n$<$/mi$><$/mrow$><$/msub$><$/math$>$, relates words having the same subwords of length up to n. We show that, over a k-letter alphabet, the number of words modulo $\sim$n$<$math$><$msub is="true"$><$mrow is="true"$><$mo is="true"$>\sim<$/mo$><$/mrow$><$mrow is="true"$><$mi is="true"$>$n$<$/mi$><$/mrow$><$/msub$><$/math$>$ is in 2$\Theta$(nk-1logn)$<$math$><$msup is="true"$><$mrow is="true"$><$mn is="true"$>$2$<$/mn$><$/mrow$><$mrow is="true"$><$mi is="true"$>\Theta<$/mi$><$mo stretchy="false" is="true"$>$($<$/mo$><$msup is="true"$><$mrow is="true"$><$mi is="true"$>$n$<$/mi$><$/mrow$><$mrow is="true"$><$mi is="true"$>$k$<$/mi$><$mo is="true"$>-<$/mo$><$mn is="true"$>$1$<$/mn$><$/mrow$><$/msup$><$mi is="true" mathvariant="normal"$>$log$<$/mi$><$mo is="true"$>$$<$/mo$><$mi is="true"$>$n$<$/mi$><$mo stretchy="false" is="true"$>$)$<$/mo$><$/mrow$><$/msup$><$/math$>$. Linear Dynamic Logic on finite traces (LDLF)$<$math$><$mo stretchy="false" is="true"$>$($<$/mo$><$msub is="true"$><$mrow is="true"$><$mi is="true" mathvariant="normal"$>$LDL$<$/mi$><$/mrow$><$mrow is="true"$><$mi is="true" mathvariant="normal"$>$F$<$/mi$><$/mrow$><$/msub$><$mo stretchy="false" is="true"$>$)$<$/mo$><$/math$>$ is a powerful logic for reasoning about the behaviour of concurrent and multi-agent systems. In this paper, we investigate techniques for both the characterisation and verification of equilibria in multi-player games with goals/objectives expressed using logics based on LDLF$<$math$><$msub is="true"$><$mrow is="true"$><$mi is="true" mathvariant="normal"$>$LDL$<$/mi$><$/mrow$><$mrow is="true"$><$mi is="true" mathvariant="normal"$>$F$<$/mi$><$/mrow$><$/msub$><$/math$>$. This study builds upon a generalisation of Boolean games, a logic-based game model of multi-agent systems where players have goals succinctly represented in a logical way. Because LDLF$<$math$><$msub is="true"$><$mrow is="true"$><$mi is="true" mathvariant="normal"$>$LDL$<$/mi$><$/mrow$><$mrow is="true"$><$mi is="true" mathvariant="normal"$>$F$<$/mi$><$/mrow$><$/msub$><$/math$>$ goals are considered, in the settings we study—Reactive Modules games and iterated Boolean games with goals over finite traces—players' goals can be defined to be regular properties while achieved in a finite, but arbitrarily large, trace. In particular, using alternating automata, the paper investigates automata-theoretic approaches to the characterisation and verification of (pure strategy Nash) equilibria, shows that the set of Nash equilibria in multi-player games with LDLF$<$math$><$msub is="true"$><$mrow is="true"$><$mi is="true" mathvariant="normal"$>$LDL$<$/mi$><$/mrow$><$mrow is="true"$><$mi is="true" mathvariant="normal"$>$F$<$/mi$><$/mrow$><$/msub$><$/math$>$ objectives is regular, and provides complexity results for the associated automata constructions. Studying complexity of various bribery problems has been one of the main research focus in computational social choice. In all the models of bribery studied so far, the briber has to pay every voter some amount of money depending on what the briber wants the voter to report and the briber has some budget at her disposal. Although these models successfully capture many real world applications, in many other scenarios, the voters may be unwilling to deviate too much from their true preferences. In this paper, we study the computational complexity of the problem of finding a preference profile which is as close to the true preference profile as possible and still achieves the briber's goal subject to budget constraints. We call this problem Local Distance constrained $bribery. We consider three important measures of distances, namely, swap distance, footrule distance, and maximum displacement distance, and resolve the complexity of the optimal bribery problem for many common voting rules. We show that the problem is polynomial time solvable for the plurality and veto voting rules for all the three measures of distance. On the other hand, we prove that the problem is NP$<$math$><$mi is="true" mathvariant="sans-serif"$>$NP$<$/mi$><$/math$>$-complete for a class of scoring rules which includes the Borda voting rule, maximin, Copeland$\alpha<$math$><$msup is="true"$><$mrow is="true"$><$mtext is="true"$>$Copeland$<$/mtext$><$/mrow$><$mrow is="true"$><$mi is="true"$>\alpha<$/mi$><$/mrow$><$/msup$><$/math$>$ for any $\alpha\in$[0,1]$<$math$><$mi is="true"$>\alpha<$/mi$><$mo is="true"$>\in<$/mo$><$mo stretchy="false" is="true"$>$[$<$/mo$><$mn is="true"$>$0$<$/mn$><$mo is="true"$>$,$<$/mo$><$mn is="true"$>$1$<$/mn$><$mo stretchy="false" is="true"$>$]$<$/mo$><$/math$>$, and Bucklin voting rules for all the three measures of distance even when the distance allowed per voter is 1 for the swap and maximum displacement distances and 2 for the footrule distance even without the budget constraints (which corresponds to having an infinite budget). For the k-approval voting rule for any constant k$>$1$<$math$><$mi is="true"$>$k$<$/mi$><$mo linebreak="goodbreak" linebreakstyle="after" is="true"$>\&$gt;$<$/mo$><$mn is="true"$>$1$<$/mn$><$/math$>$ and the simplified Bucklin voting rule, we show that the problem is NP$<$math$><$mi is="true" mathvariant="sans-serif"$>$NP$<$/mi$><$/math$>$-complete for the swap distance even when the distance allowed is 2 and for the footrule distance even when the distance allowed is 4 even without the budget constraints. We complement these hardness results by showing that the problem for the k-approval and simplified Bucklin voting rules is polynomial time solvable for the swap distance if the distance allowed is 1 and for the footrule distance if the distance allowed is at most 3. For the k-approval voting rule for the maximum displacement distance for any constant k$>$1$<$math$><$mi is="true"$>$k$<$/mi$><$mo linebreak="goodbreak" linebreakstyle="after" is="true"$>\&$gt;$<$/mo$><$mn is="true"$>$1$<$/mn$><$/math$>$, and for the simplified Bucklin voting rule for the maximum displacement distance, we show that the problem is NP$<$math$><$mi is="true" mathvariant="sans-serif"$>$NP$<$/mi$><$/math$>$-complete (with the budget constraints) and, without the budget constraints, they are polynomial time solvable.
journaltitleInformation Processing Letters
shortjournalInformation Processing Letters
titleTimed Automata and Additive Clock Constraints
Decidability of emptiness,Real-time systems,Timed automata

AAAI Press

abstractWe develop a general framework for agent abstraction based on the situation calculus and the ConGolog agent programming language. We assume that we have a high-level specification and a low-level specification of the agent, both represented as basic action theories. A refinement mapping specifies how each high-level action is implemented by a low-level ConGolog program and how each high-level fluent can be translated into a low-level formula. We define a notion of sound abstraction between such action theories in terms of the existence of a suitable bisimulation between their respective models. Sound abstractions have many useful properties that ensure that we can reason about the agent's actions (e.g., executability, projection, and planning) at the abstract level, and refine and concretely execute them at the low level. We also characterize the notion of complete abstraction where all actions (including exogenous ones) that the high level thinks can happen can in fact occur at the low level.
booktitleProceedings of the 31st Conference on Artificial Intelligence (AAAI)
titleAbstraction in Situation Calculus Action Theories
Abstraction,Agent,Bisimulation,Reasoning About Action,Refinement Mapping,Situation Calculus

booktitleProceedings of the 27th International Joint Conference on Artificial Intelligence (IJCAI)