@article{micheli_aij_2022,
  title     = {Decidability and complexity of action-based temporal planning over dense time},
  author    = {Nicola Gigante and
               Andrea Micheli and
               Angelo Montanari and
               Enrico Scala},
  journal   = {Artificial Intelligence},
  year      = {2022}
}

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.

@inproceedings{micheli_kr_2022,
  title     = {On the Expressive Power of Intermediate and Conditional Effects in Temporal Planning},
  author    = {Nicola Gigante and
               Andrea Micheli and
               Enrico Scala},
  booktitle = {KR},
  year      = {2022}
}

Automated planning is the task of finding a sequence of actions that reach a desired goal, given a description of their applicability and their effects on the world. In temporal planning, actions have a duration and can overlap in time. In modern temporal planning formalisms, two features have been introduced which are very useful from a modeling perspective, but are not yet thoroughly understood: intermediate conditions and effects (ICE) and conditional effects. The expressive power of such constructs is yet not well comprehended, especially when time is dense, and no minimum separation is required between mutex events. This paper reveals that both ICE and conditional effects do not add expressive power with regards to common temporal planning formalisms. In particular, we show how they can be compiled away using a polynomial-size encoding that makes no assumptions on the time domain. This encoding advances our understanding of these features, and allow their use with simple temporal planners that lack their support. Moreover, it provides a constructive proof that temporal planning with ICE and conditional effects remains PSPACE-complete.

@inproceedings{micheli_aaai_2022,
  title     = {Deciding Unsolvability in Temporal Planning under Action Non-Self-Overlapping},
  author    = {Stefan Panjkovic and
               Andrea Micheli},
  booktitle = {AAAI},
  year      = {2022}
}

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.

@inproceedings{micheli_concur_2021,
  title     = {SMT-Based Model Checking of Max-Plus Linear Systems},
  author    = {Muhammad Syifa'ul Mufid and
               Andrea Micheli and
               Alessandro Abate and
               Alessandro Cimatti},
  booktitle = {CONCUR},
  year      = {2021}
}

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.

@inproceedings{micheli_time_2021_2,
  title     = {Efficient Anytime Computation and Execution of Decoupled Robustness Envelopes for Temporal Plans},
  author    = {Michael Cashmore and
               Alessandro Cimatti and
               Daniele Magazzeni and
               Andrea Micheli and
               Parisa Zehtabi},
  booktitle = {TIME},
  year      = {2021}
}

One of the major limitations for the employment of model-based planning and scheduling in practical applications is the need of costly re-planning when an incongruence between the observed reality and the formal model is encountered during execution. Robustness Envelopes characterize the set of possible contingencies that a plan is able to address without re-planning, but their exact computation is extremely expensive; furthermore, general robustness envelopes are not amenable for efficient execution.

In this paper, we present a novel, anytime algorithm to approximate Robustness Envelopes, making them scalable and executable. This is proven by an experimental analysis showing the efficiency of the algorithm, and by a concrete casestudy where the execution of robustness envelopes significantly reduces the number of re-plannings.

@inproceedings{micheli_time_2021_1,
  title     = {Olisipo: A Probabilistic Approach to the Adaptable Execution of Deterministic Temporal Plans},
  author    = {Tomas Ribeiro and
               Oscar Lima and
               Michael Cashmore and
               Andrea Micheli and
               Rodrigo Ventura},
  booktitle = {TIME},
  year      = {2021}
}

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.

@inproceedings{micheli_aaai_2021,
  title     = {Synthesis of Search Heuristics for Temporal Planning via Reinforcement Learning},
  author    = {Andrea Micheli and
               Alessandro Valentini},
  booktitle = {AAAI},
  year      = {2021}
}

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.

@inproceedings{micheli_intex_2020_2,
  title     = {Robust Execution of Deterministic Plans in Non-deterministic Environments},
  author    = {Oscar Lima and
               Michael Cashmore and
               Daniele Magazzeni and
               Andrea Micheli and
               Rodrigo Ventura},
  booktitle = {INTEX},
  year      = {2020}
}

In order to ensure the robust execution of a deterministic plan, execution must be adaptable to unexpected situations in the world and to exogenous events. This is critical in domains in which committing to a wrong ordering of actions can cause the plan failure, even when all the actions succeed. We propose an approach for the execution of temporal plans that permits some adaptability to unexpected situations of the environment (non-determinism) while maintaining the validity of the plan through online reasoning.

Our approach computes an adaptable, partially-ordered plan from a given totally-ordered plan. The partially-ordered plan is adaptable in that it can exploit beneficial differences between the world and what was expected. The approach is general in that it can be used with any task planner that produces either a totally or a partially-ordered plan. We propose a plan execution algorithm that computes online the complete set of valid totally-ordered plans described by an adaptable partially-ordered plan together with the probability of success for each of them. This set is then used to choose the next action to execute.

@inproceedings{micheli_intex_2020_1,
  title     = {Efficient Anytime Computation and Execution of Decoupled Robustness Envelopes for Temporal Plans},
  author    = {Michael Cashmore and
               Alessandro Cimatti and
               Daniele Magazzeni and
               Andrea Micheli and
               Parisa Zehtabi},
  booktitle = {INTEX},
  year      = {2020}
}

One of the major limitations for the employment of model-based planning and scheduling in practical applications is the need of costly re-planning when an incongruence between the observed reality and the formal model is encountered during execution. Robustness Envelopes characterize the set of possible contingencies that a plan is able to address without re-planning, but their exact computation is extremely expensive; furthermore, general robustness envelopes are not amenable for efficient execution.

In this paper, we present a novel, anytime algorithm to approximate Robustness Envelopes, making them scalable and executable. This is proven by an experimental analysis showing the efficiency of the algorithm, and by a concrete casestudy where the execution of robustness envelopes significantly reduces the number of re-plannings.

@inproceedings{micheli_prl_2020,
  title     = {Synthesis of Search Heuristics for Temporal Planning via Reinforcement Learning},
  author    = {Andrea Micheli and
               Alessandro Valentini},
  booktitle = {PRL},
  year      = {2020}
}

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.

@inproceedings{micheli_aaai_2020_2,
  title     = {Decidability and Complexity of Action-Based Temporal Planning over Dense Time},
  author    = {Nicola Gigante and
               Andrea Micheli and
               Angelo Montanari and
               Enrico Scala},
  booktitle = {AAAI},
  year      = {2020}
}

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.

@inproceedings{micheli_aaai_2020_1,
  title     = {Temporal Planning with Intermediate Conditions and Effects},
  author    = {Alessandro Valentini and
               Andrea Micheli and
               Alessandro Cimatti},
  booktitle = {AAAI},
  year      = {2020}
}

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.

@inproceedings{micheli_aaai_2019_2,
  title     = {Temporal Planning with Temporal Metric Trajectory Constraints},
  author    = {Andrea Micheli and
               Enrico Scala},
  booktitle = {AAAI},
  year      = {2019}
}

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-the-art planning approaches on industrial benchmarks, and competitive with similar solving methods on well known benchmarks took from the planning competition.

@inproceedings{micheli_aaai_2019_1,
  title     = {Robustness Envelopes for Temporal Plans},
  author    = {Michael Cashmore and
               Alessandro Cimatti and
               Daniele Magazzeni and
               Andrea Micheli and
               Parisa Zehtabi},
  booktitle = {AAAI},
  year      = {2019}
}

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.

@article{micheli_aij_2017,
  title     = {Strong Temporal Planning with Uncontrollable Durations},
  author    = {Alessandro Cimatti and
               Minh Do and
               Andrea Micheli and
               Marco Roveri and
               David E. Smith},
  journal   = {Artificial Intelligence},
  year      = {2017}
}

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.

@article{micheli_ia_2017,
  title     = {Disjunctive temporal networks with uncertainty via SMT: Recent results and directions},
  author    = {Andrea Micheli},
  journal   = {Intelligenza Artificiale},
  year      = {2017}
}

Many Planning and Scheduling systems are designed assuming that the system under control is able to decide the duration of all the activities being executed. However, in many application scenarios this assumption is not acceptable because the actual timing of actions is not under direct control of the plan executor. Hence, new Planning and Scheduling techniques are needed to deal with this temporal uncertainty explicitly.

In this paper, we summarize and systematize a series of works in which we addressed this uncertainty problem in the realm of temporal network scheduling. We show how Satisfiability Modulo Theory (SMT) solvers can be exploited to quickly solve different kinds of query in this setting. In particular, we focus on the framework of Disjunctive Temporal Networks with Uncertainty and address the three degrees of controllability for the fully-disjunctive class of problems, solving several open problems in the literature and experimentally showing the performance of the developed techniques. Finally, we outline and discuss several foreseeable directions of research in this field.

@inproceedings{micheli_aaai_2017,
  title     = {Validating Domains and Plans for Temporal Planning via Encoding into Infinite-State Linear Temporal Logic},
  author    = {Alessandro Cimatti and
               Andrea Micheli and
               Marco Roveri},
  booktitle = {AAAI},
  year      = {2017}
}

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

@article{micheli_acta_2016,
  title     = {Dynamic Controllability via Timed Game Automata},
  author    = {Alessandro Cimatti and
               Luke Hunsberger and
               Andrea Micheli and
               Roberto Posenato and
               Marco Roveri},
  journal   = {Acta Informatica},
  year      = {2016}
}

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 temporal consistency or different levels of controllability, but corresponding algorithms for more expressive networks (e.g., those that include observation nodes or disjunctive constraints) have so far been unavailable.

This paper introduces a new approach to determine the dynamic controllability of a very expressive class of temporal networks that accommodates observation nodes and disjunctive constraints. The approach is based on encoding the dynamic controllability problem into a reachability game for Timed Game Automata (TGAs). This is the first sound and complete approach for determining the dynamic controllability of such networks. The encoding also highlights the theoretical relationships between various kinds of temporal networks and TGAs. The new algorithms have immediate applications in the design and analysis of workflow models being developed to automate business processes, including workflows in the health-care domain.

@inproceedings{micheli_aaai_2016,
  title     = {Dynamic Controllability of Disjunctive Temporal Networks: Validation and Synthesis of Executable Strategies},
  author    = {Alessandro Cimatti and
               Andrea Micheli and
               Marco Roveri},
  booktitle = {AAAI},
  year      = {2016}
}

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.

@inproceedings{micheli_smt_2015,
  title     = {pySMT: a Solver-Agnostic Library for Fast Prototyping of SMT-Based Algorithms},
  author    = {Marco Gario and
               Andrea Micheli},
  booktitle = {SMT Workshop},
  year      = {2015}
}

Satisfiability Modulo Theory is increasingly being used as workhorse in multiple and disparate domains. Several efficient solvers exist and cross-compatibility is provided by a wide adoption of the SMT-Lib interface. Nevertheless, there are still some obstacles that slow down the development of algorithms based on the SMT technology.

First, there is no common programmatic API among different solvers: a user needs to commit to a specific solver API early in the development, or implement a text-based interaction via the SMT-Lib interface, thus losing the ability of exploiting features provided by solvers that are not part of the SMT-Lib. Second, there is no high-level SMT API for fast prototyping: a user often needs to re-implement common routines such as substitution and type-checking.

In this paper, we introduce pySMT, an open-source python library that provides a solver agnostic interface to define, manipulate and solve SMT formulae. pySMT leverages the native APIs of solvers (if available) or their SMT-LIB interface. The library allows the seamless combination of different solvers and fast prototyping of complex SMT-based algorithms.

@inproceedings{micheli_ijcai_2015,
  title     = {Compiling Away Uncertainty in Strong Temporal Planning with Uncontrollable Durations},
  author    = {Andrea Micheli and
               Minh Do and
               David E. Smith},
  booktitle = {IJCAI},
  year      = {2015}
}

Real world temporal planning often involves dealing with uncertainty about the duration of actions. In this paper, we describe a sound-and-complete compilation technique for strong planning that reduces any planning instance with uncertainty in the duration of actions to a plain temporal planning problem without uncertainty.

