4 Search Results for "Cimatti, Alessandro"


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

Authors: Michael Cashmore, Alessandro Cimatti, Daniele Magazzeni, Andrea Micheli, and Parisa Zehtabi

Published in: LIPIcs, Volume 206, 28th International Symposium on Temporal Representation and Reasoning (TIME 2021)


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

Cite as

Michael Cashmore, Alessandro Cimatti, Daniele Magazzeni, Andrea Micheli, and Parisa Zehtabi. Efficient Anytime Computation and Execution of Decoupled Robustness Envelopes for Temporal Plans. In 28th International Symposium on Temporal Representation and Reasoning (TIME 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 206, pp. 13:1-13:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{cashmore_et_al:LIPIcs.TIME.2021.13,
  author =	{Cashmore, Michael and Cimatti, Alessandro and Magazzeni, Daniele and Micheli, Andrea and Zehtabi, Parisa},
  title =	{{Efficient Anytime Computation and Execution of Decoupled Robustness Envelopes for Temporal Plans}},
  booktitle =	{28th International Symposium on Temporal Representation and Reasoning (TIME 2021)},
  pages =	{13:1--13:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-206-8},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{206},
  editor =	{Combi, Carlo and Eder, Johann and Reynolds, Mark},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2021.13},
  URN =		{urn:nbn:de:0030-drops-147895},
  doi =		{10.4230/LIPIcs.TIME.2021.13},
  annote =	{Keywords: Temporal Planning, Robustness Envelopes}
}
Document
SMT-Based Model Checking of Max-Plus Linear Systems

Authors: Muhammad Syifa'ul Mufid, Andrea Micheli, Alessandro Abate, and Alessandro Cimatti

Published in: LIPIcs, Volume 203, 32nd International Conference on Concurrency Theory (CONCUR 2021)


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

Cite as

Muhammad Syifa'ul Mufid, Andrea Micheli, Alessandro Abate, and Alessandro Cimatti. SMT-Based Model Checking of Max-Plus Linear Systems. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 22:1-22:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{mufid_et_al:LIPIcs.CONCUR.2021.22,
  author =	{Mufid, Muhammad Syifa'ul and Micheli, Andrea and Abate, Alessandro and Cimatti, Alessandro},
  title =	{{SMT-Based Model Checking of Max-Plus Linear Systems}},
  booktitle =	{32nd International Conference on Concurrency Theory (CONCUR 2021)},
  pages =	{22:1--22:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-203-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{203},
  editor =	{Haddad, Serge and Varacca, Daniele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2021.22},
  URN =		{urn:nbn:de:0030-drops-143993},
  doi =		{10.4230/LIPIcs.CONCUR.2021.22},
  annote =	{Keywords: Max-Plus Linear Systems, Satisfiability Modulo Theory, Model Checking, Linear Temporal Logic}
}
Document
Informal Presentation
Parameter Synthesis with IC3 (Informal Presentation)

Authors: Alessandro Cimatti, Alberto Griggio, Sergio Mover, and Stefano Tonetta

Published in: OASIcs, Volume 44, 2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15) (2015)


Abstract
Parametric systems arise in many application domains, from real-time systems to software to cyber-physical systems. Parameters are fundamental to model unknown quantities at design time and allow a designer to explore different instantiation of the system (i.e. every parameter valuation induces a different system), during the early development phases. A key challenge is to automatically synthesize all the parameter valuations for which the system satisfies some properties. In this talk we focus on the parameter synthesis problem for infinite-state transition systems and invariant properties. We describe the synthesis algorithm Param IC3, which is based on IC3, one of the major recent breakthroughs in SAT-based model checking, and lately extended to the SMT case. The algorithm follows a general approach that first builds the set of "bad" parameter valuations and then obtain the set of "good" valuations by complement. The approach enumerates the counterexamples that violate the property, extracting from each counterexample a region of bad parameter valuations, existentially quantifying the state variables. ParamIC3 follows the same principles, but it overcomes some limitations of the previous approach by exploiting the IC3 features. First, IC3 may find a set of counterexamples s_o, ..., s_k, where each state in s_i is guaranteed to reach some of the bad states in s_k in k-i steps; this is exploited to apply the expensive quantifier elimination on shortest, and thus more amenable, counterexamples. Second, the internal structure of IC3 allows our extension to be integrated in a fully incremental fashion, never restarting the search from scratch to find a new counterexample. While various approaches already solve the parameter synthesis problem for several kind of systems, like infinite-state transition systems, timed and hybrid automata, the advantages ParamIC3 are that: it synthesizes an optimal region of parameters, it avoids computing the whole set of the reachable states, it is incremental and applies quantifier elimination only to small formulas. We present the results of an experimental evaluation performed on benchmarks from the timed and hybrid systems domain. We compared the approach with similar SMT-based techniques and with techniques based on the computation of the reachable states. The results show the potential of our approach.

Cite as

Alessandro Cimatti, Alberto Griggio, Sergio Mover, and Stefano Tonetta. Parameter Synthesis with IC3 (Informal Presentation). In 2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15). Open Access Series in Informatics (OASIcs), Volume 44, pp. 106-107, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)


Copy BibTex To Clipboard

@InProceedings{cimatti_et_al:OASIcs.SynCoP.2015.106,
  author =	{Cimatti, Alessandro and Griggio, Alberto and Mover, Sergio and Tonetta, Stefano},
  title =	{{Parameter Synthesis with IC3}},
  booktitle =	{2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15)},
  pages =	{106--107},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-82-8},
  ISSN =	{2190-6807},
  year =	{2015},
  volume =	{44},
  editor =	{Andr\'{e}, \'{E}tienne and Frehse, Goran},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.SynCoP.2015.106},
  URN =		{urn:nbn:de:0030-drops-56144},
  doi =		{10.4230/OASIcs.SynCoP.2015.106},
  annote =	{Keywords: Parameter Synthesis, Infinite-state Transition Systems, Satisfiability Modulo Theories, IC3}
}
Document
Automated Planning and Model Checking (Dagstuhl Seminar 14482)

Authors: Alessandro Cimatti, Stefan Edelkamp, Maria Fox, Daniele Magazzeni, and Erion Plaku

Published in: Dagstuhl Reports, Volume 4, Issue 11 (2015)


Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 14482 "Automated Planning and Model Checking". There has been a lot of work on the exchanges between the areas of automated planning and model checking, based on the observation that a model-checking problem can be cast as a planning problem and vice-versa. The motivation for this seminar was to increase the synergy between the two research communities, and explore recent progress in the two areas in terms of techniques, tools and formalisms for describing planning and verification problems. The main outcomes were a greater common understanding of planning and model-checking issues and challenges, and greater appreciation of the crosswover between the modelling languages and methods. Different application domains were also explored, where planning and model-checking can be effectively integrated.

Cite as

Alessandro Cimatti, Stefan Edelkamp, Maria Fox, Daniele Magazzeni, and Erion Plaku. Automated Planning and Model Checking (Dagstuhl Seminar 14482). In Dagstuhl Reports, Volume 4, Issue 11, pp. 227-245, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)


Copy BibTex To Clipboard

@Article{cimatti_et_al:DagRep.4.11.227,
  author =	{Cimatti, Alessandro and Edelkamp, Stefan and Fox, Maria and Magazzeni, Daniele and Plaku, Erion},
  title =	{{Automated Planning and Model Checking (Dagstuhl Seminar 14482)}},
  pages =	{227--245},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2015},
  volume =	{4},
  number =	{11},
  editor =	{Cimatti, Alessandro and Edelkamp, Stefan and Fox, Maria and Magazzeni, Daniele and Plaku, Erion},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagRep.4.11.227},
  URN =		{urn:nbn:de:0030-drops-49731},
  doi =		{10.4230/DagRep.4.11.227},
  annote =	{Keywords: planning via model checking, directed model checking, plan validation, falsification, GPU-based state space exploration, hybrid systems, heuristic sea}
}
  • Refine by Author
  • 4 Cimatti, Alessandro
  • 2 Magazzeni, Daniele
  • 2 Micheli, Andrea
  • 1 Abate, Alessandro
  • 1 Cashmore, Michael
  • Show More...

  • Refine by Classification
  • 1 Computing methodologies → Robotic planning
  • 1 Theory of computation → Verification by model checking

  • Refine by Keyword
  • 1 GPU-based state space exploration
  • 1 IC3
  • 1 Infinite-state Transition Systems
  • 1 Linear Temporal Logic
  • 1 Max-Plus Linear Systems
  • Show More...

  • Refine by Type
  • 4 document

  • Refine by Publication Year
  • 2 2015
  • 2 2021

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail