16 Search Results for "Abate, Alessandro"

Issue

Leibniz Transactions on Embedded Systems, Volume 8, Issue 2, 2022

LITES, Volume 8, Issue 2

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

Special Issue on Distributed Hybrid Systems

Document
Invited Talk
DOI: 10.4230/LIPIcs.STACS.2026.2
Moments in Time: Algebraic Analysis for Solvable Loops (Invited Talk)

Authors: Laura Kovács

Published in: LIPIcs, Volume 364, 43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026)

Abstract
With substantial progress in automated reasoning, algebraic approaches emerged to automatically analyse program loops in an exact manner. In this invited talk, we discuss recent results in characterizing the functional behaviour of loops with polynomial arithmetic and probabilistic updates. This problem remains unsolved even when we restrict consideration to loops that are non-nested, without conditionals, and/or without exit conditions [Ehud Hrushovski et al., 2023; Julian Müllner and others, 2024]. We are motivated by applications of computer-aided verification, in particular to assess the safety, security, and sensitivity of computer systems [M. Z. Kwiatkowska et al., 2011; Gilles Barthe et al., 2012; Gilles Barthe and others, 2018; Marcel Moosbrugger et al., 2023; Alessandro Abate et al., 2023; Andrey Kofnov and others, 2024]. We are interested in modeling, deciding, and solving loop analysis. The key to our work are moment-computable loops [L. Kovács, 2008; Marcel Moosbrugger et al., 2022] which allow us to set limits on what is decidable and solvable in loop analysis. Our approach combines algebra, statistics, and automated reasoning to mechanize loop analysis. Various techniques, such as martingale theory and quantifier elimination, can be seen as examples of moment-computable loop analysis. This talk is structured within three inter-connected parts. We first bring moment-based loop analysis into the landscape of {loop invariant synthesis} and extend moment-computable loops with {termination guarantees}. We next automate the reasoning about (probabilistic) loops by summarizing loop semantics as (probabilistic) algebraic recurrences, whose closed-form solutions capture (higher-order) moments, and hence invariants, among loop variables. These recurrences together with loop tests yield moment-based (super)martingales necessary to prove loop termination and compute probability bounds on termination. We finally describe moment-computable loops whose invariant synthesis {decidable} or as {hard} as open problems, such as the Skolem problem [Graham Everest et al., 2003; Terrence Tao, 2008].
Cite as

Laura Kovács. Moments in Time: Algebraic Analysis for Solvable Loops (Invited Talk). In 43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 364, pp. 2:1-2:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{kovacs:LIPIcs.STACS.2026.2,
  author =	{Kov\'{a}cs, Laura},
  title =	{{Moments in Time: Algebraic Analysis for Solvable Loops}},
  booktitle =	{43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026)},
  pages =	{2:1--2:2},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-412-3},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{364},
  editor =	{Mahajan, Meena and Manea, Florin and McIver, Annabelle and Thắng, Nguy\~{ê}n Kim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2026.2},
  URN =		{urn:nbn:de:0030-drops-254910},
  doi =		{10.4230/LIPIcs.STACS.2026.2},
  annote =	{Keywords: program analysis, algebraic reasoning, symbolic computation, loop invariants}
}
Document
DOI: 10.4230/LIPIcs.CSL.2026.26
ε-Distance via Lévy-Prokhorov Lifting

Authors: Josée Desharnais and Ana Sokolova

Published in: LIPIcs, Volume 363, 34th EACSL Annual Conference on Computer Science Logic (CSL 2026)

Abstract
The most studied and accepted pseudometric for probabilistic processes is one based on the Kantorovich distance between distributions. It comes with many theoretical and motivating results, in particular it is the fixpoint of a given functional and defines a functor on (complete) pseudometric spaces. It is also the foundation for a categorical lifting of pseudometrics. Other notions of behavioural pseudometrics have also been proposed, one of them (ε-distance) based on ε-bisimulation. ε-Distance has the advantages that it is intuitively easy to understand, it relates systems that are conceptually close (for example, an imperfect implementation is close to its specification), and it comes equipped with a natural notion of ε-coupling. Finally, this distance is easy to compute. We show that ε-distance is also the greatest fixpoint of a functional and provides a functor. The latter is obtained by replacing the Kantorovich distance in the lifting functor with the Lévy-Prokhorov distance. In addition, we show that ε-couplings and ε-bisimulations have an appealing coalgebraic characterization.
Cite as

Josée Desharnais and Ana Sokolova. ε-Distance via Lévy-Prokhorov Lifting. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 26:1-26:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{desharnais_et_al:LIPIcs.CSL.2026.26,
  author =	{Desharnais, Jos\'{e}e and Sokolova, Ana},
  title =	{{\epsilon-Distance via L\'{e}vy-Prokhorov Lifting}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{26:1--26:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-411-6},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{363},
  editor =	{Guerrini, Stefano and K\"{o}nig, Barbara},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.26},
  URN =		{urn:nbn:de:0030-drops-254506},
  doi =		{10.4230/LIPIcs.CSL.2026.26},
  annote =	{Keywords: L\'{e}vy-Prokhorov metric, behavioural distance, epsilon-bisimulation, reactive probabilistic transition systems, discrete labelled Markov processes, coalgebraic epsilon-(bi)simulation}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.CONCUR.2025.3
On-The-Fly Verification: Advancements in Dependency Graphs (Invited Talk)

Authors: Jiří Srba

Published in: LIPIcs, Volume 348, 36th International Conference on Concurrency Theory (CONCUR 2025)

Abstract
Dependency graphs have emerged as a versatile and powerful formalism with wide-ranging applications in formal verification. In this extended abstract, we provide an overview of selected advancements in on-the-fly verification techniques based on dependency graphs, focusing on the recent developments, optimizations and generalizations of this generic verification framework.
Cite as

Jiří Srba. On-The-Fly Verification: Advancements in Dependency Graphs (Invited Talk). In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 3:1-3:5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{srba:LIPIcs.CONCUR.2025.3,
  author =	{Srba, Ji\v{r}{\'\i}},
  title =	{{On-The-Fly Verification: Advancements in Dependency Graphs}},
  booktitle =	{36th International Conference on Concurrency Theory (CONCUR 2025)},
  pages =	{3:1--3:5},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-389-8},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{348},
  editor =	{Bouyer, Patricia and van de Pol, Jaco},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.3},
  URN =		{urn:nbn:de:0030-drops-239534},
  doi =		{10.4230/LIPIcs.CONCUR.2025.3},
  annote =	{Keywords: dependency graphs, Boolean equation systems, on-the-fly algorithms, fixed-point computation, applications}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2025.6
Omega-Regular Verification and Control for Distributional Specifications in MDPs

Authors: S. Akshay, Ouldouz Neysari, and Ðorđe Žikelić

Published in: LIPIcs, Volume 348, 36th International Conference on Concurrency Theory (CONCUR 2025)

Abstract
A classical approach to studying Markov decision processes (MDPs) is to view them as state transformers. However, MDPs can also be viewed as distribution transformers, where an MDP under a strategy generates a sequence of probability distributions over MDP states. This view arises in several applications, even as the probabilistic model checking problem becomes much harder compared to the classical state transformer counterpart. It is known that even distributional reachability and safety problems become computationally intractable (Skolem- and positivity-hard). To address this challenge, recent works focused on sound but possibly incomplete methods for verification and control of MDPs under the distributional view. However, existing automated methods are applicable only to distributional reachability, safety and reach-avoidance specifications. In this work, we present the first automated method for verification and control of MDPs with respect to distributional omega-regular specifications. To achieve this, we propose a novel notion of distributional certificates, which are sound and complete proof rules for proving that an MDP under a distributionally memoryless strategy satisfies some distributional omega-regular specification. We then use our distributional certificates to design the first fully automated algorithms for verification and control of MDPs with respect to distributional omega-regular specifications. Our algorithms follow a template-based synthesis approach and provide soundness and relative completeness guarantees, while running in PSPACE. Our prototype implementation demonstrates practical applicability of our algorithms to challenging examples collected from the literature.
Cite as

S. Akshay, Ouldouz Neysari, and Ðorđe Žikelić. Omega-Regular Verification and Control for Distributional Specifications in MDPs. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 6:1-6:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{akshay_et_al:LIPIcs.CONCUR.2025.6,
  author =	{Akshay, S. and Neysari, Ouldouz and \v{Z}ikeli\'{c}, Ðor{\d}e},
  title =	{{Omega-Regular Verification and Control for Distributional Specifications in MDPs}},
  booktitle =	{36th International Conference on Concurrency Theory (CONCUR 2025)},
  pages =	{6:1--6:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-389-8},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{348},
  editor =	{Bouyer, Patricia and van de Pol, Jaco},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.6},
  URN =		{urn:nbn:de:0030-drops-239562},
  doi =		{10.4230/LIPIcs.CONCUR.2025.6},
  annote =	{Keywords: MDPs, Distributional objectives, \omega-regularity, Certificates}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.FSCD.2025.2
Vehicle: Bridging the Embedding Gap in the Verification of Neuro-Symbolic Programs (Invited Talk)

Authors: Matthew L. Daggitt, Wen Kokke, Robert Atkey, Ekaterina Komendantskaya, Natalia Slusarz, and Luca Arnaboldi

Published in: LIPIcs, Volume 337, 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)

Abstract
Neuro-symbolic programs, i.e. programs containing both machine learning components and traditional symbolic code, are becoming increasingly widespread. Finding a general methodology for verifying such programs is challenging due to both the number of different tools involved and the intricate interface between the "neural" and "symbolic" program components. In this paper we present a general decomposition of the neuro-symbolic verification problem into parts, and examine the problem of the embedding gap that occurs when one tries to combine proofs about the neural and symbolic components. To address this problem we then introduce Vehicle - standing as an abbreviation for a "verification condition language" - an intermediate programming language interface between machine learning frameworks, automated theorem provers, and dependently-typed formalisations of neuro-symbolic programs. Vehicle allows users to specify the properties of the neural components of neuro-symbolic programs once, and then safely compile the specification to each interface using a tailored typing and compilation procedure. We give a high-level overview of Vehicle’s overall design, its interfaces and compilation & type-checking procedures, and then demonstrate its utility by formally verifying the safety of a simple autonomous car controlled by a neural network, operating in a stochastic environment with imperfect information.
Cite as

Matthew L. Daggitt, Wen Kokke, Robert Atkey, Ekaterina Komendantskaya, Natalia Slusarz, and Luca Arnaboldi. Vehicle: Bridging the Embedding Gap in the Verification of Neuro-Symbolic Programs (Invited Talk). In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 2:1-2:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{daggitt_et_al:LIPIcs.FSCD.2025.2,
  author =	{Daggitt, Matthew L. and Kokke, Wen and Atkey, Robert and Komendantskaya, Ekaterina and Slusarz, Natalia and Arnaboldi, Luca},
  title =	{{Vehicle: Bridging the Embedding Gap in the Verification of Neuro-Symbolic Programs}},
  booktitle =	{10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
  pages =	{2:1--2:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-374-4},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{337},
  editor =	{Fern\'{a}ndez, Maribel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.2},
  URN =		{urn:nbn:de:0030-drops-236172},
  doi =		{10.4230/LIPIcs.FSCD.2025.2},
  annote =	{Keywords: Neural Network Verification, Types, Interactive Theorem Provers}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2025.31
Higher-Dimensional Automata: Extension to Infinite Tracks

Authors: Luc Passemard, Amazigh Amrane, and Uli Fahrenberg

Published in: LIPIcs, Volume 337, 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)

Abstract
We introduce higher-dimensional automata for infinite interval ipomsets (ω-HDAs). We define key concepts from different points of view, inspired from their finite counterparts. Then we explore languages recognized by ω-HDAs under Büchi and Muller semantics. We show that Muller acceptance is more expressive than Büchi acceptance and, in contrast to the finite case, both semantics do not yield languages closed under subsumption. Then, we adapt the original rational operations to deal with ω-HDAs and show that while languages of ω-HDAs are ω-rational, not all ω-rational languages can be expressed by ω-HDAs.
Cite as

Luc Passemard, Amazigh Amrane, and Uli Fahrenberg. Higher-Dimensional Automata: Extension to Infinite Tracks. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 31:1-31:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{passemard_et_al:LIPIcs.FSCD.2025.31,
  author =	{Passemard, Luc and Amrane, Amazigh and Fahrenberg, Uli},
  title =	{{Higher-Dimensional Automata: Extension to Infinite Tracks}},
  booktitle =	{10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
  pages =	{31:1--31:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-374-4},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{337},
  editor =	{Fern\'{a}ndez, Maribel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.31},
  URN =		{urn:nbn:de:0030-drops-236466},
  doi =		{10.4230/LIPIcs.FSCD.2025.31},
  annote =	{Keywords: Higher-dimensional automata, concurrency theory, omega pomsets, B\"{u}chi acceptance, Muller acceptance, interval pomsets, pomsets with interfaces}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2025.10
Bottom-Up Synthesis of Memory Mutations with Separation Logic

Authors: Kasra Ferdowsi and Hila Peleg

Published in: LIPIcs, Volume 333, 39th European Conference on Object-Oriented Programming (ECOOP 2025)

Abstract
Programming-by-Example (PBE) is the paradigm of program synthesis specified via input-output pairs. It is commonly used because examples are easy to provide and collect from the environment. A popular optimization for enumerative synthesis with examples is Observational Equivalence (OE), which groups programs into equivalence classes according to their evaluation on example inputs. Current formulations of OE, however, are severely limited by the assumption that the synthesizer’s target language contains only pure components with no side-effects, either enforcing this in their target language, or ignoring it, leading to an incorrect enumeration. This limits their ability to use realistic component sets. We address this limitation by borrowing from Separation Logic, which can compositionally reason about heap mutations. We reformulate PBE using a restricted Separation Logic: Concrete Heap Separation Logic (CHSL), transforming the search for programs into a proof search in CHSL. This lets us perform bottom-up enumerative synthesis without the need for expert-provided annotations or domain-specific inferences, but with three key advantages: we (i) preserve correctness in the presence of memory-mutating operations, (ii) compact the search space by representing many concrete programs as one under CHSL, and (iii) perform a provably correct OE-reduction. We present SObEq (Side-effects in OBservational EQuivalence), a bottom-up enumerative algorithm that, given a PBE task, searches for its CHSL derivation. The SObEq algorithm is proved correct with no purity assumptions: we show it is guaranteed to lose no solutions. We also evaluate our implementation of SObEq on benchmarks from the literature and online sources, and show that it produces high-quality results quickly.
Cite as

Kasra Ferdowsi and Hila Peleg. Bottom-Up Synthesis of Memory Mutations with Separation Logic. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 10:1-10:32, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{ferdowsi_et_al:LIPIcs.ECOOP.2025.10,
  author =	{Ferdowsi, Kasra and Peleg, Hila},
  title =	{{Bottom-Up Synthesis of Memory Mutations with Separation Logic}},
  booktitle =	{39th European Conference on Object-Oriented Programming (ECOOP 2025)},
  pages =	{10:1--10:32},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-373-7},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{333},
  editor =	{Aldrich, Jonathan and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2025.10},
  URN =		{urn:nbn:de:0030-drops-233036},
  doi =		{10.4230/LIPIcs.ECOOP.2025.10},
  annote =	{Keywords: Program synthesis, observational equivalence}
}
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},
  URN =		{urn:nbn:de:0030-drops-192926},
  doi =		{10.4230/LITES.8.2.0},
  annote =	{Keywords: Distributed hybrid systems}
}
Document
DOI: 10.4230/LITES.8.2.5
Bayesian Hybrid Automata: A Formal Model of Justified Belief in Interacting Hybrid Systems Subject to Imprecise Observation

Authors: Paul Kröger 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
Hybrid discrete-continuous system dynamics arises when discrete actions, e.g. by a decision algorithm, meet continuous behaviour, e.g. due to physical processes and continuous control. A natural domain of such systems are emerging smart technologies which add elements of intelligence, co-operation, and adaptivity to physical entities, enabling them to interact with each other and with humans as systems of (human-)cyber-physical systems or (H)CPSes.Various flavours of hybrid automata have been suggested as a means to formally analyse CPS dynamics. In a previous article, we demonstrated that all these variants of hybrid automata provide inaccurate, in the sense of either overly pessimistic or overly optimistic, verdicts for engineered systems operating under imprecise observation of their environment due to, e.g., measurement error. We suggested a revised formal model, called Bayesian hybrid automata, that is able to represent state tracking and estimation in hybrid systems and thereby enhances precision of verdicts obtained from the model in comparison to traditional model variants.In this article, we present an extended definition of Bayesian hybrid automata which incorporates a new class of guard and invariant functions that allow to evaluate traditional guards and invariants over probability distributions. The resulting framework allows to model observers with knowledge about the control strategy of an observed agent but with imprecise estimates of the data on which the control decisions are based.
Cite as

Paul Kröger and Martin Fränzle. Bayesian Hybrid Automata: A Formal Model of Justified Belief in Interacting Hybrid Systems Subject to Imprecise Observation. In LITES, Volume 8, Issue 2 (2022): Special Issue on Distributed Hybrid Systems. Leibniz Transactions on Embedded Systems, Volume 8, Issue 2, pp. 05:1-05:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@Article{kroger_et_al:LITES.8.2.5,
  author =	{Kr\"{o}ger, Paul and Fr\"{a}nzle, Martin},
  title =	{{Bayesian Hybrid Automata: A Formal Model of Justified Belief in Interacting Hybrid Systems Subject to Imprecise Observation}},
  journal =	{Leibniz Transactions on Embedded Systems},
  pages =	{05:1--05:27},
  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.5},
  URN =		{urn:nbn:de:0030-drops-192970},
  doi =		{10.4230/LITES.8.2.5},
  annote =	{Keywords: }
}
Document
DOI: 10.4230/LITES.8.2.3
Higher-Dimensional Timed and Hybrid Automata

Authors: Uli Fahrenberg

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

Abstract
We introduce a new formalism of higher-dimensional timed automata, based on Pratt and van Glabbeek’s higher-dimensional automata and Alur and Dill’s timed automata. We prove that their reachability is PSPACE-complete and can be decided using zone-based algorithms. We also extend the setting to higher-dimensional hybrid automata.The interest of our formalism is in modeling systems which exhibit both real-time behavior and concurrency. Other existing formalisms for real-time modeling identify concurrency and interleaving, which, as we shall argue, is problematic.
Cite as

Uli Fahrenberg. Higher-Dimensional Timed and Hybrid Automata. In LITES, Volume 8, Issue 2 (2022): Special Issue on Distributed Hybrid Systems. Leibniz Transactions on Embedded Systems, Volume 8, Issue 2, pp. 03:1-03:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@Article{fahrenberg:LITES.8.2.3,
  author =	{Fahrenberg, Uli},
  title =	{{Higher-Dimensional Timed and Hybrid Automata}},
  journal =	{Leibniz Transactions on Embedded Systems},
  pages =	{03:1--03:16},
  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.3},
  URN =		{urn:nbn:de:0030-drops-192951},
  doi =		{10.4230/LITES.8.2.3},
  annote =	{Keywords: timed automaton, higher-dimensional automaton, precubical set, real time, non-interleaving concurrency, hybrid automaton}
}
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/LITES-v004-i001-a004
How Is Your Satellite Doing? Battery Kinetics with Recharging and Uncertainty

Authors: Holger Hermanns, Jan Krčál, and Gilles Nies

Published in: LITES, Volume 4, Issue 1 (2017). Leibniz Transactions on Embedded Systems, Volume 4, Issue 1

Abstract
The kinetic battery model is a popular model of the dynamic behaviour of a conventional battery, useful to predict or optimize the time until battery depletion. The model however lacks certain obvious aspects of batteries in-the-wild, especially with respect to the effects of random influences and the behaviour when charging up to capacity limits.This paper considers the kinetic battery model with limited capacity in the context of piecewise constant yet random charging and discharging. We provide exact representations of the battery behaviour wherever possible, and otherwise develop safe approximations that bound the probability distribution of the battery state from above and below. The resulting model enables the time-dependent evaluation of the risk of battery depletion. This is demonstrated in an extensive dependability study of a nano satellite currently orbiting the earth.
Cite as

Holger Hermanns, Jan Krčál, and Gilles Nies. How Is Your Satellite Doing? Battery Kinetics with Recharging and Uncertainty. In LITES, Volume 4, Issue 1 (2017). Leibniz Transactions on Embedded Systems, Volume 4, Issue 1, pp. 04:1-04:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@Article{hermanns_et_al:LITES-v004-i001-a004,
  author =	{Hermanns, Holger and Kr\v{c}\'{a}l, Jan and Nies, Gilles},
  title =	{{How Is Your Satellite Doing? Battery Kinetics with Recharging and Uncertainty}},
  journal =	{Leibniz Transactions on Embedded Systems},
  pages =	{04:1--04:28},
  ISSN =	{2199-2002},
  year =	{2017},
  volume =	{4},
  number =	{1},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LITES-v004-i001-a004},
  URN =		{urn:nbn:de:0030-drops-192655},
  doi =		{10.4230/LITES-v004-i001-a004},
  annote =	{Keywords: Battery Power, Depletion Risk, Bounded Charging and Discharging, Stochastic Load, Distribution Bounds}
}
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}
}
  • Refine by Type
  • 15 Document/PDF
  • 7 Document/HTML
  • 1 Issue

  • Refine by Publication Year
  • 2 2026
  • 5 2025
  • 1 2023
  • 4 2022
  • 1 2021
  • Show More...

  • Refine by Author
  • 5 Abate, Alessandro
  • 3 Fahrenberg, Uli
  • 3 Fränzle, Martin
  • 1 Akshay, S.
  • 1 Amrane, Amazigh
  • Show More...

  • Refine by Series/Journal
  • 10 LIPIcs
  • 4 LITES
  • 1 DagRep

  • Refine by Classification
  • 3 Theory of computation → Probabilistic computation
  • 2 Computer systems organization → Embedded and cyber-physical systems
  • 2 Computing methodologies → Neural networks
  • 2 Theory of computation → Logic and verification
  • 2 Theory of computation → Program verification
  • Show More...

  • Refine by Keyword
  • 1 Analysis
  • 1 Battery Power
  • 1 Boolean equation systems
  • 1 Bounded Charging and Discharging
  • 1 Büchi acceptance
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact