Search Results

Documents authored by Abate, Alessandro

Document
DOI: 10.4230/LIPIcs.CONCUR.2023.22
Quantitative Verification with Neural Networks

Authors: Alessandro Abate, Alec Edwards, Mirco Giacobbe, Hashan Punchihewa, and Diptarko Roy

Published in: LIPIcs, Volume 279, 34th International Conference on Concurrency Theory (CONCUR 2023)

Abstract
We present a data-driven approach to the quantitative verification of probabilistic programs and stochastic dynamical models. Our approach leverages neural networks to compute tight and sound bounds for the probability that a stochastic process hits a target condition within finite time. This problem subsumes a variety of quantitative verification questions, from the reachability and safety analysis of discrete-time stochastic dynamical models, to the study of assertion-violation and termination analysis of probabilistic programs. We rely on neural networks to represent supermartingale certificates that yield such probability bounds, which we compute using a counterexample-guided inductive synthesis loop: we train the neural certificate while tightening the probability bound over samples of the state space using stochastic optimisation, and then we formally check the certificate’s validity over every possible state using satisfiability modulo theories; if we receive a counterexample, we add it to our set of samples and repeat the loop until validity is confirmed. We demonstrate on a diverse set of benchmarks that, thanks to the expressive power of neural networks, our method yields smaller or comparable probability bounds than existing symbolic methods in all cases, and that our approach succeeds on models that are entirely beyond the reach of such alternative techniques.
Cite as

Alessandro Abate, Alec Edwards, Mirco Giacobbe, Hashan Punchihewa, and Diptarko Roy. Quantitative Verification with Neural Networks. In 34th International Conference on Concurrency Theory (CONCUR 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 279, pp. 22:1-22:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{abate_et_al:LIPIcs.CONCUR.2023.22,
  author =	{Abate, Alessandro and Edwards, Alec and Giacobbe, Mirco and Punchihewa, Hashan and Roy, Diptarko},
  title =	{{Quantitative Verification with Neural Networks}},
  booktitle =	{34th International Conference on Concurrency Theory (CONCUR 2023)},
  pages =	{22:1--22:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-299-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{279},
  editor =	{P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.22},
  URN =		{urn:nbn:de:0030-drops-190162},
  doi =		{10.4230/LIPIcs.CONCUR.2023.22},
  annote =	{Keywords: Data-driven Verification, Quantitative Verification, Probabilistic Programs, Stochastic Dynamical Models, Counterexample-guided Inductive Synthesis, Neural Networks}
}
Document
Introduction
DOI: 10.4230/LITES.8.2.0
Introduction to the Special Issue on Distributed Hybrid Systems

Authors: Alessandro Abate, Uli Fahrenberg, and Martin Fränzle

Published in: LITES, Volume 8, Issue 2 (2022): Special Issue on Distributed Hybrid Systems. Leibniz Transactions on Embedded Systems, Volume 8, Issue 2

Abstract
This special issue contains seven papers within the broad subject of Distributed Hybrid Systems, that is, systems combining hybrid discrete-continuous state spaces with elements of concurrency and logical or spatial distribution. It follows up on several workshops on the same theme which were held between 2017 and 2019 and organized by the editors of this volume. The first of these workshops was held in Aalborg, Denmark, in August 2017 and associated with the MFCS conference. It featured invited talks by Alessandro Abate, Martin Fränzle, Kim G. Larsen, Martin Raussen, and Rafael Wisniewski. The second workshop was held in Palaiseau, France, in July 2018, with invited talks by Luc Jaulin, Thao Dang, Lisbeth Fajstrup, Emmanuel Ledinot, and André Platzer. The third workshop was held in Amsterdam, The Netherlands, in August 2019, associated with the CONCUR conference. It featured a special theme on distributed robotics and had invited talks by Majid Zamani, Hervé de Forges, and Xavier Urbain. The vision and purpose of the DHS workshops was to connect researchers working in real-time systems, hybrid systems, control theory, formal verification, distributed computing, and concurrency theory, in order to advance the subject of distributed hybrid systems. Such systems are abundant and often safety-critical, but ensuring their correct functioning can in general be challenging. The investigation of their dynamics by analysis tools from the aforementioned domains remains fragmentary, providing the rationale behind the workshops: it was conceived that convergence and interaction of theories, methods, and tools from these different areas was needed in order to advance the subject.
Cite as

LITES, Volume 8, Issue 2: Special Issue on Distributed Hybrid Systems, pp. 0:i-0:iii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@Article{abate_et_al:LITES.8.2.0,
  author =	{Abate, Alessandro and Fahrenberg, Uli and Fr\"{a}nzle, Martin},
  title =	{{Introduction to the Special Issue on Distributed Hybrid Systems}},
  journal =	{Leibniz Transactions on Embedded Systems},
  pages =	{00:1--00:3},
  ISSN =	{2199-2002},
  year =	{2022},
  volume =	{8},
  number =	{2},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LITES.8.2.0},
  doi =		{10.4230/LITES.8.2.0},
  annote =	{Keywords: Distributed hybrid systems}
}
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
DOI: 10.4230/LIPIcs.CONCUR.2015.169
Dynamic Bayesian Networks as Formal Abstractions of Structured Stochastic Processes

Authors: Sadegh Esmaeil Zadeh Soudjani, Alessandro Abate, and Rupak Majumdar

Published in: LIPIcs, Volume 42, 26th International Conference on Concurrency Theory (CONCUR 2015)

Abstract
We study the problem of finite-horizon probabilistic invariance for discrete-time Markov processes over general (uncountable) state spaces. We compute discrete-time, finite-state Markov chains as formal abstractions of general Markov processes. Our abstraction differs from existing approaches in two ways. First, we exploit the structure of the underlying Markov process to compute the abstraction separately for each dimension. Second, we employ dynamic Bayesian networks (DBN) as compact representations of the abstraction. In contrast, existing approaches represent and store the (exponentially large) Markov chain explicitly, which leads to heavy memory requirements limiting the application to models of dimension less than half, according to our experiments. We show how to construct a DBN abstraction of a Markov process satisfying an independence assumption on the driving process noise. We compute a guaranteed bound on the error in the abstraction w.r.t. the probabilistic invariance property; the dimension-dependent abstraction makes the error bounds more precise than existing approaches. Additionally, we show how factor graphs and the sum-product algorithm for DBNs can be used to solve the finite-horizon probabilistic invariance problem. Together, DBN-based representations and algorithms can be significantly more efficient than explicit representations of Markov chains for abstracting and model checking structured Markov processes.
Cite as

Sadegh Esmaeil Zadeh Soudjani, Alessandro Abate, and Rupak Majumdar. Dynamic Bayesian Networks as Formal Abstractions of Structured Stochastic Processes. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 169-183, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{esmaeilzadehsoudjani_et_al:LIPIcs.CONCUR.2015.169,
  author =	{Esmaeil Zadeh Soudjani, Sadegh and Abate, Alessandro and Majumdar, Rupak},
  title =	{{Dynamic Bayesian Networks as Formal Abstractions of Structured Stochastic Processes}},
  booktitle =	{26th International Conference on Concurrency Theory (CONCUR 2015)},
  pages =	{169--183},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-91-0},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{42},
  editor =	{Aceto, Luca and de Frutos Escrig, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2015.169},
  URN =		{urn:nbn:de:0030-drops-53693},
  doi =		{10.4230/LIPIcs.CONCUR.2015.169},
  annote =	{Keywords: Structured stochastic systems, general space Markov processes, formal verification, dynamic Bayesian networks, Markov chain abstraction}
}
Document
DOI: 10.4230/DagRep.4.10.69
Modeling, Verification, and Control of Complex Systems for Energy Networks (Dagstuhl Seminar 14441)

Authors: Alessandro Abate, Martin Fränzle, Ian Hiskens, and Martin Strelec

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

Abstract
Power and energy networks) are systems of great societal and economic relevance and impact, particularly given the recent growing emphasis on environmental issues and on sustainable substitutes (renewables) to traditional energy sources (coal, oil, nuclear). Power networks also represent systems of considerable engineering interest. The aim of this Dagstuhl seminar has been to survey existing and explore novel formal frameworks for modeling, analysis and control of complex, large scale cyber-physical systems, with emphasis on applications in power networks. Stochastic hybrid systems (SHS) stand for a mathematical framework that allows capturing the complex interactions between continuous dynamics, discrete dynamics, and probabilistic uncertainty. In the context of power networks, stochastic hybrid dynamics arises naturally: (i) continuous dynamics models the evolution of voltages, frequencies, etc.; (ii) discrete dynamics models controller logic and changes in network topology (unit commitment); and (iii) probability models the uncertainty about power demand, power supply from renewables and power market price. The seminar has covered relevant approaches to modeling and analysis of stochastic hybrid dynamics, in the context of energy networks.
Cite as

Alessandro Abate, Martin Fränzle, Ian Hiskens, and Martin Strelec. Modeling, Verification, and Control of Complex Systems for Energy Networks (Dagstuhl Seminar 14441). In Dagstuhl Reports, Volume 4, Issue 10, pp. 69-97, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@Article{abate_et_al:DagRep.4.10.69,
  author =	{Abate, Alessandro and Fr\"{a}nzle, Martin and Hiskens, Ian and Strelec, Martin},
  title =	{{Modeling, Verification, and Control of Complex Systems for Energy Networks (Dagstuhl Seminar 14441)}},
  pages =	{69--97},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2015},
  volume =	{4},
  number =	{10},
  editor =	{Abate, Alessandro and Fr\"{a}nzle, Martin and Hiskens, Ian and Strelec, Martin},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.4.10.69},
  URN =		{urn:nbn:de:0030-drops-48939},
  doi =		{10.4230/DagRep.4.10.69},
  annote =	{Keywords: Analysis, control, and verification of complex stochastic systems; formal synthesis; reliability engineering and assessment; energy networks}
}
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 Imprint Privacy Contact