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=article,heading=subbibliography,title=Journal Publications]

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)
titleAbstraction of Agents Executing Online and Their Abilities in the Situation Calculus

abstractWe present a hybrid discrete-continuous extension of Reiter's temporal situation calculus, directly inspired by hybrid systems in control theory. While keeping to the foundations of Reiter's approach, we extend it by adding a time argument to all fluents that represent continuous change. Thereby, we ensure that change can happen not only because of actions, but also due to the passage of time. We present a systematic methodology to derive, from simple premises, a new group of axioms which specify how continuous fluents change over time within a situation. We study regression for our new hybrid action theories and demonstrate what reasoning problems can be solved. Finally, we show that our hybrid theories indeed capture hybrid automata.
booktitleAdvances in Artificial Intelligence
titleHybrid Temporal Situation Calculus
Computer Science - Artificial Intelligence,Hybrid systems,Situation calculus,Temporal reasoning

abstractIn this paper we present KnowRob2, a second generation knowledge representation and reasoning framework for robotic agents. KnowRob2 is an extension and partial redesign of KnowRob, currently one of the most advanced knowledge processing systems for robots that has enabled them to successfully perform complex manipulation tasks such as making pizza, conducting chemical experiments, and setting tables. The knowledge base appears to be a conventional first-order time interval logic knowledge base, but it exists to a large part only virtually: many logical expressions are constructed on demand from data structures of the control program, computed through robotics algorithms including ones for motion planning and solving inverse kinematics problems, and log data stored in noSQL databases. Novel features and extensions of KnowRob2 substantially increase the capabilities of robotic agents of acquiring open-ended manipulation skills and competence, reasoning about how to perform manipulation actions more realistically, and acquiring commonsense knowledge.
booktitle2018 IEEE International Conference on Robotics and Automation (ICRA)
titleKnow Rob 2.0 — A 2nd Generation Knowledge Processing Framework for Cognition-Enabled Robotic Agents
2nd generation knowledge processing framework,advanced knowledge,chemical experiments,Cognition,cognition-enabled robotic agents,commonsense knowledge,complex manipulation tasks,Data structures,first-order time interval logic knowledge base,generation knowledge representation,inverse kinematic problem solving,knowledge based systems,Knowledge based systems,knowledge representation,KnowRob2.0,logical expressions,manipulator kinematics,manipulators,motion planning,Ontologies,open-ended manipulation skills,Physics,robotics algorithms,Robots,service robots,Task analysis

Berlin, Heidelberg

abstractIn 2005 we proposed the first efficient on-the-fly algorithm for solving games based on timed game automata with respect to reachability and safety properties. The first prototype presented at that time has now matured to a fully integrated tool with dramatic improvements both in terms of performance and the availability of the extended input language of Uppaal-4.0. The new tool can output strategies or let the user play against them both from the command line and from the graphical simulator that was completely re-designed.
booktitleComputer Aided Verification (CAV)
titleUPPAAL-Tiga: Time for Playing Games!
Controller Synthesis,Input Language,Safety Property,Time Automaton,Winning Strategy

abstractUPPAAL is a tool suitable for model checking real-time systems described as networks of timed automata communicating by channel synchronizations and extended with integer variables. Its first version was released in 1995 and its development is still very active. It now features an advanced modeling language, a user-friendly graphical interface, and a performant model checker engine. In addition, several flavors of the tool have matured in recent years. In this paper, we present how we managed to maintain the tool during 15 years, its current architecture with its challenges, and we give the future directions of the tool. Copyright © 2011 John Wiley & Sons, Ltd.
journaltitleSoftware: Practice and Experience
titleDeveloping UPPAAL over 15 Years

RWTH Aachen University

abstractThe problem of projection has been identified as a fundamental reasoning concern in dynamical domains, where we are to determine whether or not some conditions will hold after a sequence of actions has been performed starting in some initial state. Solving the problem requires, at the very least, effectively reasoning about how actions transform the world, and inferring the logical consequences of the initial knowledge base (KB). For various reasons, tractability one of them, applications often make the closed-world assumption, thereby limiting the scope of these systems for the real world. In this thesis, using the language of the situation calculus, we investigate the computational properties of a number of unsolved reasoning tasks in the context of projection with incomplete information. We first look at inherently incomplete KBs, where the information provided to the agent may not determine every fact about the world. Projection, then, may involve reasoning about what is believed and also, about what is not believed. We then look at physical agents with unreliable hardware, as a result of which actions lead to certain kinds of incomplete knowledge. Intuitively, beliefs should be (periodically) synchronized with this noise. Finally, we consider the presence of other agents in the environment, whose beliefs may differ arbitrarily, and the formalism should incorporate what others sense and learn during actions. To enable a precise mathematical treatment of incomplete KBs, we appeal to a seminal proposal by Levesque, called only knowing. Building on existing work, we investigate projection wrt extensions to the situation calculus for only knowing, noisy hardware and multiple agents. Our central contribution will be to show that, in spite of the additional expressivity, reasoning about knowledge and action reduces to non- epistemic non-dynamic reasoning about the initial KB. More precisely, we show that when the initial KB is an arbitrary first-order theory, we are able to identify conditions under which projection can be solved by progressing the KB to a sentence reflecting the changes due to actions that have already occurred. Moreover, when effectors are unreliable, we allow the system to maintain probabilistic beliefs and then show how projection can be addressed by means of updating these beliefs. Finally, when there are many agents in the picture, we show that queries about the future can be resolved by regressing the query backwards to a formula about the initial KB. Only knowing comes with a significant result that allows us to reduce queries about knowledge to first-order theorem-proving tasks, which is then made use of when solving projection.
titleOn the Projection Problem in Active Knowledge Bases with Incomplete Information

abstraction is a powerful idea widely used in science, to model, reason and explain the behavior of systems in a more tractable search space, by omitting irrelevant details. While notions of abstraction have matured for deterministic systems, the case for abstracting probabilistic models is not yet fully understood. In this paper, we provide a semantical framework for analyzing such abstractions from first principles. We develop the framework in a general way, allowing for expressive languages, including logic-based ones that admit relational, deterministic and hierarchical constructs with stochastic primitives. We motivate a definition of consistency between a high-level model and its low-level counterpart, but also treat the case when the high-level model is missing critical information present in the low-level model. We go on to prove properties of abstractions, both at the level of the parameter as well as the structure of the models. We conclude with some observations about how abstractions can be derived automatically.
journaltitleKnowledge-Based Systems
shortjournalKnowledge-Based Systems
shorttitleAbstracting Probabilistic Models
titleAbstracting Probabilistic Models: Relations, Constraints and Beyond

Berlin, Heidelberg

abstractUppaal is a tool suite for automatic verification of safety and bounded liveness properties of real-time systems modeled as networks of timed automata. It includes: a graphical interface that supports graphical and textual representations of networks of timed automata, and automatic transformation from graphical representations to textual format, a compiler that transforms a certain class of linear hybrid systems to networks of timed automata, and a model-checker which is implemented based on constraint-solving techniques. Uppaal also supports diagnostic model-checking providing diagnostic information in case verification of a particular real-time systems fails.The current version of Uppaal is available on the World Wide Web via the Uppaal home page http://www.docs.uu.se/docs/rtmv/uppaal.
booktitleHybrid Systems III
titleUPPAAL — a Tool Suite for Automatic Verification of Real-Time Systems
Atomic Clock,Automatic Verification,Data Variable,Hybrid Automaton,Variable Assignment

IOS Press

abstractTimed automata are among the most widely studied models for real-time systems. Silent transitions, i.e., $\epsilon$-transitions, have already been proposed in the original paper on timed automata by Alur and Dill [3]. We show that the class TL$\epsilon$ of timed langu
journaltitleFundamenta Informaticae
titleCharacterization of the Expressive Power of Silent Transitions in Timed Automata

abstractWe introduce a new approach to planning in STRIPS-like domains based on constructing and analyzing a compact structure we call a Planning Graph. We describe a new planner, Graphplan, that uses this paradigm. Graphplan always returns a shortest possible partial-order plan, or states that no valid plan exists. We provide empirical evidence in favor of this approach, showing that Graphplan outperforms the total-order planner, Prodigy, and the partial-order planner, UCPOP, on a variety of interesting natural and artificial planning problems. We also give empirical evidence that the plans produced by Graphplan are quite sensible. Since searches made by this approach are fundamentally different from the searches of other common planning methods, they provide a new perspective on the planning problem.
journaltitleArtificial Intelligence
titleFast Planning through Planning Graph Analysis
general purpose planning,graph algorithms,planning graph analysis,strips planning

AAAI Press

booktitleProceedings of the 10th International Conference on Principles of Knowledge Representation and Reasoning (KR)
titlePlanning with Qualitative Temporal Preferences

abstractIn this paper, we address the problem of specifying and computing preferred plans using rich, qualitative, user preferences. We propose a logical language for specifying preferences over the evolution of states and actions associated with a plan. We provide a semantics for our first-order preference language in the situation calculus, and prove that progression of our preference formulae preserves this semantics. This leads to the development of PPlan, a bounded best-first search planner that computes preferred plans. Our preference language is amenable to integration with many existing planners, and beyond planning, can be used to support a diversity of dynamical reasoning tasks that employ preferences.
journaltitleArtificial Intelligence
shortjournalArtificial Intelligence
titleSpecifying and Computing Preferred Plans
Knowledge representation,Planning with preferences,Preferences

abstractIn the AIPS98 Planning Contest, the hsp planner showed that heuristic search planners can be competitive with state-of-the-art Graphplan and sat planners. Heuristic search planners like hsp transform planning problems into problems of heuristic search by automatically extracting heuristics from Strips encodings. They differ from specialized problem solvers such as those developed for the 24-Puzzle and Rubik's Cube in that they use a general declarative language for stating problems and a general mechanism for extracting heuristics from these representations. In this paper, we study a family of heuristic search planners that are based on a simple and general heuristic that assumes that action preconditions are independent. The heuristic is then used in the context of best-first and hill-climbing search algorithms, and is tested over a large collection of domains. We then consider variations and extensions such as reversing the direction of the search for speeding node evaluation, and extracting information about propositional invariants for avoiding dead-ends. We analyze the resulting planners, evaluate their performance, and explain when they do best. We also compare the performance of these planners with two state-of-the-art planners, and show that the simplest planner based on a pure best-first search yields the most solid performance over a large set of problems. We also discuss the strengths and limitations of this approach, establish a correspondence between heuristic search planning and Graphplan, and briefly survey recent ideas that can reduce the current gap in performance between general heuristic search planners and specialized solvers.
journaltitleArtificial Intelligence
shortjournalArtificial Intelligence
titlePlanning as Heuristic Search
Domain-independent heuristics,Forward/backward search,Graphplan,Heuristic search,Non-optimal planning,Planning,Strips

abstractWe develop a general framework for abstracting the behavior of an agent that operates in a nondeterministic domain, i.e., where the agent does not control the outcome of the nondeterministic actions, based on the nondeterministic situation calculus and the ConGolog programming language. We assume that we have both an abstract and a concrete nondeterministic basic action theory, and a refinement mapping which specifies how abstract actions, decomposed into agent actions and environment reactions, are implemented by concrete ConGolog programs. This new setting supports strategic reasoning and strategy synthesis, by allowing us to quantify separately on agent actions and environment reactions. We show that if the agent has a (strong FOND) plan/strategy to achieve a goal/complete a task at the abstract level, and it can always execute the nondeterministic abstract actions to completion at the concrete level, then there exist a refinement of it that is a (strong FOND) plan/strategy to achieve the refinement of the goal/task at the concrete level.
titleAbstraction of Nondeterministic Situation Calculus Action Theories

AAAI Press

abstractWe consider a sequence of successively more restrictive definitions of abstraction for causal models, starting with a notion introduced by Rubenstein et al. (2017) called exact transformation that applies to probabilistic causal models, moving to a notion of uniform transformation that applies to deterministic causal models and does not allow differences to be hidden by the “right” choice of distribution, and then to abstraction, where the interventions of interest are determined by the map from low-level states to high-level states, and strong abstraction, which takes more seriously all potential interventions in a model, not just the allowed interventions. We show that procedures for combining micro-variables into macro-variables are instances of our notion of strong abstraction, as are all the examples considered by Rubenstein et al.
booktitleProceedings of the 33rd AAAI Conference on Artificial Intelligence (AAAI)
titleAbstracting Causal Models

abstractAgents interacting with an incompletely known world need to be able to reason about the effects of their actions, and to gain further information about that world they need to use sensors of some sort. Unfortunately, both the effects of actions and the information returned from sensors are subject to error. To cope with such uncertainties, the agent can maintain probabilistic beliefs about the state of the world. With probabilistic beliefs the agent will be able to quantify the likelihood of the various outcomes of its actions and is better able to utilize the information gathered from its error-prone actions and sensors. In this paper, we present a model in which we can reason about an agent's probabilistic degrees of belief and the manner in which these beliefs change as various actions are executed. We build on a general logical theory of action developed by Reiter and others, formalized in the situation calculus. We propose a simple axiomatization that captures an agent's state of belief and the manner in which these beliefs change when actions are executed. Our model displays a number of intuitively reasonable properties.
journaltitleArtificial Intelligence
shortjournalArtificial Intelligence
titleReasoning about Noisy Sensors and Effectors in the Situation Calculus
Logical representations,Probabilistic models,Sensors

