Search Results

Documents authored by Cimatti, Alessandro

Document
DOI: 10.4230/OASIcs.DX.2024.9
Inferring Sensor Placement Using Critical Pairs and Satisfiability Modulo Theory

Authors: Alexander Diedrich, René Heesch, Marco Bozzano, Björn Ludwig, Alessandro Cimatti, and Oliver Niggemann

Published in: OASIcs, Volume 125, 35th International Conference on Principles of Diagnosis and Resilient Systems (DX 2024)

Abstract
Industrial fault diagnosis exhibits the perennial problem of reasoning with partial and real-valued information. This is mainly due to the fact that in real-world applications, industrial systems are only instrumented insofar, as sensor information is required for their functioning. However, such instrumentation leaves out much information that would be useful for fault diagnosis. This is problematic since consistency-based fault diagnosis uses available information and computes intermediate values within a system description. These values are then used to compare expected normal behaviour to actual observed values. In the past, this was done only for Boolean circuits. Recently, satisfiability modulo non-linear arithmetic (SMT) formulations have been developed that allow the calculation of real values, instead of only Boolean ones. Leveraging those formulations, we in this article present a novel method to infer missing sensor values using an SMT system description and the notion of critical pairs. We show on a running example and also empirically that we can infer novel measurements for five process industrial systems. We conclude that, although SMT calculations accumulate some error, we can infer novel optimal measurements for all systems.
Cite as

Alexander Diedrich, René Heesch, Marco Bozzano, Björn Ludwig, Alessandro Cimatti, and Oliver Niggemann. Inferring Sensor Placement Using Critical Pairs and Satisfiability Modulo Theory. In 35th International Conference on Principles of Diagnosis and Resilient Systems (DX 2024). Open Access Series in Informatics (OASIcs), Volume 125, pp. 9:1-9:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{diedrich_et_al:OASIcs.DX.2024.9,
  author =	{Diedrich, Alexander and Heesch, Ren\'{e} and Bozzano, Marco and Ludwig, Bj\"{o}rn and Cimatti, Alessandro and Niggemann, Oliver},
  title =	{{Inferring Sensor Placement Using Critical Pairs and Satisfiability Modulo Theory}},
  booktitle =	{35th International Conference on Principles of Diagnosis and Resilient Systems (DX 2024)},
  pages =	{9:1--9:19},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-356-0},
  ISSN =	{2190-6807},
  year =	{2024},
  volume =	{125},
  editor =	{Pill, Ingo and Natan, Avraham and Wotawa, Franz},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.DX.2024.9},
  URN =		{urn:nbn:de:0030-drops-221013},
  doi =		{10.4230/OASIcs.DX.2024.9},
  annote =	{Keywords: Sensor Placement, Satisfiability Modulo Theory, Critical Pairs, Diagnosability}
}
Document
Extended Abstract
DOI: 10.4230/OASIcs.DX.2024.32
Summary of "A Lazy Approach to Neural Numerical Planning with Control Parameters" (Extended Abstract)

Authors: René Heesch, Alessandro Cimatti, Jonas Ehrhardt, Alexander Diedrich, and Oliver Niggemann

Published in: OASIcs, Volume 125, 35th International Conference on Principles of Diagnosis and Resilient Systems (DX 2024)

Abstract
This is an extended abstract of the manuscript "A Lazy Approach to Neural Numerical Planning with Control Parameters" [René Heesch et al., 2024]. The paper presents a lazy, hierarchical approach to tackle the challenge of planning in complex numerical domains, where the effects of actions are influenced by control parameters, and may be described by neural networks.
Cite as

René Heesch, Alessandro Cimatti, Jonas Ehrhardt, Alexander Diedrich, and Oliver Niggemann. Summary of "A Lazy Approach to Neural Numerical Planning with Control Parameters" (Extended Abstract). In 35th International Conference on Principles of Diagnosis and Resilient Systems (DX 2024). Open Access Series in Informatics (OASIcs), Volume 125, pp. 32:1-32:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{heesch_et_al:OASIcs.DX.2024.32,
  author =	{Heesch, Ren\'{e} and Cimatti, Alessandro and Ehrhardt, Jonas and Diedrich, Alexander and Niggemann, Oliver},
  title =	{{Summary of "A Lazy Approach to Neural Numerical Planning with Control Parameters"}},
  booktitle =	{35th International Conference on Principles of Diagnosis and Resilient Systems (DX 2024)},
  pages =	{32:1--32:3},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-356-0},
  ISSN =	{2190-6807},
  year =	{2024},
  volume =	{125},
  editor =	{Pill, Ingo and Natan, Avraham and Wotawa, Franz},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.DX.2024.32},
  URN =		{urn:nbn:de:0030-drops-221243},
  doi =		{10.4230/OASIcs.DX.2024.32},
  annote =	{Keywords: Satisfiability Modulo Theory, Neural Numerical Planning with Control Parameters, Neural Networks}
}
Document
DOI: 10.4230/LIPIcs.TIME.2024.13
Introducing Interdependent Simple Temporal Networks with Uncertainty for Multi-Agent Temporal Planning

Authors: Ajdin Sumic, Thierry Vidal, Andrea Micheli, and Alessandro Cimatti

Published in: LIPIcs, Volume 318, 31st International Symposium on Temporal Representation and Reasoning (TIME 2024)

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

Ajdin Sumic, Thierry Vidal, Andrea Micheli, and Alessandro Cimatti. Introducing Interdependent Simple Temporal Networks with Uncertainty for Multi-Agent Temporal Planning. In 31st International Symposium on Temporal Representation and Reasoning (TIME 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 318, pp. 13:1-13:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{sumic_et_al:LIPIcs.TIME.2024.13,
  author =	{Sumic, Ajdin and Vidal, Thierry and Micheli, Andrea and Cimatti, Alessandro},
  title =	{{Introducing Interdependent Simple Temporal Networks with Uncertainty for Multi-Agent Temporal Planning}},
  booktitle =	{31st International Symposium on Temporal Representation and Reasoning (TIME 2024)},
  pages =	{13:1--13:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-349-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{318},
  editor =	{Sala, Pietro and Sioutis, Michael and Wang, Fusheng},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2024.13},
  URN =		{urn:nbn:de:0030-drops-212200},
  doi =		{10.4230/LIPIcs.TIME.2024.13},
  annote =	{Keywords: Temporal constraints satisfaction, uncertainty, STNU, Controllability checking, Explainable inconsistency, Multi-agent planning}
}
Document
DOI: 10.4230/DagRep.14.1.25
Fusing Causality, Reasoning, and Learning for Fault Management and Diagnosis (Dagstuhl Seminar 24031)

Authors: Alessandro Cimatti, Ingo Pill, and Alexander Diedrich

Published in: Dagstuhl Reports, Volume 14, Issue 1 (2024)

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar "Fusing Causality, Reasoning, and Learning for Fault Management and Diagnosis" (24031). The goal of this Dagstuhl Seminar was to provide an interdisciplinary forum to discuss the fundamental principles of fault management and diagnosis, bringing together international researchers and practitioners from the fields of symbolic reasoning, machine learning, and control engineering.
Cite as

Alessandro Cimatti, Ingo Pill, and Alexander Diedrich. Fusing Causality, Reasoning, and Learning for Fault Management and Diagnosis (Dagstuhl Seminar 24031). In Dagstuhl Reports, Volume 14, Issue 1, pp. 25-48, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@Article{cimatti_et_al:DagRep.14.1.25,
  author =	{Cimatti, Alessandro and Pill, Ingo and Diedrich, Alexander},
  title =	{{Fusing Causality, Reasoning, and Learning for Fault Management and Diagnosis (Dagstuhl Seminar 24031)}},
  pages =	{25--48},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2024},
  volume =	{14},
  number =	{1},
  editor =	{Cimatti, Alessandro and Pill, Ingo and Diedrich, Alexander},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.14.1.25},
  URN =		{urn:nbn:de:0030-drops-204899},
  doi =		{10.4230/DagRep.14.1.25},
  annote =	{Keywords: cyber-physical systems, diagnosis, fault detection and management, integrative ai, model-based reasoning}
}
Document
DOI: 10.4230/LIPIcs.TIME.2021.13
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.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
DOI: 10.4230/LIPIcs.CONCUR.2021.22
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.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
DOI: 10.4230/OASIcs.SynCoP.2015.106
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.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
DOI: 10.4230/DagRep.4.11.227
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.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}
}
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
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact