PDDL 2.1 is the community standard for specifications of temporal planning problems, involving actions that have a duration and can overlap in time. Recent work has shown that some modelling features, such as intermediate and conditional effects, can be expressed in PDDL 2.1 by means of specific encodings. At the core of these encodings is a construction that requires two events to happen simultaneously. However, in practice, almost none of the state-space heuristic search planners known in the literature are capable of finding plans exhibiting this required simultaneity, suggesting that the search approach they use is actually incomplete with regards to the official PDDL 2.1 semantics. In this paper, we explore this issue both theoretically and experimentally. On the theoretical side, we define two different notions of required simultaneity, and we isolate which features of the semantics of PDDL 2.1 allow for such behaviors and how to possibly change the semantics to forbid each of them. In particular, we prove that the crucial detail is how the over-all conditions interact with the mutex relation. From these observations we isolate the reason why most search-based planners cannot find plans with required simultaneity, and provide an updated search strategy that recovers semantic completeness at the cost of a larger branching factor which, however, can be suitably pruned thanks to an application of our results. On the experimental side, we compare the proposed search strategies, showing that our pruning criterion allows us to recover semantic completeness without significant overhead.

One of the major techniques to tackle temporal planning problems is heuristic search augmented with a symbolic representation of time in the states. Augmenting the problem with composite actions (macro-actions) is a simple and powerful approach to create "shortcuts" in the search space, at the cost of augmenting the branching factor of the problem and thus the expansion time of a heuristic search planner. Hence, it is of paramount importance to select the right macro-actions and minimize the number of such actions to optimize the planner performance. In this paper, we first discuss a simple, yet powerful, model similar to macro-actions for the case of temporal planning, and we call these macro-events. Then, we present a novel ranking function to extract and select a suitable set of macro-events from a dataset of valid plans. In our ranking approach, we consider an estimation of the hypothetical search space for a blind search including a candidate set of macro-events under four different exploitation schemata. Finally, we experimentally demonstrate that the proposed approach yields a substantial performance improvement for a state-of-the-art temporal planner.

Integrating metric time into Task And Motion Planning (TAMP) is challenging, especially with simultaneous object motion. Existing work focuses on classical and numeric TAMP, not considering deadlines, motions overlapping in time, and other temporal constraints. In this paper, we fill this gap by formalizing Temporal Task and Motion Planning (TTAMP) for multi-object navigation. We propose a novel interleaved planning technique for this problem, which leverages incremental Satisfiability Modulo Theory to ensure efficient reasoning on deadlines and action duration coupled with a motion planner supporting simultaneous object motion. Geometric data on encountered obstacles prunes unreachable symbolic regions, while temporal bounds limit the geometric search space. For multiple moving objects, our algorithm contextualizes the conflicts learned from the motion planner on overlapping actions so that entire classes of temporal plans are pruned from the search space of the task planner, ensuring the eventual termination of the interplay. We provide a comprehensive benchmark suite and demonstrate the effectiveness of our solver in leveraging these scenarios.

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.

Learning domain knowledge from small training problems to improve planning performance on arbitrarily sized problems is a highly active research area. Many works explored the use of macro-actions to create “shortcuts” in the search space, at the cost of increasing the branching factor of the problem. In temporal planning, a recent technique proposes to equip a heuristic-search temporal planner with selected “macro-events”: a “shortcut” mechanism similar to macro-actions but with state-dependent semantics. In this paper, we generalize macro-events to a lifted representation, making them independent of specific problem objects. We devise a fully automated framework that, given a domain and a collection of small training problems, constructs and selects a suitable set of lifted macro-events. We define a learning pipeline that mixes the optimization of the statistical expectation on an abstraction of the problem with an empirical refinement of the selection on a validation set. We experimentally show that the proposed approach scales to complex problems, yielding substantial improvements over the baseline.

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.

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.

