Alessandro Cimatti

I&C Journal 2026 Journal Article

Multiple interdependent Simple Temporal Networks with Uncertainty: A semi-decentralized multi-agent model with shared control of activity durations

• Ajdin SUMIC
• Thierry Vidal
• Andrea Micheli
• Alessandro Cimatti

Simple Temporal Networks with Uncertainty are a powerful and widely used formalism for representing and reasoning over convex temporal constraints, when some of them are subject to uncertainty. Since their introduction, they have been used in planning and scheduling applications to model situations where some agent acting in the real world does not control some activity durations or event timings, which are called contingent constraints. Depending on when uncertainties are revealed, one needs now to check the Weak, Dynamic or Strong controllability of the network, i. e. , that there is a valid execution strategy, whatever the values of the contingent constraints. This paper proposes for the first time a semantic characterization of the possible extensions to multi-agent settings and reviews previous approaches that tried to address such topics, in order to thoroughly introduce a new type of multi-agent collaborative model, where, as opposed to previous works, each agent manages its own separate STNU, and the control over activity durations is shared among the agents: what is called here a contract is a mutual constraint controllable for some agent and contingent for others. We introduce the cSTNU, a semantically enriched version of an STNU, a set of cSTNUs forming the global Multiple Interdependent STNUs model. Then, controllability issues are revisited, and a new problem called the Repair problem is introduced, which goal is to find how to regain failed controllability by shrinking some of the shared contract durations. In this paper, we also propose the very first SMT-based centralized algorithms that are able to solve both the Weak and Strong repair problems, supported by detailed experimentation with different SMT solvers. We finally discuss why that first approach remains limited in terms of scalability, and suggest some promising alternatives to design more effective methods, both paving the way towards a Dynamic repair solving method and distributed algorithms.

KR Conference 2025 Conference Paper

Generalizing Platform-Aware Mission Planning for Infinite-State Timed Transition Systems

• Stefan Panjkovic
• Alessandro Cimatti
• Andrea Micheli
• Stefano Tonetta

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.

ECAI Conference 2024 Conference Paper

A Lazy Approach to Neural Numerical Planning with Control Parameters

• René Heesch
• Alessandro Cimatti
• Jonas Ehrhardt
• Alexander Diedrich
• Oliver Niggemann

In this paper, we tackle the problem of planning in complex numerical domains, where actions are indexed by control parameters, and their effects may be described by neural networks. We propose a lazy, hierarchical approach based on two ingredients. First, a Satisfiability Modulo Theory solver looks for an abstract plan where the neural networks in the model are abstracted into uninterpreted functions. Then, we attempt to concretize the abstract plan by querying the neural network to determine the control parameters. If the concretization fails and no valid control parameters could be found, suitable information to refine the abstraction is lifted to the Satisfiability Modulo Theory model. We contrast our work against the state of the art in NN-enriched numerical planning, where the neural network is eagerly and exactly represented as terms in Satisfiability Modulo Theories over nonlinear real arithmetic. Our systematic evaluation on four different planning domains shows that avoiding symbolic reasoning about the neural network not only leads to substantial efficiency improvements, but also enables their integration as black-box models.

TIME Conference 2024 Conference Paper

Introducing Interdependent Simple Temporal Networks with Uncertainty for Multi-Agent Temporal Planning

• Aïdin Sumic
• Thierry Vidal
• Andrea Micheli
• Alessandro Cimatti

Simple Temporal Networks with Uncertainty are a powerful and widely used formalism for representing and reasoning over convex temporal constraints in the presence of uncertainty called contingent constraints. Since their introduction, they have been used in planning and scheduling applications to model situations where the scheduling agent does not control some activity durations or event timings. What needs to be checked is then the controllability of the network, i. e. , that there is a valid execution strategy whatever the values of the contingents. This paper considers a new type of multi-agent extension, where, as opposed to previous works, each agent manages its own separate STNU, and the control over activity durations is shared among the agents: what is called here a contract is a mutual constraint controllable for some agent and contingent for others. We will propose a semantically enriched version of STNUs that will be composed into a global Multi-agent Interdependent STNUs model. Then, controllability issues will be revisited, and we will focus on the repair problem, i. e. , how to regain failed controllability by shrinking some of the shared contract durations, here in a centralized manner.

AAAI Conference 2022 Conference Paper

Deciding Unsolvability in Temporal Planning under Action Non-Self-Overlapping

• Stefan Panjkovic
• Andrea Micheli
• Alessandro Cimatti

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

AIJ Journal 2022 Journal Article

Diagnosability of fair transition systems

• Benjamin Bittner
• Marco Bozzano
• Alessandro Cimatti
• Marco Gario
• Stefano Tonetta
• Viktoria Vozarova

The integrity of complex dynamic systems often relies on the ability to detect, during operation, the occurrence of faults, or, in other words, to diagnose the system. The feasibility of this task, also known as diagnosability, depends on the nature of the system dynamics, the impact of faults, and the availability of a suitable set of sensors. Standard techniques for analyzing the diagnosability problem rely on a model of the system and on proving the absence of a faulty trace that cannot be distinguished by a non-faulty one (this pair of traces is called critical pair). In this paper, we tackle the problem of verifying diagnosability under the presence of fairness conditions. These extend the expressiveness of the system models enabling the specification of assumptions on the system behavior such as the infinite occurrence of observations and/or faults. We adopt a comprehensive framework that encompasses fair transition systems, temporally extended fault models, delays between the occurrence of a fault and its detection, and rich operational contexts. We show that in presence of fairness the definition of diagnosability has several interesting variants, and discuss the relative strengths and the mutual relationships. We prove that the existence of critical pairs is not always sufficient to analyze diagnosability, and needs to be generalized to critical sets. We define new notions of critical pairs, called ribbon-shape, with special looping conditions to represent the critical sets. Based on these findings, we provide algorithms to prove the diagnosability under fairness. The approach is built on top of the classical twin plant construction, and generalizes it to cover the various forms of diagnosability and find sufficient delays. The proposed algorithms are implemented within the xSAP platform for safety analysis, leveraging efficient symbolic model checking primitives. An experimental evaluation on a heterogeneous set of realistic benchmarks from various application domains demonstrates the effectiveness of the approach.

I&C Journal 2022 Journal Article

LTL falsification in infinite-state systems

• Alessandro Cimatti
• Alberto Griggio
• Enrico Magnago

In finite-state systems, if an LTL property is false, there is always a counterexample path (i. e. a witness) for it which is ultimately periodic (i. e. in a lasso-shaped form). When dealing with infinite-state systems, this is no longer the case. In this work, we address this issue by proposing an automatic approach that presents witnesses in an indirect way. The approach is based on two key insights. First, we leverage the notion of well-founded funnel, where a ranking function ensures that the states in the source set are guaranteed to inevitably reach the destination set. We show that, under suitable conditions, a sequence of funnels ensures the existence of a fair path. Second, we adopt a compositional approach to partition the original system into projections and to prove that they result in a non-empty under-approximation of the original system that only contains fair paths. Then, we propose an algorithm that, working in an abstract space induced by a set of predicates, identifies candidate funnels, proves their well-foundedness, and searches for a sequencing order. We experimentally evaluate the approach on examples taken from software, timed and hybrid systems, showing its wide applicability and expressiveness, with an implementation that outperforms various competitor tools.

TIST Journal 2021 Journal Article

A Comprehensive Approach to On-board Autonomy Verification and Validation

• Marco Bozzano
• Alessandro Cimatti
• Marco Roveri

Deep space missions are characterized by severely constrained communication links. To meet the needs of future missions and increase their scientific return, future space systems will require an increased level of autonomy on-board. In this work, we propose a comprehensive approach to on-board autonomy. We rely on model-based reasoning, and we consider many important (on-line and off-line) reasoning capabilities such as plan generation, validation, execution and monitoring, runtime diagnosis, and fault detection, identification, and recovery. The controlled platform is represented symbolically, and the reasoning capabilities are seen as symbolic manipulation of such formal model. We have developed a prototype of our framework, and we have integrated it within an on-board Autonomous Reasoning Engine. Finally, we have evaluated our approach on three case-studies inspired by real-world projects and characterized it in terms of reliability, availability, and performance.

TIME Conference 2021 Conference Paper

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

• Michael Cashmore
• Alessandro Cimatti
• Daniele Magazzeni
• Andrea Micheli
• Parisa Zehtabi

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.

GandALF Workshop 2021 Workshop Paper

Expressiveness of Extended Bounded Response LTL

• Alessandro Cimatti
• Luca Geatti
• Nicola Gigante
• Angelo Montanari
• Stefano Tonetta

Extended Bounded Response LTL with Past (LTLEBR+P) is a safety fragment of Linear Temporal Logic with Past (LTL+P) that has been recently introduced in the context of reactive synthesis. The strength of LTLEBR+P is a fully symbolic compilation of formulas into symbolic deterministic automata. Its syntax is organized in four levels. The first three levels feature (a particular combination of) future temporal modalities, the last one admits only past temporal operators. At the base of such a structuring there are algorithmic motivations: each level corresponds to a step of the algorithm for the automaton construction. The complex syntax of LTLEBR+P made it difficult to precisely characterize its expressive power, and to compare it with other LTL+P safety fragments. In this paper, we first prove that LTLEBR+P is expressively complete with respect to the safety fragment of LTL+P, that is, any safety language definable in LTL+P can be formalized in LTLEBR+P, and vice versa. From this, it follows that LTLEBR+P and Safety-LTL are expressively equivalent. Then, we show that past modalities play an essential role in LTLEBR+P: we prove that the future fragment of LTLEBR+P is strictly less expressive than full LTLEBR+P.

I&C Journal 2020 Journal Article

SMT-based satisfiability of first-order LTL with event freezing functions and metric operators

• Alessandro Cimatti
• Alberto Griggio
• Enrico Magnago
• Marco Roveri
• Stefano Tonetta

In this paper, we propose to extend First-Order Linear-time Temporal Logic with Past adding two operators “at next” and “at last”, which take in input a term and a formula and return the value of the term at the next state in the future or last state in the past in which the formula holds. The new logic, named LTL-EF, can be interpreted with different models of time (including discrete, dense, and super-dense time) and with different first-order theories (à la Satisfiability Modulo Theories (SMT)). We show that the “at next” and “at last” can encode (first-order) MTL 0, ∞ with counting. We provide rewriting procedures to reduce the satisfiability problem to the discrete-time case (to leverage on the mature state-of-the-art corresponding verification techniques) and to remove the extra functional symbols. We implemented these techniques in the nuXmv model checker enabling the analysis of LTL-EF and MTL 0, ∞ based on SMT-based model checking. We show the feasibility of the approach experimenting with several non-trivial valid and satisfiable formulas.

AAAI Conference 2020 Conference Paper

Temporal Planning with Intermediate Conditions and Effects

• Alessandro Valentini
• Andrea Micheli
• Alessandro Cimatti

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.

AAAI Conference 2019 Conference Paper

Robustness Envelopes for Temporal Plans

• Michael Cashmore
• Alessandro Cimatti
• Daniele Magazzeni
• Andrea Micheli
• Parisa Zehtabi

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.

SAT Conference 2018 Conference Paper

Experimenting on Solving Nonlinear Integer Arithmetic with Incremental Linearization

• Alessandro Cimatti
• Alberto Griggio
• Ahmed Irfan
• Marco Roveri
• Roberto Sebastiani

Abstract Incremental linearization is a conceptually simple, yet effective, technique that we have recently proposed for solving SMT problems over nonlinear real arithmetic constraints. In this paper, we show how the same approach can be applied successfully also to the harder case of nonlinear integer arithmetic problems. We describe in detail our implementation of the basic ideas inside the MathSAT SMT solver, and evaluate its effectiveness with an extensive experimental analysis over all nonlinear integer benchmarks in SMT-LIB. Our results show that MathSAT is very competitive with (and often outperforms) state-of-the-art SMT solvers based on alternative techniques.

AIJ Journal 2018 Journal Article

Strong temporal planning with uncontrollable durations

• Alessandro Cimatti
• Minh Do
• Andrea Micheli
• Marco Roveri
• David E. Smith

Planning in real world domains often involves modeling and reasoning about the duration of actions. Temporal planning allows such modeling and reasoning by looking for plans that specify start and end time points for each action. In many practical cases, however, the duration of actions may be uncertain and not under the full control of the executor. For example, a navigation task may take more or less time, depending on external conditions such as terrain or weather. In this paper, we tackle the problem of strong temporal planning with uncontrollable action durations (STPUD). For actions with uncontrollable durations, the planner is only allowed to choose the start of the actions, while the end is chosen, within known bounds, by the environment. A solution plan must be robust with respect to all uncontrollable action durations, and must achieve the goal on all executions, despite the choices of the environment. We propose two complementary techniques. First, we discuss a dedicated planning method, that generalizes the state-space temporal planning framework, leveraging SMT-based techniques for temporal networks under uncertainty. Second, we present a compilation-based method, that reduces any STPUD problem to an ordinary temporal planning problem. Moreover, we investigate a set of sufficient conditions to simplify domains by removing some of the uncontrollability. We implemented both our approaches, and we experimentally evaluated our techniques on a large number of instances. Our results demonstrate the practical applicability of the two techniques, which show complementary behavior.

AAAI Conference 2017 Conference Paper

Validating Domains and Plans for Temporal Planning via Encoding into Infinite-State Linear Temporal Logic

• Alessandro Cimatti
• Andrea Micheli
• Marco Roveri

Temporal planning is an active research area of Artificial Intelligence because of its many applications ranging from robotics to logistics and beyond. Traditionally, authors focused on the automatic synthesis of plans given a formal representation of the domain and of the problem. However, the effectiveness of such techniques is limited by the complexity of the modeling phase: it is hard to produce a correct model for the planning problem at hand. In this paper, we present a technique to simplify the creation of correct models by leveraging formal-verification tools for automatic validation. We start by using the ANML language, a very expressive language for temporal planning problems that has been recently presented. We chose ANML because of its usability and readability. Then, we present a soundand-complete, formal encoding of the language into Linear Temporal Logic over predicates with infinite-state variables. Thanks to this reduction, we enable the formal verification of several relevant properties over the planning problem, providing useful feedback to the modeler.

AAMAS Conference 2016 Conference Paper

A Lazy Approach to Temporal Epistemic Logic Model Checking

• Alessandro Cimatti
• Marco Gario
• Stefano Tonetta

Temporal Epistemic Logic is used to reason about the evolution of knowledge over time. A notable example is the temporal epistemic logic KL1, which is used to model what a reasoner can infer about the state of a dynamic system by using available observations. Applications of KL1 span from security (verification of cryptography protocols and information flow) to diagnostic systems (fault detection and diagnosability). In this paper, we tackle the verification of KL1 properties under observational semantics, by proposing an effective approach that is able to deal with both finite and infinite state systems. The denotation of the epistemic atoms is computed in a lazy way, driven by the counter-examples obtained from model checking an abstraction of the property. We analyze the approach on a comprehensive set of finite- and infinite-state benchmarks from the literature, evaluate the effectiveness of various optimizations, and demonstrate that our approach outperforms existing approaches.

IJCAI Conference 2016 Conference Paper

Automated Synthesis of Timed Failure Propagation Graphs

• Benjamin Bittner
• Marco Bozzano
• Alessandro Cimatti

Timed Failure Propagation Graphs (TFPGs) are used in the design of safety-critical systems as a way of modeling failure propagation, and to evaluate and implement diagnostic systems. TFPGs are mostly produced manually, from a given dynamic system of greater complexity. In this paper we present a technique to automate the construction of TFPGs. It takes as input a set of failure mode and discrepancy nodes and builds the graph on top of them, based on an exhaustive analysis of all system behaviors. The result is a TFPG that accurately represents the sequences of failures and their effects as they appear in the system model. The proposed approach has been implemented on top of state-of-the-art symbolic model-checking techniques, and thoroughly evaluated on a number of synthetic and industrial benchmarks.

AAAI Conference 2016 Conference Paper

Automated Verification and Tightening of Failure Propagation Models

• Benjamin Bittner
• Marco Bozzano
• Alessandro Cimatti
• Gianni Zampedri

Timed Failure Propagation Graphs (TFPGs) are used in the design of safety-critical systems as a way of modeling failure propagation, and to evaluate and implement diagnostic systems. TFPGs are a very rich formalism: they allow to model Boolean combinations of faults and events, also dependent on the operational modes of the system and quantitative delays between them. TFPGs are often produced manually, from a given dynamic system of greater complexity, as abstract representations of the system behavior under specific faulty conditions. In this paper we tackle two key difficulties in this process: first, how to make sure that no important behavior of the system is overlooked in the TFPG, and that no spurious, nonexistent behavior is introduced; second, how to devise the correct values for the delays between events. We propose a model checking approach to automatically validate the completeness and tightness of a TFPG for a given infinite-state dynamic system, and a procedure for the automated synthesis of the delay parameters. The proposed approach is evaluated on a number of synthetic and industrial benchmarks.

AAAI Conference 2016 Conference Paper

Dynamic Controllability of Disjunctive Temporal Networks: Validation and Synthesis of Executable Strategies

• Alessandro Cimatti
• Andrea Micheli
• Marco Roveri

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.

AIJ Journal 2015 Journal Article

An SMT-based approach to weak controllability for disjunctive temporal problems with uncertainty

• Alessandro Cimatti
• Andrea Micheli
• Marco Roveri

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.

I&C Journal 2015 Journal Article

HRELTL: A temporal logic for hybrid systems

• Alessandro Cimatti
• Marco Roveri
• Stefano Tonetta

Hybrid traces are useful to describe behaviors of dynamic systems where continuous and discrete evolutions are combined. The ability to represent sets of traces by means of formulas in temporal logic has recently found important applications in various fields, such as requirements analysis, compositional verification, and contract-based design. In this paper we present HRELTL, a temporal logic to characterize hybrid traces. The logic is highly expressive: it allows the description of continuous behaviors, by expressing mathematical constraints over derivatives, and discrete behaviors, by constraining values of variables across instantaneous transitions. HRELTL combines the power of temporal operators and regular expressions, and enjoys important properties such as sampling invariance. We demonstrate that the satisfiability problem for a fragment of HRELTL allows for a satisfiability-preserving reduction to RELTL(RA), a logic over discrete traces with atoms in non-linear Real Arithmetic for which automated reasoning procedures are being developed.

AAAI Conference 2015 Conference Paper

SMT-Based Validation of Timed Failure Propagation Graphs

• Marco Bozzano
• Alessandro Cimatti
• Marco Gario
• Andrea Micheli

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

AAAI Conference 2015 Conference Paper

Strong Temporal Planning with Uncontrollable Durations: A State-Space Approach

• Alessandro Cimatti
• Andrea Micheli
• Marco Roveri

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 temporal planning framework, integrating recent techniques for solving temporal problems under uncertainty. We discuss different ways of lifting the total order plans generated by the heuristic search to partial order plans, showing (in)completeness results for each of them. We implemented our approach on top of COLIN, a stateof-the-art planner. An experimental evaluation over several benchmark problems shows the practical feasibility of the proposed approach.

TIME Conference 2014 Conference Paper

Sound and Complete Algorithms for Checking the Dynamic Controllability of Temporal Networks with Uncertainty, Disjunction and Observation

• Alessandro Cimatti
• Luke Hunsberger
• Andrea Micheli
• Roberto Posenato
• Marco Roveri

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.

AAAI Conference 2014 Conference Paper

Using Timed Game Automata to Synthesize Execution Strategies for Simple Temporal Networks with Uncertainty

• Alessandro Cimatti
• Luke Hunsberger
• Andrea Micheli
• Marco Roveri

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); that is, 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.

SAT Conference 2013 Conference Paper

A Modular Approach to MaxSAT Modulo Theories

• Alessandro Cimatti
• Alberto Griggio
• Bastiaan Joost Schaafsma
• Roberto Sebastiani

Abstract In this paper we present a novel “modular” approach for (weighted partial) MaxSAT Modulo Theories. The main idea is to combine a lazy SMT solver with a purely-propositional (weighted partial) MaxSAT solver, by making them exchange information iteratively: the former produces an increasing set of theory lemmas which are used by the latter to progressively refine an approximation of the final subset of the soft clauses, which is eventually returned as output. The approach has several practical features. First, it is independent from the theories addressed. Second, it is simple to implement and to update, since both SMT and MaxSAT solvers can be used as blackboxes. Third, it can be interfaced with external MaxSAT and SMT solvers in a plug-and-play manner, so that to benefit for free of tools which are or will be made available. We have implemented our approach on top of the MathSAT5 SMT solver and of a selection of external MaxSAT solvers, and we have evaluated it by means of an extensive empirical test on SMT-LIB benchmarks. The results confirm the validity and potential of this approach.

GandALF Workshop 2013 Invited Paper

Temporal logic satisfiability for the design of complex systems

• Alessandro Cimatti
• Stefano Tonetta

Abstract The development of computer-based dynamic systems is a very hard task. On the one hand, the required functionalities are very complex, and often include inherently contradicting aspects (e. g. moving trains in a railways station versus avoiding crashes). On the other hand, it is required to integrate the continuous dynamics of physical plants with the discrete dynamics in the control modules and procedures. In addition, such systems often carry out critical functions, which calls for rigorous means to support a development process. The use of a formal approach, coupled with suitable reasoning tools, has found its way in several practical domains, such as railways [5], industrial production [20], hardware design [2, 13, 11], and avionics [15]. Most formal approaches focus on a behavioral characterization of a system, possibly expressed as an automaton or network/hierarchy of automata. Model-based approaches build this behavioral model as a result of semantics-preserving transformation of some design language, and use the model to verify the system description. The verification uses some properties, in form of first-order or temporal formulas, which represent the requirements and are typically assumed to be correct. More recently, the role of properties is being recognized as increasingly important. For example, in hardware design, specification languages for properties (e. g. PSL [10], SVA [19]) have been introduced to increase expressive power (augmenting for example Linear-time Temporal Logic (LTL) with regular expressions) and usability (using natural language expressions and maximizing the syntactic sugar). The quality of the assertions expressed with such languages has emerged as a problem leading to the development of specialized techniques for their validation [3, 6]. Interestingly, the same type of problem has been addressed in requirements engineering, across domains, for many years. According to studies sponsored by NASA in 90s, many software bugs in safety-critical embedded systems were due to flaws in requirements [14]. The role of formal methods in finding such errors is becoming more and more important (e. g. , [7]). The role of properties is also fundamental in compositional reasoning [17], where a global verification problem is decomposed into a number of localized problems. Finally, contract based design [18] allows to decompose the properties of the architectural blocks according to the hierarchical system decomposition, before behavioral descriptions are available, and provides a strong support for property-based refinement and reuse of components [9]. In the talk, we explore the role of temporal logic satisfiability in the design of complex systems, focusing on a property-based design, where behaviors of systems are expressed as formulas in temporal logics. We first discuss the challenges resulting in practice from requirements analysis, compositional reasoning, and contract-based design, showing that satisfiability of temporal formulas is a crucial problem. Then, we analyze the satisfiability problem for various logics of interest. We adopt a linear model of time, and take into account two kinds of traces: discrete traces and hybrid traces. Properties are therefore represented by sets of traces and temporal formulas are used to specify such sets. We analyze two classes of temporal logics of practical interest. The first class is interpreted over discrete traces, that are sequences of states (assignments to sets of variables). It includes the usual temporal operators of Linear Temporal Logic (LTL) [16], regular expression and suffix operators [10, 4]. In addition, it allows for first order atoms, composed of symbols to be interpreted according to a background theory, similarly to Satisfiability Modulo Theories [1]. We call this class RELTL(T), LTL with regular expressions Modulo Theory. This class is decidable for specific classes of theories and if the variable interpretation is local to each state [12]. The second class, referred to as HRELTL, for Hybrid RELTL [8], is interpreted over hybrid traces. Hybrid traces are useful to model the behaviors of systems featuring continuous transitions, with discrete, instantaneous transitions. Continuous variables are interpreted as functions of time, and the predicates are required to have a uniform interpretation over all interval. The satisfiability problem for HRELTL is undecidable. However, there exists a satisfiability-preserving reduction from HRELTL to RELTL(T) over discrete traces [8]. The main idea is to introduce a sufficient number of constraints on the temporal evolution of the evaluation of predicates to guarantee that the nature of the hybrid dynamics is retained also in the discrete case. We conclude the talk with an overview of the practical effectiveness of the current methods, and the open challenges in the area. References C. W. Barrett, R. Sebastiani, S. A. Seshia & C. Tinelli (2009): Satisfiability Modulo Theories. In: Handbook of Satisfiability, pp. 825–885, doi: 10. 3233/978-1-58603-929-5-825. M. Bernardo & A. Cimatti (2006): Formal Methods for Hardware Verification, 6th International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM 2006, Bertinoro, Italy, May 22-27, 2006, Advanced Lectures. Lecture Notes in Computer Science 3965. Springer. R. Bloem, R. Cavada, I. Pill, M. Roveri & A. Tchaltsev (2007): RAT: A Tool for the Formal Analysis of Requirements. In: CAV, pp. 263–267, doi: 10. 1007/978-3-540-73368-3_30. D. Bustan, A. Flaisher, O. Grumberg, O. Kupferman & M. Y. Vardi (2005): Regular Vacuity. In: CHARME, pp. 191–206, doi: 10. 1007/11560548_16. A. Cimatti, R. Corvino, A. Lazzaro, I. Narasamdya, T. Rizzo, M. Roveri, A. Sanseviero & A. Tchaltsev (2012): Formal Verification and Validation of ERTMS Industrial Railway Train Spacing System. In: CAV, pp. 378–393, doi: 10. 1007/978-3-642-31424-7_29. A. Cimatti, M. Roveri, V. Schuppan & S. Tonetta (2007): Boolean Abstraction for Temporal Logic Satisfiability. In: CAV, pp. 532–546, doi: 10. 1007/978-3-540-73368-3_53. A. Cimatti, M. Roveri, A. Susi & S. Tonetta (2012): Validation of requirements for hybrid systems: A formal approach. ACM Trans. Softw. Eng. Methodol. 21(4), pp. 22, doi: 10. 1145/2377656. 2377659. A. Cimatti, M. Roveri & S. Tonetta (2009): Requirements Validation for Hybrid Systems. In: CAV, pp. 188–203, doi: 10. 1007/978-3-642-02658-4_17. A. Cimatti & S. Tonetta (2012): A Property-Based Proof System for Contract-Based Design. In: EUROMICRO-SEAA, pp. 21–28, doi: 10. 1109/SEAA. 2012. 68. C. Eisner & D. Fisman (2006): A Practical Introduction to PSL (Series on Integrated Circuits and Systems). Springer-Verlag New York, Inc. , doi: 10. 1007/978-0-387-36123-9. A. Franzén, A. Cimatti, A. Nadel, R. Sebastiani & J. Shalev (2010): Applying SMT in symbolic execution of microcode. In: FMCAD, pp. 121–128. Available at http: //ieeexplore. ieee. org/xpls/abs_all. jsp? arnumber=5770940. S. Ghilardi, E. Nicolini, S. Ranise & D. Zucchelli (2007): Combination Methods for Satisfiability and Model-Checking of Infinite-State Systems. In: CADE, pp. 362–378, doi: 10. 1007/978-3-540-73595-3_25. W. A. Hunt, Jr. , S. Swords, J. Davis & A. Slobodová (2010): Use of Formal Verification at Centaur Technology. In: Design and Verification of Microprocessor Systems for High-Assurance Applications. Springer, pp. 65–88, doi: 10. 1007/978-1-4419-1539-9_3. R. R. Lutz (1993): Analyzing Software Requirements Errors in Safety-Critical, Embedded Systems. In: RE, pp. 126–133, doi: 10. 1109/ISRE. 1993. 324825. S. P. Miller, M. W. Whalen & D. D. Cofer (2010): Software model checking takes off. Commun. ACM 53(2), pp. 58–64, doi: 10. 1145/1646353. 1646372. A. Pnueli (1977): The Temporal Logic of Programs. In: FOCS, pp. 46–57, doi: 10. 1109/SFCS. 1977. 32. W. P. de Roever, F. S. de Boer, U. Hannemann, J. Hooman, Y. Lakhnech, M. Poel & J. Zwiers (2001): Concurrency Verification: Introduction to Compositional and Noncompositional Methods. Cambridge Tracts in Theoretical Computer Science 54. Cambridge University Press. A. L. Sangiovanni-Vincentelli, W. Damm & R. Passerone (2012): Taming Dr. Frankenstein: Contract-Based Design for Cyber-Physical Systems. Eur. J. Control 18(3), pp. 217–238, doi: 10. 3166/ejc. 18. 217-238. S. Vijayaraghavan & M. Ramanathan (2005): A Practical Guide for SystemVerilog Assertions. Springer, doi: 10. 1007/b137011. M. Weißmann, S. Bedenk, C. Buckl & A. Knoll (2011): Model Checking Industrial Robot Systems. In: SPIN, pp. 161–176, doi: 10. 1007/978-3-642-22306-8_11.

AAAI Conference 2013 Conference Paper

Timelines with Temporal Uncertainty

• Alessandro Cimatti
• Andrea Micheli
• Marco Roveri

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 fact that the plan executor cannot decide the actual 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.

AAAI Conference 2012 Conference Paper

SMT-Based Verification of Hybrid Systems

• Alessandro Cimatti
• Sergio Mover
• Stefano Tonetta

Hybrid automata networks (HAN) are a powerful formalism to model complex embedded systems. In this paper, we survey the recent advances in the application of Satisfiability Modulo Theories (SMT) to the analysis of HAN. SMT can be seen as an extended form of Boolean satisfiability (SAT), where literals are interpreted with respect to a background theory (e. g. linear arithmetic). HAN can be symbolically represented by means of SMT formulae, and analyzed by generalizing to the case of SMT the traditional model checking algorithms based on SAT.

AAAI Conference 2012 Conference Paper

Solving Temporal Problems Using SMT: Weak Controllability

• Alessandro Cimatti
• Andrea Micheli
• Marco Roveri

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.

AAAI Conference 2012 Conference Paper

Symbolic Synthesis of Observability Requirements for Diagnosability

• Benjamin Bittner
• Marco Bozzano
• Alessandro Cimatti
• Xavier Olive

Given a partially observable dynamic system and a diagnoser observing its evolution over time, diagnosability analysis formally verifies (at design time) if the diagnosis system will be able to infer (at runtime) the required information on the hidden part of the dynamic state. Diagnosability directly depends on the availability of observations, and can be guaranteed by different sets of sensors, possibly associated with different costs. In this paper, we tackle the problem of synthesizing observability requirements, i. e. automatically discovering a set of observations that is sufficient to guarantee diagnosability. We propose a novel approach with the following characterizing features. First, it fully covers a comprehensive formal framework for diagnosability analysis, and enables ranking configurations of observables in terms of cost, minimality, and diagnosability delay. Second, we propose two complementary algorithms for the synthesis of observables. Third, we describe an efficient implementation that takes full advantage of mature symbolic model checking techniques. The proposed approach is thoroughly evaluated over a comprehensive suite of benchmarks taken from the aerospace domain.

IJCAI Conference 2011 Conference Paper

A Comprehensive Approach to On-Board Autonomy Verification and Validation

• Marco Bozzano
• Alessandro Cimatti
• Marco Roveri
• Andrei Tchaltsev

Deep space missions are characterized by severely constrained communication links. To meet the needs of future missions and increase their scientific return, future space systems will require an increased level of autonomy on-board. In this work, we propose a comprehensive approach to on-board autonomy relying on model-based reasoning, and encompassing many important reasoning capabilities such as plan generation, validation, execution and monitoring, FDIR, and run-time diagnosis. The controlled platform is represented symbolically, and the reasoning capabilities are seen as symbolic manipulation of such formal model. We have developed a prototype of our framework, implemented within an on-board Autonomous Reasoning Engine. We have evaluated our approach on two case-studies inspired by real-world, ongoing projects, and characterized it in terms of reliability, availability and performance.

SAT Conference 2007 Conference Paper

A Simple and Flexible Way of Computing Small Unsatisfiable Cores in SAT Modulo Theories

• Alessandro Cimatti
• Alberto Griggio
• Roberto Sebastiani

Abstract Finding small unsatisfiable cores for SAT problems has recently received a lot of interest, mostly for its applications in formal verification. Surprisingly, the same problem in the context of SAT Modulo Theories (SMT) has instead received very little attention in the literature; in particular, we are not aware of any work aiming at producing small unsatisfiable cores in SMT. The purpose of this paper is to start filling the gap in this area, by proposing a novel approach for computing small unsat cores in SMT. The main idea is to combine an SMT solver with an external propositional core extractor: the SMT solver produces the theory lemmas found during the search; the core extractor is then called on the boolean abstraction of the original SMT problem and of the theory lemmas. This results in an unsatisfiable core for the original SMT problem, once the remaining theory lemmas have been removed. The approach has several advantages: it is extremely simple to implement and to update, and it can be interfaced with every propositional core extractor in a plug-and-play way, so that to benefit for free of all unsat-core reduction techniques which have been or will be made available.

LPAR Conference 2006 Conference Paper

Delayed Theory Combination vs. Nelson-Oppen for Satisfiability Modulo Theories: A Comparative Analysis

• Roberto Bruttomesso
• Alessandro Cimatti
• Anders Franzén
• Alberto Griggio
• Roberto Sebastiani

Abstract Many approaches for Satisfiability Modulo Theory ( SMT \({\mathcal({T})})\) rely on the integration between a SAT solver and a decision procedure for sets of literals in the background theory \({\mathcal{T}} ({\mathcal{T}}-solver\) ). When \({\mathcal{T}}\) is the combination \({{\mathcal{T}}_1\cup{\mathcal{T}}_2}\) of two simpler theories, the approach is typically handled by means of Nelson-Oppen’s (NO) theory combination schema in which two specific \({\mathcal{T}}\) - solver deduce and exchange (disjunctions of) interface equalities. In recent papers we have proposed a new approach to \(({{\mathcal{T}}_1\cup{\mathcal{T}}_2})\), called Delayed Theory Combination ( Dtc ). Here part or all the (possibly very expensive) task of deducing interface equalities is played by the SAT solver itself, at the potential cost of an enlargement of the boolean search space. In principle this enlargement could be up to exponential in the number of interface equalities generated. In this paper we show that this estimate was too pessimistic. We present a comparative analysis of Dtc vs. NO for SMT \(({{\mathcal{T}}_1\cup{\mathcal{T}}_2})\), which shows that, using state-of-the-art SAT-solving techniques, the amount of boolean branches performed by Dtc can be upper bounded by the number of deductions and boolean branches performed by NO on the same problem. We prove the result for different deduction capabilities of the \({\mathcal({T}-solver)}\) and for both convex and non-convex theories.

I&C Journal 2006 Journal Article

Efficient theory combination via boolean search

• Marco Bozzano
• Roberto Bruttomesso
• Alessandro Cimatti
• Tommi Junttila
• Silvio Ranise
• Peter van Rossum
• Roberto Sebastiani

Many approaches to deciding the satisfiability of quantifier-free formulae with respect to a background theory T—also known as Satisfiability Modulo Theory, or SMT(T)—rely on the integration between an enumerator of truth assignments and a decision procedure for conjunction of literals in T. When the background theory T is the combination T 1 ∪ T 2 of two simpler theories, the approach is typically instantiated by means of a theory combination schema (e. g. Nelson–Oppen, Shostak). In this paper we propose a new approach to SMT ( T 1 ∪ T 2 ), where the enumerator of truth assignments is integrated with two decision procedures, one for T 1 and one for T 2, acting independently from each other. The key idea is to search for a truth assignment not only to the atoms occurring in the formula, but also to all the equalities between variables which are shared between the theories. This approach is simple and expressive: for instance, no modification is required to handle non-convex theories (as opposed to traditional Nelson-Oppen combinations which require a mechanism for splitting). Furthermore, it can be made practical by leveraging on state-of-the-art boolean and SMT search techniques, and on theory layering (i. e. , cheaper reasoning first, and more often). We provide thorough experimental evidence to support our claims: we instantiate the framework with two decision procedures for the combinations of Equality and Uninterpreted Functions ( EUF ) and Linear Arithmetic ( LA ), both for (the convex case of) reals and for (the non-convex case of) integers; we analyze the impact of the different optimizations on a variety of test cases; and we compare the approach with state-of-the-art competitor tools, showing that our implemented tool compares positively with them, sometimes with dramatic gains in performance.

ECAI Conference 2006 Conference Paper

Stong Cyclic Planning Under Partial Observability

• Piergiorgio Bertoli
• Alessandro Cimatti
• Marco Pistore

Strong Cycling Planning aims at generating iterative plans that implement trial-and-error strategies, where loops are allowed only so far as there is a chance to reach the goal. In this paper, we tackle the problem of Strong Cyclic Planning under Partial Observability, making three main contributions. First, we provide a formal definition of the problem. We point out that several degrees of solution are possible and equally interesting, depending on the admissible delay between achieving the goal and detecting that it has been achieved. Second, we present a family of planning algorithms that tackle the different versions of the problem. Third, we implement the algorithms using efficient symbolic representation techniques, and experimentally compare their performances.

AIJ Journal 2006 Journal Article

Strong planning under partial observability

• Piergiorgio Bertoli
• Alessandro Cimatti
• Marco Roveri
• Paolo Traverso

Rarely planning domains are fully observable. For this reason, the ability to deal with partial observability is one of the most important challenges in planning. In this paper, we tackle the problem of strong planning under partial observability in nondeterministic domains: find a conditional plan that will result in a successful state, regardless of multiple initial states, nondeterministic action effects, and partial observability. We make the following contributions. First, we formally define the problem of strong planning within a general framework for modeling partially observable planning domains. Second, we propose an effective planning algorithm, based on and-or search in the space of beliefs. We prove that our algorithm always terminates, and is correct and complete. In order to achieve additional effectiveness, we leverage on a symbolic, bdd-based representation for the domain, and propose several search strategies. We provide a thorough experimental evaluation of our approach, based on a wide selection of benchmarks. We compare the performance of the proposed search strategies, and identify a uniform winner that combines heuristic distance measures with mechanisms that reduce runtime uncertainty. Then, we compare our planner mbp with other state-of-the art-systems. mbp is able to outperform its competitor systems, often by orders of magnitude.

LPAR Conference 2006 Conference Paper

To Ackermann-ize or Not to Ackermann-ize? On Efficiently Handling Uninterpreted Function Symbols in SMT ( EUF È T )

• Roberto Bruttomesso
• Alessandro Cimatti
• Anders Franzén
• Alberto Griggio
• Alessandro Santuari
• Roberto Sebastiani

Abstract Satisfiability Modulo Theories \((\mathit{SMT}(\mathcal{T}))\) is the problem of deciding the satisfiability of a formula with respect to a given background theory \({\mathcal{T}}\). When \({\mathcal{T}}\) is the combination of two simpler theories \({{\mathcal{T}}_1}\) and \({{\mathcal{T}}_2} ({\mathit{SMT}({{\mathcal{T}}_1\cup{\mathcal{T}}_2})})\), a standard and general approach is to handle the integration of \({{\mathcal{T}}_1}\) and \({{\mathcal{T}}_2}\) by performing some form of search on the equalities between the shared variables. A frequent and very relevant sub-case of \({\mathit{SMT}({{\mathcal{T}}_1\cup{\mathcal{T}}_2})}\) is when \({{\mathcal{T}}_1}\) is the theory of Equality and Uninterpreted Functions \(({\mathcal{EUF}})\). For this case, an alternative approach is to eliminate first all uninterpreted function symbols by means of Ackermann’s expansion, and then to solve the resulting \({\mathit{SMT}}({{\mathcal{T}}_2})\) problem. In this paper we build on the empirical observation that there is no absolute winner between these two alternative approaches, and that the performance gaps between them are often dramatic, in either direction. We propose a simple technique for estimating a priori the costs and benefits, in terms of the size of the search space of an \({\mathit{SMT}}\) tool, of applying Ackermann’s expansion to all or part of the function symbols. A thorough experimental analysis, including the benchmarks of the SMT’05 competition, shows that the proposed technique is extremely effective in improving the overall performance of the \({\mathit{SMT}}\) tool.

ICAPS Conference 2006 Conference Paper

Towards Strong Cyclic Planning under Partial Observability

• Piergiorgio Bertoli
• Alessandro Cimatti
• Marco Pistore

Strong Cyclic Planning aims at generating iterative plans that only allow loops so far as there is a chance to reach the goal. The problem is already significantly complex for fully observable domains; when considering partially observable domains, even providing a formal definition is far from straightforward. In this work, we provide a formal definition of Strong Cyclic Planning under Partial Observability, which makes clear how several degrees of solution are possible and equally interesting, depending on the admissible delay between achieving the goal and detecting that it has been achieved.

ECAI Conference 2004 Conference Paper

Interleaving Execution and Planning for Nondeterministic, Partially Observable Domains

• Piergiorgio Bertoli
• Alessandro Cimatti
• Paolo Traverso

ECAI Conference 2004 Conference Paper

Many Hands Make Light Work: Localized Satisfiability for Multi-Context Systems

• Floris Roelofsen
• Luciano Serafini
• Alessandro Cimatti

ICAPS Conference 2003 Conference Paper

A Framework for Planning with Extended Goals under Partial Observability

• Piergiorgio Bertoli
• Alessandro Cimatti
• Marco Pistore
• Paolo Traverso

Planning in nondeterministic domains with temporally extended goals under partial observability is one of the most challenging problems in planning. Subsets of this problem have been already addressed in the literature. For instance, planning for extended goals has been developed under the simplifying hypothesis of full observability. And the problem of a partial observability has been tackled in the case of simple reachability goals. The general combination of extended goals and partial observability is, to the best of our knowledge, still an open problem, whose solution turns out to be by no means trivial. In this paper we do not solve the problem in its generality, but we perform a significant step in this direction by providing a solid basis for tackling it. Our first contribution is the definition of a general framework that encompasses both partial observability and temporally extended goals, and that allows for describing complex, realistic domains and significant goals over them. A second contribution is the definition of the K-CTL goal language, that extends CTL (a classical language for expressing temporal requirements) with a knowledge operator that allows to reason about the information that can be acquired at run-time. This is necessary to deal with partially observable domains, where only limited run-time "knowledge" about the domain state is available. A general mechanism for plan validation with K-CTL goals is also defined. This mechanism is based on a monitor, that plays the role of evaluating the truth of knowledge predicates.

IJCAI Conference 2003 Conference Paper

Formal Verification of Diagnosability via Symbolic Model Checking

• Alessandro Cimatti
• Charles Pecheur
• Roberto Cavada

This paper addresses the formal verification of diagnosis systems. We tackle the problem of diagnosability: given a partially observable dynamic system, and a diagnosis system observing its evolution over time, we discuss how to verify (at design time) if the diagnosis system will be able to infer (at runtime) the required information on the hidden part of the dynamic state. We tackle the problem by looking for pairs of scenarios that are observationally indistinguishable, but lead to situations that are required to be distinguished. We reduce the problem to a model checking problem. The finite state machine modeling the dynamic system is replicated to construct such pairs of scenarios; the diagnosability conditions are formally expressed in temporal logic; the check for diagnosability is carried out by solving a model checking problem. We focus on the practical applicability of the method. We show how the formalism is adequate to represent diagnosability problems arising from a significant, real-world application. Symbolic model checking techniques are used to formally verify and incrementally refine the diagnosability conditions.

ICAPS Conference 2002 Conference Paper

Improving Heuristics for Planning as Search in Belief Space

• Piergiorgio Bertoli
• Alessandro Cimatti

Search in the space of beliefs has been proposed as a convenient framework for tackling planning under uncertainty. Significant improvements have been recently achieved, especially thanks to the use of symbolic model checking techniques such as Binary Decision Diagrams. However, the problem is extremely complex, and the heuristics available so far are unable to provide enough guidance for an informed search. In this paper we tackle the problem of defining effective heuristics for driving the search in belief space. The basic intuition is that the "degree of knowledge" associated with the belief states reached by partial plans must be explicitly taken into account when deciding the search direction. We propose a way of ranking belief states depending on their degree of knowledge with respect to a given set of boolean functions. This allows us to define a planning algorithm based on the identification and solution of suitable "knowledge subgoals", that are used as intermediate steps during the search. The solution of knowledge subgoals is based on the identifi- cation of "knowledge acquisition conditions", i. e. subsets of the state space from where it is possible to perform knowledge acquisition actions. We show the effectiveness of the proposed ideas by observing substantial improvements in the conformant planning algorithms of MBP.

ECAI Conference 2002 Conference Paper

Solving Power Supply Restoration Problems with Planning via Symbolic Model Checking

• Piergiorgio Bertoli
• Alessandro Cimatti
• John K. Slaney
• Sylvie Thiébaux

AAAI Conference 1998 Conference Paper

Automatic OBDD-Based Generation of Universal Plans in Non-Deterministic Domains

• Alessandro Cimatti

Mostreal worldenvironmentsare non-deterministic. Automaticplan formation in non-deterministic dommns is, however, still an open problem. In this paper wepresent a practical algorithmfor the automatic generation of solutions to planning problemsin nondeterministic domains. Ourapproachhas the following mainfeatures. First, the planner generates Universal Plans. Second, it generatesplans whichare guaranteed to achievethe goal in spite of non-determinism, if such plans exist. Otherwise, the planner generates plans whichencodeiterative trial-and-error strategies (e. g. try to pick up a blockuntil succeed), whichare guaranteedto achievethe goal underthe assumption that if there is a non-deterministic possibilityfor the iteration to terminate, this will not be ignoredforever. Third, the implementation of the planneris basedon symbolic modelcheckingtechniqueswhichhavebeendesignedto exploreefficiently large state spaces. Theimplementation exploits the compactness of ORDDS (OrderedBinary DecisionDiagrams) to express in a practical way universalplans of extremely large size. *

ICAPS Conference 1998 Conference Paper

Strong Planning in Non-Deterministic Domains Via Model Checking

• Alessandro Cimatti
• Marco Roveri
• Paolo Traverso

Most real world domains are non-deterministic: the state of the world can be incompletely known, the effect of actions can not be completely foreseen, and the environment can change in unpredictable ways. Automatic plan formation in non-deterministic domains is, however, still an open problem. In this paper we show how to do strong planning in non-deterministic domains, i.e. finding automatically plans which are guaranteed to achieve the goal regardless of non-determinism. We define a notion of planning solution which is guaranteed to achieve the goal independently of non-determinism, a notion of plan including conditionals and iterations, and an automatic decision procedure for strong planning based on model checking techniques. The procedure is correct, complete and returns optimal plans. The work has been implemented in MBP, a planner based on model checking techniques.

ECAI Conference 1992 Conference Paper

Beyond the Single Planning Paradigm: Introspective Planning

• Paolo Traverso
• Alessandro Cimatti
• Luca Spalazzi