Berlin, Heidelberg

abstractSymbolic Model Checking [3], [14] has proven to be a powerful technique for the verification of reactive systems. BDDs [2] have traditionally been used as a symbolic representation of the system. In this paper we show how boolean decision procedures, like Stålmarck's Method [16] or the Davis & Putnam Procedure [7], can replace BDDs. This new technique avoids the space blow up of BDDs, generates counterexamples much faster, and sometimes speeds up the verification. In addition, it produces counterexamples of minimal length. We introduce a bounded model checking procedure for LTL which reduces model checking to propositional satisfiability.We show that bounded LTL model checking can be done without a tableau construction. We have implemented a model checker BMC, based on bounded model checking, and preliminary results are presented.
booktitleTools and Algorithms for the Construction and Analysis of Systems (TACAS)
titleSymbolic Model Checking without BDDs
Kripke Structure,Liveness Property,Model Check,Propositional Formula,Symbolic Model Check

abstractOver the years increasingly sophisticated planning algorithms have been developed. These have made for more efficient planners, but unfortunately these planners still suffer from combinatorial complexity even in simple domains. Theoretical results demonstrate that planning is in the worst case intractable. Nevertheless, planning in particular domains can often be made tractable by utilizing additional domain structure. In fact, it has long been acknowledged that domain-independent planners need domain-dependent information to help them plan effectively. In this work we present an approach for representing and utilizing domain-specific control knowledge. In particular, we show how domain-dependent search control knowledge can be represented in a temporal logic, and then utilized to effectively control a forward-chaining planner. There are a number of advantages to our approach, including a declarative semantics for the search control knowledge; a high degree of modularity (new search control knowledge can be added without affecting previous control knowledge); and an independence of this knowledge from the details of the planning algorithm. We have implemented our ideas in the TLplan system, and have been able to demonstrate its remarkable effectiveness in a wide range of planning domains.
journaltitleArtificial Intelligence
shortjournalArtificial Intelligence
titleUsing Temporal Logics to Express Search Control Knowledge for Planning
Planning,Search control knowledge,Temporal Logic

Cambridge, MA, USA

MIT Press

abstractA comprehensive introduction to the foundations of model checking, a fully automated technique for finding flaws in hardware and software; with extensive examples and both practical and theoretical exercises.
titlePrinciples of Model Checking

abstractModern satisfiability (SAT) solvers have become the enabling technology of many model checkers. In this chapter, we will focus on those techniques most relevant to industrial practice. In bounded model checking (BMC), a transition system and a property are jointly unwound for a given number k$k$of steps to obtain a formula that is satisfiable if there is a counterexample for the property up to length k$k$. The formula is then passed to an efficient SAT solver. The strength of BMC is refutation: BMC has been used to discover subtle flaws in digital systems. We cover the application of BMC to both hardware and software systems, and to hardware/software co-verification. We also discuss means to make BMC complete, including k$k$-induction, Craig interpolation, abstraction refinement techniques, and inductive techniques with iterative strengthening.
booktitleHandbook of Model Checking
titleSAT-Based Model Checking

abstractIn planning, goals have traditionally been viewed as specifying a set of desirable final states. Any plan that transforms the current state to one of these desirable states is viewed to be correct. Goals of this form are limited in what they can specify, and they also do not allow us to constrain the manner in which the plan achieves its objectives. We propose viewing goals as specifying desirable sequences of states, and a plan to be correct if its execution yields one of these desirable sequences. We present a logical language, a temporal logic, for specifying goals with this semantics. Our language is rich and allows the representation of a range of temporally extended goals, including classical goals, goals with temporal deadlines, quantified goals (with both universal and existential quantification), safety goals, and maintenance goals. Our formalism is simple and yet extends previous approaches in this area. We also present a planning algorithm that can generate correct plans for these goals. This algorithm has been implemented, and we provide some examples of the formalism at work. The end result is a planning system which can generate plans that satisfy a novel and useful set of conditions.
journaltitleAnnals of Mathematics and Artificial Intelligence
titlePlanning for Temporally Extended Goals
planning,temporal logic

AAAI Press

booktitleProceedings of the 36th AAAI Conference on Artificial Intelligence (AAAI)
titleFrom Actions to Programs as Abstract Actual Causes

AAAI Press

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

AAAI Press

abstractOnly knowing captures the intuitive notion that the beliefs of an agent are precisely those that follow from its knowledge base. It has previously been shown to be useful in characterizing knowledge-based reasoners, especially in a quantified setting. While this allows us to reason about incomplete knowledge in the sense of not knowing whether a formula is true or not, there are many applications where one would like to reason about the degree of belief in a formula. In this work, we propose a new general first-order account of probability and only knowing that admits knowledge bases with incomplete and probabilistic specifications. Beliefs and non-beliefs are then shown to emerge as a direct logical consequence of the sentences of the knowledge base at a corresponding level of specificity.
booktitleProceedings of the 30th Conference on Artificial Intelligence (AAAI 2016)
titleA First-Order Logic of Probability and Only Knowing in Unbounded Domains
Technical Papers: Knowledge Representation and Rea

abstractKnowledge-based programs contain both world-altering actions, which upon execution change the state of the world, and sensing actions, which upon execution change the knowledge state of the agent. Knowledge-based programming has been proposed as an alternative to planning, since programs allow solving families of planning problems. Notwithstanding, agents equipped with a variety of knowledge-based procedures can compose these procedures to achieve goals, exhibiting greater degrees of flexibility. Optimized state-of-the-art planners, unfortunately, cannot be used directly to compose programs since they require operators (not programs), defined by preconditions and effects. In this article we study how to compute preconditions and effects of knowledge-based programs in order to allow state-of-the-art planners to construct plans with knowledge-based programs as building blocks. We study the problem in the language of the situation calculus, appealing to Golog to represent our programs. To this end, we propose an offline execution semantics for Golog programs with sensing. We then propose a compilation method that transforms our action theory with programs into a new theory where programs are replaced by primitive actions. This enables us to use state-of-the-art, operator-based planning techniques to plan with programs that sense for a restricted but compelling class of problems. Finally, we discuss the applicability of these results to existing operator-based planners that support sensing and illustrate the computational advantage of planning with programs that sense via an experiment.
journaltitleArtificial Intelligence
shortjournalArtificial Intelligence
titleKnowledge-Based Programs as Building Blocks for Planning
Automated planning,Contingent planning,Epistemic planning,Knowledge-based planning

San Francisco, CA

Morgan Kaufmann

abstractClassical planning started with goals and produced plans. To do something similar in a reactive framework, it is necessary to treat the achievement or maintenance of a goal as specifying a default behavior, while at the same time being able to deploy tools to generate more complex plans. These tools rely on representing the relations between goals and plan patterns that achieve them. An important component of the representation is a set of fast, local methods for making probabilistic estimations of the quality of proposed plans, including their robustness, completeness, and efficiency.
booktitleArtificial Intelligence Planning Systems
titleDeclarative Goals in Reactive Plans

Berlin, Heidelberg

abstractWe describe XFRML, the transformation language of the planning system XFRM. XFRM is embedded in a simulated robot that performs jobs in a changing and partly unknown environment. XFRML allows XFRM to anticipate and forestall many common flaws in autonomous robot behavior that cannot be dealt with by other planning representations. In order to diagnose execution failures in projected execution scenarios, XFRM has to infer whether or not particular parts of the plan were projected to be executed and why. The use of XFRML makes such inferences possible because XFRML not only represents the physical effects of plan execution, but also the process of plan interpretation, as well as temporal, causal, and teleological relationships among plan interpretation, the world, and the physical behavior of the robot.
booktitleRecent Advances in AI Planning
titleExpressing Transformations of Structured Reactive Plans
Horn Clause,Object Description,Plan Execution,Plan Failure,Reactive Plan

abstractThis paper describes CRAM (Cognitive Robot Abstract Machine) as a software toolbox for the design, the implementation, and the deployment of cognition-enabled autonomous robots performing everyday manipulation activities. CRAM equips autonomous robots with lightweight reasoning mechanisms that can infer control decisions rather than requiring the decisions to be preprogrammed. This way CRAM-programmed autonomous robots are much more flexible, reliable, and general than control programs that lack such cognitive capabilities. CRAM does not require the whole domain to be stated explicitly in an abstract knowledge base. Rather, it grounds symbolic expressions in the knowledge representation into the perception and actuation routines and into the essential data structures of the control programs. In the accompanying video, we show complex mobile manipulation tasks performed by our household robot that were realized using the CRAM infrastructure.
booktitle2010 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS)
titleCRAM — A Cognitive Robot Abstract Machine for Everyday Manipulation in Human Environments
abstract knowledge base,Cognition,cognition enabled autonomous robots,cognitive capability,cognitive robot abstract machine,cognitive systems,complex mobile manipulation activity,Computer architecture,control programs,CRAM programmed autonomous robots,household robot,human environment,infer control decision,Kernel,knowledge representation,lightweight reasoning mechanism,manipulators,mobile robots,program compilers,Robot control,robot programming,Robot sensing systems,software toolbox,symbol manipulation,symbolic expression,Trajectory

abstractIn order to behave intelligently, artificial agents must be able to deliberatively plan their future actions. Unfortunately, realistic agent environments are usually highly dynamic and only partially observable, which makes planning computationally hard. For most practical purposes this rules out planning techniques that account for all possible con- tingencies in the planning process. However, many agent environments permit an alternative approach, namely continual planning, i.e. the interleaving of planning with acting and sens- ing. This paper presents a new principled approach to continual planning that describes why andwhen an agent should switch between planning and acting. The resulting continual plan- ning algorithm enables agents to deliberately postpone parts of their planning process and instead actively gather missing information that is relevant for the later refinement of the plan. To this end, the algorithm explictly reasons about the knowledge (or lack thereof) of an agent and its sensory capabilities. These concepts are modelled in the planning language (MAPL). Since in many environments the major reason for dynamism is the behaviour of other agents, MAPL can also model multiagent environments, common knowledge among agents, and communicative actions between them. For Continual Planning, MAPL intro- duces the concept of of assertions, abstract actions that substitute yet unformed subplans. To evaluate our continual planning approach empirically we have developed MAPSIM, a sim- ulation environment that automatically builds multiagent simulations from formal MAPL domains. Thus, agents can not only plan, but also execute their plans, perceive their envi- ronment, and interact with each other. Our experiments show that, using continual planning techniques, deliberate action planning can be used efficiently even in complex multiagent environments.
journaltitleAutonomous Agents and Multi-Agent Systems
titleContinual Planning and Acting in Dynamic Multiagent Environments
Continual planning,Multiagent planning

Berlin, Heidelberg

abstractWe present Acacia+, a tool for solving the LTL realizability and synthesis problems. We use recent approaches that reduce these problems to safety games, and can be solved efficiently by symbolic incremental algorithms based on antichains. The reduction to safety games offers very interesting properties in practice: the construction of compact solutions (when they exist) and a compositional approach for large conjunctions of LTL formulas.
booktitleComputer Aided Verification (CAV)
titleAcacia+, a Tool for LTL Synthesis
antichains,Church problem,LTL synthesis,Moore machines,safety games

abstractDespite recent progress in AI planning, many benchmarks remain challenging for current planners. In many domains, the performance of a planner can greatly be improved by discovering and exploiting information about the domain structure that is not explicitly encoded in the initial PDDL formulation. In this paper we present and compare two automated methods that learn relevant information from previous experience in a domain and use it to solve new problem instances. Our methods share a common four-step strategy. First, a domain is analyzed and structural information is extracted, then macro-operators are generated based on the previously discovered structure. A filtering and ranking procedure selects the most useful macro-operators. Finally, the selected macros are used to speed up future searches. We have successfully used such an approach in the fourth international planning competition IPC-4. Our system, Macro-FF, extends Hoffmann's state-of-the-art planner FF 2.3 with support for two kinds of macro-operators, and with engineering enhancements. We demonstrate the effectiveness of our ideas on benchmarks from international planning competitions. Our results indicate a large reduction in search effort in those complex domains where structural information can be inferred.
journaltitleJournal of Artificial Intelligence Research
titleMacro-FF: Improving AI Planning with Automatically Learned Macro-Operators

AAAI Press

abstractWe propose a framework for robot programming which allows the seamless integration of explicit agent programming with decision-theoretic planning. Specifically, the DTGolog model allows one to partially specify a control program in a highlevel, logical language, and provides an interpreter that, given a logical axiomatization of a domain, will determine the optimal completion of that program (viewed as a Markov decision process). We demonstrate the utility of this model with results...
booktitleProceedings of the 17th National Conference on Artificial Intelligence (AAAI)
titleDecision-Theoretic, High-Level Agent Programming in the Situation Calculus

abstractWe 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.
journaltitleTheoretical Computer Science
shortjournalTheoretical Computer Science
titleUpdatable Timed Automata

Springer, Berlin, Heidelberg

abstractMetric Interval Temporal Logic (MITL) is a popular formalism for expressing real-time specifications. This logic achieves decidability by restricting the precision of timing constraints, in...
booktitleAutomata, Languages and Programming
titleOn Expressiveness and Complexity in Real-Time Model Checking

abstractIn this paper, we present several timed extensions of temporal logics, that can be used for model-checking real-time systems. We give different formalisms and the corresponding decidability/complexity results. We also give intuition to explain these results.
journaltitleElectronic Notes in Theoretical Computer Science
shortjournalElectronic Notes in Theoretical Computer Science
titleModel-Checking Timed Temporal Logics
model-checking,reading list,temporal logics,timed systems

abstractIn this paper we present a new data structure for representing Boolean functions and an associated set of manipulation algorithms. Functions are represented by directed, acyclic graphs in a manner similar to the representations introduced by Lee [1] and Akers [2], but with further restrictions on the ordering of decision variables in the graph. Although a function requires, in the worst case, a graph of size exponential in the number of arguments, many of the functions encountered in typical applications have a more reasonable representation. Our algorithms have time complexity proportional to the sizes of the graphs being operated on, and hence are quite efficient as long as the graphs do not grow too large. We present experimental results from applying these algorithms to problems in logic design verification that demonstrate the practicality of our approach.
journaltitleIEEE Transactions on Computers
titleGraph-Based Algorithms for Boolean Function Manipulation
binary decision diagrams,Boolean functions,logic design verification,symbolic manipulation

abstractWe reduce synthesis for CTL* properties to synthesis for LTL. In the context of model checking this is impossible - CTL* is more expressive than LTL. Yet, in synthesis we have knowledge of the system structure and we can add new outputs. These outputs can be used to encode witnesses of the satisfaction of CTL* subformulas directly into the system. This way, we construct an LTL formula, over old and new outputs and original inputs, which is realisable if, and only if, the original CTL* formula is realisable. The CTL*-via-LTL synthesis approach preserves the problem complexity, although it might increase the minimal system size. We implemented the reduction, and evaluated the CTL*-via-LTL synthesiser on several examples.
journaltitleElectronic Proceedings in Theoretical Computer Science
shortjournalElectronic Proceedings in Theoretical Computer Science
titleCTL* Synthesis via LTL Synthesis

abstractMany different methods have been devised for automatically verifying finite state systems by examining state-graph models of system behavior. These methods all depend on decision procedures that explicitly represent the state space using a list or a table that grows in proportion to the number of states. We describe a general method that represents the state space symbolically instead of explicitly. The generality of our method comes from using a dialect of the Mu-Calculus as the primary specification language. We describe a model checking algorithm for Mu-Calculus formulas that uses Bryant's Binary Decision Diagrans (Bryant, R. E., 1986, IEEE Trans. Comput.C-35) to represent relations and formulas. We then show how our new Mu-Calculus model checking algorithm can be used to derive efficient decision procedures for CTL model checking, satisfiability of linear-time temporal logic formulas, strong and weak observational equivalence of finite transition systems, and language containment for finite $\omega$-automata. The fixed point computations for each decision procedure are sometimes complex, but can be concisely expressed in the Mu-Calculus. We illustrate the practicality of our approach to symbolic model checking by discussing how it can be used to verify a simple synchronous pipeline circuit.
journaltitleInformation and Computation
shortjournalInformation and Computation
shorttitleSymbolic Model Checking
titleSymbolic Model Checking: 1020 States and Beyond

Berlin, Heidelberg

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

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

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

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

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

Berlin, Heidelberg

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

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

San Francisco, CA, USA

Morgan Kaufmann Publishers Inc.

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

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

Berlin, Heidelberg

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

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

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

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

journaltitleJournal of the ACM
shortjournalJ. ACM

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

AAAI Press

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

AAAI Press

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

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

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

AAAI Press

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

RWTH Aachen University

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

AAAI Press

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

IOS Press

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

AAAI Press

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

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

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

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

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

labelalphaDe +22