The Platform-Aware Mission Planning (PAMP) problem, formalizes the relationship between an automated temporal planning problem and an execution platform modeled as a Timed Automaton. The PAMP problem consists in finding a valid plan that guarantees the plan executability and the satisfaction of a safety property on the platform, regardless of non-determinism. In this paper, we significantly generalize the PAMP problem along three directions. First, we consider platforms represented as infinite state timed transition systems (TTSs), allowing a more natural and expressive modeling of realistic systems. Second, we introduce a new feature to model relations between the fluents of the planning problem and the platform variables. Finally, we generalize the semantics to cope with unbounded traces. We define a solution method for the resulting generalized PAMP, combining an automated temporal planner and an infinite-state model-checker. Our method is largely more efficient than the existing approach for bounded PAMP problems, despite being strictly more expressive.

Given the model of a system with explicit temporal constraints, optimal temporal planning is the problem of finding a schedule of actions that achieves a certain goal while optimizing an objective function. Recent approaches for optimal planning reduce the problem to a series of queries to an Optimization Modulo Theory (OMT) solver: each query encodes a bounded version of the problem, with additional abstract actions representing an over-approximation of the plans beyond the bound. This technique suffers from performance issues, mainly due to the looseness of the over-approximation, which can include many non-executable plans. In this paper, we propose a refined abstraction for solving optimal temporal planning via OMT by introducing abstract scheduling constraints, which have a double purpose. First, they enforce a partial ordering of abstract actions based on mutual dependencies between them, which leads to a better makespan estimation and allows to prove optimality sooner. Second, they implicitly forbid circular self-enabling of abstract actions, which is a common cause of spurious models that severely affects performance in existing approaches. We prove the soundness and completeness of the resulting approach and empirically demonstrate its superiority with respect to the state of the art.

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.

International audience

Temporal Planning is the problem of synthesizing a course of actions given a predictive model of a system subject to temporal constraints. This kind of planning finds natural applications in the automation of industrial processes and in robotics when the timing and deadlines are important. Finding any plan in temporal planning is often not enough as it is sometimes needed to optimize a certain objective function: particularly interesting are the minimization of the makespan and the optimization of the costs of actions. Despite the importance of the problem, only few works in the literature tackled the problem of optimal temporal planning because of the complicated intermix of planning and scheduling. In this paper, we address the problem of optimal temporal planning for a very expressive class of problems using a reduction of the bounded planning problem to Optimization Modulo Theory (OMT) a powerful discrete/continuous optimization framework. We theoretically and empirically show the expressive power of this approach and we set a baseline for future research in this area.

The field of Temporal Planning (TP) is receiving increasing interest for its many real-world applications. Most of the literature focuses on the TP problem of finding a plan, with algorithms that are not guaranteed to terminate when the problem admits no solution. In this paper, we present sound and complete decision procedures that address the dual problem of proving that no plan exists, which has important applications in oversubscription, model validation and optimization. We focus on the expressive and practically relevant semantics of action non-self-overlapping, recently proved to be PSPACE-complete. For this subclass, we propose two approaches: a reduction of the planning problem to model-checking of Timed Transition Systems, and a heuristic-search algorithm where temporal constraints are represented by Difference Bound Matrices. We implemented the approaches, and carried out an experimental evaluation against other state-of-the-art TP tools. On benchmarks that admit no plans, both approaches dramatically outperform the other planners, while the heuristic-search algorithm remains competitive on solvable benchmarks.

In this paper, we study the computational complexity of action-based temporal planning interpreted over dense time. When time is assumed to be discrete, the problem is known to be EXPSPACE-complete. However, the official PDDL 2.1 semantics and many implementations interpret time as a dense domain. This work provides several results about the complexity of the problem, focusing on some particularly interesting cases: whether a minimum amount ε of separation between mutually exclusive events is given, in contrast to the separation being simply required to be non-zero, and whether or not actions are allowed to overlap already running instances of themselves. We prove the problem to be PSPACE-complete when self-overlap is forbidden, whereas, when it is allowed, it becomes EXPSPACE-complete with ε-separation and even undecidable with non-zero separation. These results clarify the computational consequences of different choices in the definition at the core of the PDDL 2.1 semantics, which have been vague until now.1

Automated temporal planning is the problem of synthesizing, starting from a model of a system, a course of actions to achieve a desired goal when temporal constraints, such as deadlines, are present in the problem. Despite considerable successes in the literature, scalability is still a severe limitation for existing planners, especially when confronted with real-world, industrial scenarios. In this paper, we aim at exploiting recent advances in reinforcement learning, for the synthesis of heuristics for temporal planning. Starting from a set of problems of interest for a specific domain, we use a customized reinforcement learning algorithm to construct a value function that is able to estimate the expected reward for as many problems as possible. We use a reward schema that captures the semantics of the temporal planning problem and we show how the value function can be transformed in a planning heuristic for a semi-symbolic heuristic search exploration of the planning model. We show on two case-studies how this method can widen the reach of current temporal planners with encouraging results.

Max-Plus Linear (MPL) systems are an algebraic formalism with practical applications in transportation networks, manufacturing and biological systems. MPL systems can be naturally modeled as infinite-state transition systems, and exhibit interesting structural properties (e.g. periodicity or steady state), for which analysis methods have been recently proposed. In this paper, we tackle the open problem of specifying and analyzing user-defined temporal properties for MPL systems. 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 propose a family of specialized algorithms leveraging the periodic behaviour of an MPL system. We prove soundness and completeness, showing that the transient and cyclicity of the MPL system induce a completeness threshold for the verification problem. The algorithms are cast in the setting of SMT-based verification of infinite-state transition systems over the reals, with variants depending on the (incremental vs upfront) computation of the bound, and on the (explicit vs implicit) unrolling of the transition relation. Our comprehensive experiments show that the proposed techniques can be applied to MPL systems of large dimensions and on general TDLTL formulae, with remarkable performance gains against a dedicated abstraction-based technique and a translation to the nuXmv symbolic model checker.

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 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.

The robust execution of a temporal plan in a perturbed environment is a problem that remains to be solved. Perturbed environments, such as the real world, are non-deterministic and filled with uncertainty. Hence, the execution of a temporal plan presents several challenges and the employed solution often consists of replanning when the execution fails. In this paper, we propose a novel algorithm, named Olisipo, which aims to maximise the probability of a successful execution of a temporal plan in perturbed environments. To achieve this, a probabilistic model is used in the execution of the plan, instead of in the building of the plan. This approach enables Olisipo to dynamically adapt the plan to changes in the environment. In addition to this, the execution of the plan is also adapted to the probability of successfully executing each action. Olisipo was compared to a simple dispatcher and it was shown that it consistently had a higher probability of successfully reaching a goal state in uncertain environments, performed fewer replans and also executed fewer actions. Hence, Olisipo offers a substantial improvement in performance for disturbed environments.

This paper studies the computational complexity of temporal planning, as represented by PDDL 2.1, interpreted over dense time. When time is considered discrete, the problem is known to be EXPSPACE-complete. However, the official PDDL 2.1 semantics, and many implementations, interpret time as a dense domain. This work provides several results about the complexity of the problem, studying a few interesting cases: whether a minimum amount ϵ of separation between mutually exclusive events is given, in contrast to the separation being simply required to be non-zero, and whether or not actions are allowed to overlap already running instances of themselves. We prove the problem to be PSPACE-complete when self-overlap is forbidden, whereas, when allowed, it becomes EXPSPACE-complete with ϵ-separation and undecidable with non-zero separation. These results clarify the computational consequences of different choices in the definition of the PDDL 2.1 semantics, which were vague until now.

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.

To achieve practical execution, planners must produce temporal plans with some degree of run-time adaptability. Such plans can be expressed as Simple Temporal Networks (STN), that constrain the timing of action activations, and implicitly represent the space of choices for the plan executor.A first problem is to verify that all the executor choices allowed by the STN plan will be successful, i.e. the plan is valid. An even more important problem is to assess the effect of discrepancies between the model used for planning and the execution environment.We propose an approach to compute the “robustness envelope” (i.e., alternative action durations or resource consumption rates) of a given STN plan, for which the plan remains valid. Plans can have boolean and numeric variables as well as discrete and continuous change. We leverage Satisfiability Modulo Theories (SMT) to make the approach formal and practical.

In several industrial applications of planning, complex temporal metric trajectory constraints are needed to adequately model the problem at hand. For example, in production plants, items must be processed following a “recipe” of steps subject to precise timing constraints. Modeling such domains is very challenging in existing action-based languages due to the lack of sufficiently expressive trajectory constraints.We propose a novel temporal planning formalism allowing quantified temporal constraints over execution timing of action instances. We build on top of instantaneous actions borrowed from classical planning and add expressive temporal constructs. The paper details the semantics of our new formalism and presents a solving technique grounded in classical, heuristic forward search planning. Our experiments prove the proposed framework superior to alternative state-of-theart planning approaches on industrial benchmarks, and competitive with similar solving methods on well known benchmarks took from the planning competition.

Temporal planning is an active research area of Artificial Intelligence because of its many applications ranging from roboticsto logistics and beyond. Traditionally, authors focused on theautomatic synthesis of plans given a formal representation of thedomain and of the problem. However, the effectiveness of suchtechniques is limited by the complexity of the modeling phase: it ishard to produce a correct model for the planning problem at hand. In this paper, we present a technique to simplify the creation ofcorrect models by leveraging formal-verification tools for automaticvalidation. We start by using the ANML language, a very expressivelanguage for temporal planning problems that has been recentlypresented. We chose ANML because of its usability andreadability. Then, we present a sound-and-complete, formal encodingof the language into Linear Temporal Logic over predicates withinfinite-state variables. Thanks to this reduction, we enable theformal verification of several relevant properties over the planningproblem, providing useful feedback to the modeler.

The Temporal Network with Uncertainty (TNU) modeling framework is used to represent temporal knowledge in presence of qualitative temporal uncertainty. Dynamic Controllability (DC) is the problem of deciding the existence of a strategy for scheduling the controllable time points of the network observing past happenings only. In this paper, we address the DC problem for a very general class of TNU, namely Disjunctive Temporal Network with Uncertainty. We make the following contributions. First, we define strategies in the form of an executable language; second, we propose the first decision procedure to check whether a given strategy is a solution for the DC problem; third we present an efficient algorithm for strategy synthesis based on techniques derived from Timed Games and Satisfiability Modulo Theory. The experimental evaluation shows that the approach is superior to the state-of-the-art.

Timed Failure Propagation Graphs (TFPGs) are a formalism used in industry to describe failure propagation in a dynamic partially observable system. TFPGs are commonly used to perform model-based diagnosis. As in any model-based diagnosis approach, however, the quality of the diagnosis strongly depends on the quality of the model. Approaches to certify the quality of the TFPG are limited and mainly rely on testing. In this work we address this problem by leveraging efficient Satisfiability Modulo Theories (SMT) engines to perform exhaustive reasoning on TFPGs. We apply model-checking techniques to certify that a given TFPG satisfies (or not) a property of interest. Moreover, we discuss the problem of refinement and diagnosability testing and empirically show that our technique can be used to efficiently solve them.

In many practical domains, planning systems are required to reason about durative actions. A common assumption in the literature is that the executor is allowed to decide the duration of each action. However, this assumption may be too restrictive for applications. In this paper, we tackle the problem of temporal planning with uncontrollable action durations. We show how to generate robust plans,that guarantee goal achievement despite the uncontrollability of the actual duration of the actions. We extend the state-space temporalplanning framework, integrating recent techniques for solving temporalproblems under uncertainty. We discuss different ways of lifting the total order plans generated by the heuristic search to partial orderplans, showing (in)completeness results for each of them. We implemented our approach on top of COLIN, a state-of-the-art planner. An experimental evaluation over several benchmark problems shows the practical feasibility of the proposed approach.

The framework of temporal problems with uncertainty (TPU) is useful to express temporal constraints over a set of activities subject to uncertain (and uncontrollable) duration. In this work, we focus on the most general class of TPU, namely disjunctive TPU (DTPU), and consider the case of weak controllability, that allows one to model problems arising in practical scenarios (e.g. on-line scheduling). We first tackle the decision problem, i.e. whether there exists a schedule of the activities that, depending on the uncertainty, satisfies all the constraints. We propose a logical approach, based on the reduction to a problem of Satisfiability Modulo Theories (SMT), in the theory of Linear Real Arithmetic with Quantifiers. This results in the first implemented solver for weak controllability of DTPUs. Then, we tackle the problem of synthesizing control strategies for scheduling the activities. We focus on strategies that are amenable for efficient execution. We prove that linear strategies are not always sufficient, even in the sub-case of simple TPU (STPU), while piecewise-linear strategies, that are multiple conditionally-applied linear strategies, are always sufficient. We present several algorithms for the synthesis of linear and piecewise-linear strategies, in case of STPU and of DTPU. All the algorithms are implemented on top of SMT solvers. We provide experimental evidence of the scalability of the proposed techniques, with dramatic speed-ups in strategy execution compared to on-line reasoning.

A Simple Temporal Network with Uncertainty (STNU) is a structure for representing and reasoning about temporal constraints in domains where some temporal durations are not controlled by the executor. The most important property of an STNU is whether it is dynamically controllable (DC) whether there exists a strategy for executing the controllable time-points that guarantees that all constraints will be satisfied no matter how the uncontrollable durations turn out. This paper provides a novel mapping from STNUs to Timed Game Automata (TGAs) that: (1) explicates the deep theoretical relationships between STNUs and TGAs; and (2) enables the memoryless strategies generated from the TGA to be transformed into equivalent STNU execution strategies that reduce the real-time computational burden for the executor. The paper formally proves that the STNU-to-TGA encoding properly captures the execution semantics of STNUs.

Temporal networks are data structures for representing and reasoning about temporal constraints on activities. Many kinds of temporal networks have been defined in the literature, differing in their expressiveness. The simplest kinds of networks have polynomial algorithms for determining their consistency or controllability, but corresponding algorithms for more expressive networks (e.g., Those that include observation nodes or disjunctive constraints) have so far been unavailable. However, recent work has introduced a new approach to such algorithms based on translating temporal networks into Timed Game Automata (TGAs) and then using off-the-shelf software to synthesize execution strategies -- or determine that none exist. So far, that approach has only been used on Simple Temporal Networks with Uncertainty, for which polynomial algorithms already exist. This paper extends the temporal-network-to-TGA approach to accommodate observation nodes and disjunctive constraints. Insodoing the paper presents, for the first time, sound and complete algorithms for checking the dynamic controllability of these more expressive networks. The translations also highlight the theoretical relationships between various kinds of temporal networks and the TGA model. The new algorithms have immediate applications in the workflow models being developed to automate business processes, including in the health-care domain.

Timelines are a formalism to model planning domains where the temporal aspects are predominant, and have been used in many real-world applications. Despite their practical success, a major limitation is the inability to model temporal uncertainty, i.e. the plan executor cannot decide the duration of some activities.In this paper we make two key contributions. First, we propose a comprehensive, semantically well founded framework that (conservatively) extends with temporal uncertainty the state of the art timeline approach. Second, we focus on the problem of producing time-triggered plans that are robust with respect to temporal uncertainty, under a bounded horizon. In this setting, we present the first complete algorithm, and we show how it can be made practical by leveraging the power of Satisfiability Modulo Theories.

Temporal problems with uncertainty are a well established formalism to model time constraints of a system interacting with an uncertain environment. Several works have addressed the definition and the solving of controllability problems, and three degrees of controllability have been proposed: weak, strong, and dynamic. In this work we focus on weak controllability: we address both the decision and the strategy extraction problems. Extracting a strategy means finding a function from assignments to uncontrollable time points to assignments to controllable time points that fulfills all the temporal constraints. We address the two problems in the satisfiability modulo theory framework. We provide a clean and complete formalization of the problems, and we propose novel techniques to extract strategies. We also provide experimental evidence of the scalability and efficiency of the proposed techniques.

We present the EuRailCheck tool, which supports the formalization and the validation of requirements, based on the use of formal methods. The tool allows the user to analyze the requirements in natural language and to categorize and structure them. It allows to formalize the requirements into a subset of UML enriched with static and temporal constraints for which we defined a formal semantics. Finally, the tool allows to apply model checking techniques specialized for the validation of formal requirements. The tool has been developed and validated within a project funded by the European Railway Agency for the validation of the European Train Control System specification. By now, the tool has been successfully used by about thirty railway experts of different companies.