We evaluate our technique by comparing it with a recently-presented technique for PDDL domains with temporal uncertainty. The experimental results demonstrate the practical applicability of our approach and show a complementary behavior with respect to the previous techniques. We also demonstrate the high expressiveness of the translation by applying it to a significant fragment of the ANML language.

@article{micheli_corr_2015,
  title     = {The xSAP Safety Analysis Platform},
  author    = {Benjamin Bittner and
               Marco Bozzano and
               Roberto Cavada and
               Alessandro Cimatti and
               Marco Gario and
               Alberto Griggio and
               Cristian Mattarei and
               Andrea Micheli and
               Gianni Zampedri},
  journal   = {CoRR},
  year      = {2015}
}

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

@inproceedings{micheli_spark_2015,
  title     = {Compiling Away Uncertainty in Strong Temporal Planning with Uncontrollable Durations},
  author    = {Andrea Micheli and
               Minh Do and
               David E. Smith},
  booktitle = {SPARK},
  year      = {2015}
}

Real world temporal planning often involves dealing with uncertainty about the duration of actions. In this paper, we describe a sound-and-complete compilation technique for strong planning that reduces any planning instance with uncertainty in the duration of actions to a plain temporal planning problem without uncertainty.

We evaluate our technique by comparing it with a recently-presented technique for PDDL domains with temporal uncertainty. The experimental results demonstrate the practical applicability of our approach and show a complementary behavior with respect to the previous techniques. We also demonstrate the high expressiveness of the translation by applying it to a significant fragment of the ANML language.

@article{micheli_aij_2015,
  title     = {An SMT-based approach to Weak Controllability for Disjunctive Temporal Problems with Uncertainty},
  author    = {Alessandro Cimatti and
               Andrea Micheli and
               Marco Roveri},
  journal   = {Artificial Intelligence},
  year      = {2015}
}

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.

@inproceedings{micheli_aaai_2015_tfpg,
  title     = {SMT-based Validation of Timed Failure Propagation Graphs},
  author    = {Marco Bozzano and
               Alessandro Cimatti and
               Marco Gario and
               Andrea Micheli},
  booktitle = {AAAI},
  year      = {2015}
}

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.

@inproceedings{micheli_aaai_2015_stpud,
  title     = {Strong Temporal Planning with Uncontrollable Durations: a State-Space Approach},
  author    = {Alessandro Cimatti and
               Andrea Micheli and
               Marco Roveri},
  booktitle = {AAAI},
  year      = {2015}
}

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 state-of-the-art planner. An experimental evaluation over several benchmark problems shows the practical feasibility of the proposed approach.

@article{micheli_constraints_2014,
  title     = {Solving strong controllability of temporal problems with uncertainty using SMT},
  author    = {Alessandro Cimatti and
               Andrea Micheli and
               Marco Roveri},
  journal   = {Constraints},
  year      = {2015}
}

Temporal Problems (TPs) represent constraints over the timing of activities, as arising in many applications such as scheduling and temporal planning. A TP with uncertainty (TPU) is characterized by activities with uncontrollable duration. Different classes of TPU are possible, depending on the Boolean structure of the constraints: we have simple (STPU), constraint satisfaction (TCSPU), and disjunctive (DTPU) temporal problems with uncertainty.

In this paper we tackle the problem of strong controllability, i.e. finding an assignment to all the controllable time points, such that the constraints are fulfilled under any possible assignment of uncontrollable time points.

Our approach casts the problem in the framework of Satisfiability Modulo Theory (SMT), where the uncertainty of durations can be modeled by means of universal quantifiers. The use of quantifier elimination techniques leads to quantifier-free encodings, which are in turn solved with efficient SMT solvers.

We obtain the first practical and comprehensive solution for strong controllability. We provide a family of efficient encodings, that are able to exploit the specific structure of the problem. The approach has been implemented, and experimentally evaluated over a large set of benchmarks. The results clearly demonstrate that the proposed approach is feasible, and outperforms the best state-of-the-art competitors, when available.

@inproceedings{micheli_cav_2014,
  title     = {The nuXmv Symbolic Model Checker},
  author    = {Roberto Cavada and
               Alessandro Cimatti and
               Michele Dorigatti and
               Alberto Griggio and
               Alessandro Mariotti and
               Andrea Micheli and
               Sergio Mover and
               Marco Roveri and
               Stefano Tonetta},
  booktitle = {CAV},
  year      = {2014},
  pages     = {334-342}
}

This paper describes the nuXmv symbolic model checker for finite- and infinite-state synchronous transition systems. nuXmv is the evolution of the NuSMV open source model checker. It builds on and extends NuSMV along two main directions. For finite-state systems it complements the basic verification techniques of NuSMV with state-of-the-art verification algorithms.

For infinite-state systems, it extends the NuSMV language with new data types, namely Integers and Reals, and it provides advanced SMT-based model checking techniques.

Besides extended functionalities, nuXmv has been optimized in terms of performance to be competitive with the state of the art. nuXmv has been used in several industrial projects as verification back-end, and it is the basis for several extensions to cope with requirements analysis, contract based design, model checking of hybrid systems, safety assessment, and software model checking.

@inproceedings{micheli_time_2014,
  title     = {Sound and Complete Algorithms for Checking the Dynamic Controllability of Temporal Networks with Uncertainty, Disjunction and Observation},
  author    = {Alessandro Cimatti and
               Luke Hunsberger and
               Andrea Micheli and
               Roberto Posenato and
               Marco Roveri},
  booktitle = {TIME},
  year      = {2014}
}

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.

@inproceedings{micheli_aaai_2014,
  title     = {Using Timed Game Automata to Synthesize Execution Strategies for Simple Temporal Networks with Uncertainty},
  author    = {Alessandro Cimatti and
               Luke Hunsberger and
               Andrea Micheli and
               Marco Roveri},
  booktitle = {AAAI},
  year      = {2014}
}

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.

@inproceedings{micheli_aaai_2013,
  title     = {Timelines with Temporal Uncertainty},
  author    = {Alessandro Cimatti and
               Andrea Micheli and
               Marco Roveri},
  booktitle = {AAAI},
  year      = {2013}
}

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.

@inproceedings{micheli_cp_2012,
  title     = {Solving Temporal Problems Using SMT: Strong Controllability},
  author    = {Alessandro Cimatti and
               Andrea Micheli and
               Marco Roveri},
  booktitle = {CP},
  year      = {2012},
  pages     = {248-264}
}

Many applications, such as scheduling and temporal planning, require the solution of Temporal Problems (TP's) representing constraints over the timing of activities. A TP with uncertainty (TPU) is characterized by activities with uncontrollable duration. Depending on the Boolean structure of the constraints, we have simple (STPU), constraint satisfaction (TCSPU), and disjunctive (DTPU) temporal problems with uncertainty.

In this work we tackle the problem of strong controllability, i.e. finding an assignment to all the controllable time points, such that the constraints are fulfilled under any possible assignment of uncontrollable time points. We work in the framework of Satisfiability Modulo Theory (SMT), where uncertainty is expressed by means of universal quantifiers. We obtain the first comprehensive solution to strong controllability: the use of quantifier elimination techniques leads to quantifier-free encodings, which are in turn solved with efficient SMT solvers.

We provide a detailed experimental evaluation of our approach over a large set of benchmarks. The results clearly demonstrate that the proposed approach is feasibile, and outperforms the best state-of-the-art competitors, when available.

@inproceedings{micheli_aaai_2012,
  title     = {Solving Temporal Problems Using SMT: Weak Controllability},
  author    = {Alessandro Cimatti and
               Andrea Micheli and
               Marco Roveri},
  booktitle = {AAAI},
  year      = {2012},
  pages     = {448-454}
}

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.

@inproceedings{micheli_cav_2011,
  title     = {Kratos - A Software Model Checker for SystemC},
  author    = {Alessandro Cimatti and
               ALberto Griggio and
               Andrea Micheli and
               Iman Narasamdya and
               Marco Roveri},
  booktitle = {CAV},
  year      = {2011},
  pages     = {310-316}
}

The growing popularity of SystemC has attracted research aimed at the formal verification of SystemC designs. In this paper we present KRATOS, a software model checker for SystemC. KRATOS verifies safety properties, in the form of program assertions, by allowing users to explore two directions in the verification. First, by relying on the translation from SystemC designs to sequential C programs, KRATOS is capable of model checking the resulting C programs using the symbolic lazy predicate abstraction technique. Second, KRATOS implements a novel algorithm, called ESST, that combines Explicit state techniques to deal with the SystemC Scheduler, with Symbolic techniques to deal with the Threads. KRATOS is built on top of NuSMV and MathSAT, and uses state-ofthe-art SMT-based techniques for program abstractions and refinements.

@inproceedings{micheli_topi_2010,
  title     = {OthelloPlay: a plug-in based tool for requirement formalization and validation},
  author    = {Roberto Cavada and
               Alessandro Cimatti and
               Andrea Micheli and
               Marco Roveri and
               Angelo Susi and
               Stefano Tonetta},
  booktitle = {TOPI},
  year      = {2010},
  pages     = {59-59}
}

Requirement engineering is one of the most important phases in the development process of software and systems. In safety-critical applications, it is important to support the validation of the requirements with formal techniques to identify and remove flaws. However, requirements are often written in textual documents and their formalization and validation is not trivial for non-experts in formal methods. The goal of the OthelloPlay tool is to support formalization of textual requirements and to simplify the use of formal techniques for requirements validation. The tool combines a formal verification engine and the Microsoft Word editor in a single and consistent environment. A fundamental key in our design approach is a plug-in-based architecture, which uses the Python language in conjunction with a Microsoft Word Add-In. The user can jump between textual requirements in the Microsoft Word editor and the corresponding formal requirements model.

@inproceedings{micheli_fmcad_2010,
  title     = {Verifying SystemC: A software model checking approach},
  author    = {Alessandro Cimatti and
               Andrea Micheli and
               Iman Narasamdya and
               Marco Roveri},
  booktitle = {FMCAD},
  year      = {2010},
  pages     = {51-59}
}

SystemC is becoming a de-facto standard for the development of embedded systems. Verification of SystemC designs is critical since it can prevent error propagation down to the hardware. SystemC allows for very efficient simulations before synthesizing the RTL description, but formal verification is still at a preliminary stage. Recent works translate SystemC into the input language of finite-state model checkers, but they abstract away relevant semantic aspects, and show limited scalability.

In this paper, we approach formal verification of SystemC by reduction to software model checking. We explore two directions. First, we rely on a translation from SystemC to a sequential C program, that contains both the mapping of the SystemC threads in form of C functions, and the coding of relevant semantic aspects (e.g. of the SystemC kernel). In terms of verification, this enables the “off-the-shelf” use of model checking techniques for sequential software, such as lazy abstraction.

Second, we propose an approach that exploits the intrinsic structure of SystemC. In particular, each SystemC thread is translated into a separate sequential program and explored with lazy abstraction, while the overall verification is orchestrated by the direct execution of the SystemC scheduler. The technique can be seen as generalizing lazy abstraction to the case of multi-threaded software with exclusive threads and cooperative scheduling.

The above approaches have been implemented in a new software model checker. An experimental evaluation carried out on several case studies taken from the SystemC distribution and from the literature demonstrate the potential of the approach.

@inproceedings{micheli_ase_2009,
  title     = {Supporting Requirements Validation: The EuRailCheck Tool},
  author    = {Roberto Cavada and
               Alessandro Cimatti and
               Alessandro Mariotti and
               Cristian Mattarei and
               Andrea Micheli and
               Sergio Mover and
               Marco Pensallorto and
               Marco Roveri and
               Angelo Susi and
               Stefano Tonetta},
  booktitle = {ASE},
  year      = {2009},
  pages     = {665-667}
}

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.