SearcharxivSearch

arXiv subjects

Andrea Micheli

Publications and source records attributed to Andrea Micheli.

17 recordsLinked to original sources

Exploiting Symbolic Heuristics for the Synthesis of Domain-Specific Temporal Planning Guidance using Reinforcement Learning

Recent work investigated the use of Reinforcement Learning (RL) for the synthesis of heuristic guidance to improve the performance of temporal planners when a domain is fixed and a set of training problems (not plans) is given. The idea is to extract a heuristic from the value function of a particular (possibly infinite-state) MDP constructed over the training problems. In this paper, we propose an evolution of this learning and planning framework that focuses on exploiting the information provided by symbolic heuristics during both the RL and planning phases. First, we formalize different reward schemata for the synthesis and use symbolic heuristics to mitigate the problems caused by the truncation of episodes needed to deal with the potentially infinite MDP. Second, we propose learning a residual of an existing symbolic heuristic, which is a "correction" of the heuristic value, instead of eagerly learning the whole heuristic from scratch. Finally, we use the learned heuristic in combination with a symbolic heuristic using a multiple-queue planning approach to balance systematic search with imperfect learned information. We experimentally compare all the approaches, highlighting their strengths and weaknesses and significantly advancing the state of the art for this planning and learning schema.

cs.AI

Interleaving Scheduling and Motion Planning with Incremental Learning of Symbolic Space-Time Motion Abstractions

Task and Motion Planning combines high-level task sequencing (what to do) with low-level motion planning (how to do it) to generate feasible, collision-free execution plans. However, in many real-world domains, such as automated warehouses, tasks are predefined, shifting the challenge to if, when, and how to execute them safely and efficiently under resource, time and motion constraints. In this paper, we formalize this as the Scheduling and Motion Planning problem for multi-object navigation in shared workspaces. We propose a novel solution framework that interleaves off-the-shelf schedulers and motion planners in an incremental learning loop. The scheduler generates candidate plans, while the motion planner checks feasibility and returns symbolic feedback, i.e., spatial conflicts and timing adjustments, to guide the scheduler towards motion-feasible solutions. We validate our proposal on logistics and job-shop scheduling benchmarks augmented with motion tasks, using state-of-the-art schedulers and sampling-based motion planners. Our results show the effectiveness of our framework in generating valid plans under complex temporal and spatial constraints, where synchronized motion is critical.

cs.RO

Compiling Temporal Numeric Planning into Discrete PDDL+: Extended Version

Since the introduction of the PDDL+ modeling language, it was known that temporal planning with durative actions (as in PDDL 2.1) could be compiled into PDDL+. However, no practical compilation was presented in the literature ever since. We present a practical compilation from temporal planning with durative actions into PDDL+, fully capturing the semantics and only assuming the non-self-overlapping of actions. Our compilation is polynomial, retains the plan length up to a constant factor and is experimentally shown to be of practical relevance for hard temporal numeric problems.

cs.AI

Counterfactual Scenarios for Automated Planning

Counterfactual Explanations (CEs) are a powerful technique used to explain Machine Learning models by showing how the input to a model should be minimally changed for the model to produce a different output. Similar proposals have been made in the context of Automated Planning, where CEs have been characterised in terms of minimal modifications to an existing plan that would result in the satisfaction of a different goal. While such explanations may help diagnose faults and reason about the characteristics of a plan, they fail to capture higher-level properties of the problem being solved. To address this limitation, we propose a novel explanation paradigm that is based on counterfactual scenarios. In particular, given a planning problem $P$ and an \ltlf formula $ψ$ defining desired properties of a plan, counterfactual scenarios identify minimal modifications to $P$ such that it admits plans that comply with $ψ$. In this paper, we present two qualitative instantiations of counterfactual scenarios based on an explicit quantification over plans that must satisfy $ψ$. We then characterise the computational complexity of generating such counterfactual scenarios when different types of changes are allowed on $P$. We show that producing counterfactual scenarios is often only as expensive as computing a plan for $P$, thus demonstrating the practical viability of our proposal and ultimately providing a framework to construct practical algorithms in this area.

cs.AI

Platform-Aware Mission Planning

Planning for autonomous systems typically requires reasoning with models at different levels of abstraction, and the harmonization of two competing sets of objectives: high-level mission goals that refer to an interaction of the system with the external environment, and low-level platform constraints that aim to preserve the integrity and the correct interaction of the subsystems. The complicated interplay between these two models makes it very hard to reason on the system as a whole, especially when the objective is to find plans with robustness guarantees, considering the non-deterministic behavior of the lower layers of the system. In this paper, we introduce the problem of Platform-Aware Mission Planning (PAMP), addressing it in the setting of temporal durative actions. The PAMP problem differs from standard temporal planning for its exists-forall nature: the high-level plan dealing with mission goals is required to satisfy safety and executability constraints, for all the possible non-deterministic executions of the low-level model of the platform and the environment. We propose two approaches for solving PAMP. The first baseline approach amalgamates the mission and platform levels, while the second is based on an abstraction-refinement loop that leverages the combination of a planner and a verification engine. We prove the soundness and completeness of the proposed approaches and validate them experimentally, demonstrating the importance of heterogeneous modeling and the superiority of the technique based on abstraction-refinement.

cs.AI

A Meta-Engine Framework for Interleaved Task and Motion Planning using Topological Refinements

Task And Motion Planning (TAMP) is the problem of finding a solution to an automated planning problem that includes discrete actions executable by low-level continuous motions. This field is gaining increasing interest within the robotics community, as it significantly enhances robot's autonomy in real-world applications. Many solutions and formulations exist, but no clear standard representation has emerged. In this paper, we propose a general and open-source framework for modeling and benchmarking TAMP problems. Moreover, we introduce an innovative meta-technique to solve TAMP problems involving moving agents and multiple task-state-dependent obstacles. This approach enables using any off-the-shelf task planner and motion planner while leveraging a geometric analysis of the motion planner's search space to prune the task planner's exploration, enhancing its efficiency. We also show how to specialize this meta-engine for the case of an incremental SMT-based planner. We demonstrate the effectiveness of our approach across benchmark problems of increasing complexity, where robots must navigate environments with movable obstacles. Finally, we integrate state-of-the-art TAMP algorithms into our framework and compare their performance with our achievements.

cs.RO

Formal Analysis and Verification of Max-Plus Linear Systems

Max-Plus Linear (MPL) systems are an algebraic formalism with practical applications in transportation networks, manufacturing and biological systems. In this paper, we investigate the problem of automatically analyzing the properties of MPL, taking into account both structural properties such as transient and cyclicity, and the open problem of user-defined temporal properties. We propose Time-Difference LTL (TDLTL), a logic that encompasses the delays between the discrete time events governed by an MPL system, and characterize the problem of model checking TDLTL over MPL. We first consider a framework based on the verification of infinite-state transition systems, and propose an approach based on an encoding into model checking. Then, we leverage the specific features of MPL systems to devise a highly optimized, combinational approach based on Satisfiability Modulo Theory (SMT). We experimentally evaluate the features of the proposed approaches on a large set of benchmarks. The results show that the proposed approach substantially outperforms the state of the art competitors in expressiveness and effectiveness, and demonstrate the superiority of the combinational approach over the reduction to model checking.

cs.FL

An Efficient Incremental Simple Temporal Network Data Structure for Temporal Planning

One popular technique to solve temporal planning problems consists in decoupling the causal decisions, demanding them to heuristic search, from temporal decisions, demanding them to a simple temporal network (STN) solver. In this architecture, one needs to check the consistency of a series of STNs that are related one another, therefore having methods to incrementally re-use previous computations and that avoid expensive memory duplication is of paramount importance. In this paper, we describe in detail how STNs are used in temporal planning, we identify a clear interface to support this use-case and we present an efficient data-structure implementing this interface that is both time- and memory-efficient. We show that our data structure, called \deltastn, is superior to other state-of-the-art approaches on temporal planning sequences of problems.

cs.AI

Computation of the Transient in Max-Plus Linear Systems via SMT-Solving

This paper proposes a new approach, grounded in Satisfiability Modulo Theories (SMT), to study the transient of a Max-Plus Linear (MPL) system, that is the number of steps leading to its periodic regime. Differently from state-of-the-art techniques, our approach allows the analysis of periodic behaviors for subsets of initial states, as well as the characterization of sets of initial states exhibiting the same specific periodic behavior and transient. Our experiments show that the proposed technique dramatically outperforms state-of-the-art methods based on max-plus algebra computations for systems of large dimensions.

eess.SY

Robust Plan Execution with Unexpected Observations

In order to ensure the robust actuation of a plan, execution must be adaptable to unexpected situations in the world and to exogenous events. This is critical in domains in which committing to a wrong ordering of actions can cause the plan failure, even when all the actions succeed. We propose an approach to the execution of a task plan that permits some adaptability to unexpected observations of the state while maintaining the validity of the plan through online reasoning. Our approach computes an adaptable, partially-ordered plan from a given totally-ordered plan. The partially-ordered plan is adaptable in that it can exploit beneficial differences between the world and what was expected. The approach is general in that it can be used with any task planner that produces either a totally or a partially-ordered plan. We propose a plan execution algorithm that computes online the complete set of valid totally-ordered plans described by an adaptable partially-ordered plan together with the probability of success for each of them. This set is then used to choose the next action to execute.

cs.RO

Towards Efficient Anytime Computation and Execution of Decoupled Robustness Envelopes for Temporal Plans

One of the major limitations for the employment of model-based planning and scheduling in practical applications is the need of costly re-planning when an incongruence between the observed reality and the formal model is encountered during execution. Robustness Envelopes characterize the set of possible contingencies that a plan is able to address without re-planning, but their exact computation is extremely expensive; furthermore, general robustness envelopes are not amenable for efficient execution. In this paper, we present a novel, anytime algorithm to approximate Robustness Envelopes, making them scalable and executable. This is proven by an experimental analysis showing the efficiency of the algorithm, and by a concrete case study where the execution of robustness envelopes significantly reduces the number of re-plannings.

cs.AI

Temporal Planning with Intermediate Conditions and Effects

Automated temporal planning is the technology of choice when controlling systems that can execute more actions in parallel and when temporal constraints, such as deadlines, are needed in the model. One limitation of several action-based planning systems is that actions are modeled as intervals having conditions and effects only at the extremes and as invariants, but no conditions nor effects can be specified at arbitrary points or sub-intervals. In this paper, we address this limitation by providing an effective heuristic-search technique for temporal planning, allowing the definition of actions with conditions and effects at any arbitrary time within the action duration. We experimentally demonstrate that our approach is far better than standard encodings in PDDL 2.1 and is competitive with other approaches that can (directly or indirectly) represent intermediate action conditions or effects.

cs.AI

The xSAP Safety Analysis Platform

This paper describes the xSAP safety analysis platform. xSAP provides several model-based safety analysis features for finite- and infinite-state synchronous transition systems. In particular, it supports library-based definition of fault modes, an automatic model extension facility, generation of safety analysis artifacts such as Dynamic Fault Trees (DFTs) and Failure Mode and Effects Analysis (FMEA) tables. Moreover, it supports probabilistic evaluation of Fault Trees, failure propagation analysis using Timed Failure Propagation Graphs (TFPGs), and Common Cause Analysis (CCA). xSAP has been used in several industrial projects as verification back-end, and is currently being evaluated in a joint R&D Project involving FBK and The Boeing Company.

cs.SE

Dynamical Phase Transitions and Instabilities in Open Atomic Many-Body Systems

We discuss an open driven-dissipative many-body system, in which the competition of unitary Hamiltonian and dissipative Liouvillian dynamics leads to a nonequilibrium phase transition. It shares features of a quantum phase transition in that it is interaction driven, and of a classical phase transition, in that the ordered phase is continuously connected to a thermal state. Within a generalized Gutzwiller approach which includes the description of mixed state density matrices, we characterize the complete phase diagram and the critical behavior at the phase transition approached as a function of time. We find a novel fluctuation induced dynamical instability, which occurs at long wavelength as a consequence of a subtle dissipative renormalization effect on the speed of sound.

cond-mat.quant-gas

Universal rates for reactive ultracold polar molecules in reduced dimensions

Analytic expressions describe universal elastic and reactive rates of quasi-two-dimensional and quasi-one-dimensional collisions of highly reactive ultracold molecules interacting by a van der Waals potential. Exact and approximate calculations for the example species of KRb show that stability and evaporative cooling can be realized for spin-polarized fermions at moderate dipole and trapping strength, whereas bosons or unlike fermions require significantly higher dipole or trapping strengths.

physics.atom-ph

Structure and melting behavior of classical bilayer crystals of dipoles

We study the structure and melting of a classical bilayer system of dipoles, in a setup where the dipoles are oriented perpendicular to the planes of the layers and the density of dipoles is the same in each layer. Due to the anisotropic character of the dipole-dipole interactions, we find that the ground-state configuration is given by two hexagonal crystals positioned on top of each other, independent of the interlayer spacing and dipolar density. For large interlayer distances these crystals are independent, while in the opposite limit of small interlayer distances the system behaves as a two-dimensional crystal of paired dipoles. Within the harmonic approximation for the phonon excitations, the melting temperature of these crystalline configurations displays a non-monotonic dependence on the interlayer distance, which is associated with a re-entrant melting behavior in the form of solid-liquid-solid-liquid transitions at fixed temperature.

cond-mat.other

Designing spin-1 lattice models using polar molecules

We describe how to design a large class of always on spin-1 interactions between polar molecules trapped in an optical lattice. The spin degrees of freedom correspond to the hyperfine levels of a ro-vibrational ground state molecule. Interactions are induced using a microwave field to mix ground states in one hyperfine manifold with the spin entangled dipole-dipole coupled excited states. Using multiple fields anistropic models in one, two, or three dimensions, can be built with tunable spatial range. An illustrative example in one dimension is the generalized Haldane model, which at a specific parameter has a gapped valence bond solid ground state. The interaction strengths are large compared to decoherence rates and should allow for probing the rich phase structure of strongly correlated systems, including dimerized and gapped phases.

quant-ph