Issue
Leibniz Transactions on Embedded Systems, Volume 8, Issue 2
LITES, Volume 8, Issue 2
-
Part of:
Volume:
LITES, Volume 8
Journal: Leibniz Transactions on Embedded Systems (LITES)
Special Issue
Special Issue on Distributed Hybrid SystemsEditors
Publication Details
- published at: 2022-12-07
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- DBLP: db/journals/lites/lites8
Access Numbers
- Detailed Access Statistics available here
-
Total Document Accesses (updated on a weekly basis):
0PDF Downloads
Documents
No documents found matching your filter selection.
Document
Complete Issue
LITES, Volume 8, Issue 2
Abstract
LITES, Volume 8, Issue 2
Cite as
LITES, Volume 8, Issue 2: Special Issue on Distributed Hybrid Systems, pp. 1-180, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@Article{LITES-v008-i002,
title = {{LITES, Volume 8, Issue 2}},
journal = {Leibniz Transactions on Embedded Systems},
pages = {1--180},
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-v008-i002},
doi = {10.4230/LITES-v008-i002},
annote = {Keywords: LITES, Volume 8, Issue 2}
}
Document
Introduction
Introduction to the Special Issue on Distributed Hybrid Systems
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
Safety Verification of Networked Control Systems by Complex Zonotopes
Abstract
Networked control systems (NCS) are widely used in real world applications because of their advantages, such as remote operability and reduced installation costs. However, they are prone to various inaccuracies in execution like delays, packet dropouts, inaccurate sensing and quantization errors. To ensure safety of NCS, their models have to be verified under the consideration of aforementioned uncertainties. In this paper, we tackle the problem of verifying safety of models of NCS under uncertain sampling time, inaccurate output measurement or estimation, and unknown disturbance input. Unbounded-time safety verification requires approximation of reachable sets by invariants, whose computation involves set operations. For uncertain linear dynamics, two important set operations for invariant computation are linear transformation and Minkowski sum operations. Zonotopes have the advantage that linear transformation and Minkowski sum operations can be efficiently approximated. However, they can not encode directions of convergence of trajectories along complex eigenvectors, which is closely related to encoding invariants. Therefore, we extend zonotopes to the complex valued domain by a representation called complex zonotope, which can capture contraction along complex eigenvectors for determining invariants. We prove a related mathematical result that in case of accurate feedback sampling, a complex zonotope will represent an invariant for a stable NCS. In addition, we propose an algorithm to verify the general case based on complex zonotopes, when there is uncertainty in sampling time and in input. We demonstrate the efficiency of our algorithm on benchmark examples and compare it with a state-of-the-art verification tool.
Cite as
Arvind Adimoolam and Thao Dang. Safety Verification of Networked Control Systems by Complex Zonotopes. In LITES, Volume 8, Issue 2 (2022): Special Issue on Distributed Hybrid Systems. Leibniz Transactions on Embedded Systems, Volume 8, Issue 2, pp. 01:1-01:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@Article{adimoolam_et_al:LITES.8.2.1,
author = {Adimoolam, Arvind and Dang, Thao},
title = {{Safety Verification of Networked Control Systems by Complex Zonotopes}},
journal = {Leibniz Transactions on Embedded Systems},
pages = {01:1--01:22},
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.1},
doi = {10.4230/LITES.8.2.1},
annote = {Keywords: Safety Verification, Networked Control System, Reachability Analysis, Complex Zonotope}
}
Document
Swarms of Mobile Robots: Towards Versatility with Safety
Abstract
We present Pactole, a formal framework to design and prove the correctness of protocols (or the impossibility of their existence) that target mobile robotic swarms. Unlike previous approaches, our methodology unifies in a single formalism the execution model, the problem specification, the protocol, and its proof of correctness. The Pactole framework makes use of the Coq proof assistant, and is specially targeted at protocol designers and problem specifiers, so that a common unambiguous language is used from the very early stages of protocol development. We stress the underlying framework design principles to enable high expressivity and modularity, and provide concrete examples about how the Pactole framework can be used to tackle actual problems, some previously addressed by the Distributed Computing community, but also new problems, while being certified correct.
Cite as
Pierre Courtieu, Lionel Rieg, Sébastien Tixeuil, and Xavier Urbain. Swarms of Mobile Robots: Towards Versatility with Safety. In LITES, Volume 8, Issue 2 (2022): Special Issue on Distributed Hybrid Systems. Leibniz Transactions on Embedded Systems, Volume 8, Issue 2, pp. 02:1-02:36, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@Article{courtieu_et_al:LITES.8.2.2,
author = {Courtieu, Pierre and Rieg, Lionel and Tixeuil, S\'{e}bastien and Urbain, Xavier},
title = {{Swarms of Mobile Robots: Towards Versatility with Safety}},
journal = {Leibniz Transactions on Embedded Systems},
pages = {02:1--02:36},
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.2},
doi = {10.4230/LITES.8.2.2},
annote = {Keywords: distributed algorithm, mobile autonomous robots, formal proof}
}
Document
Higher-Dimensional Timed and Hybrid Automata
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},
doi = {10.4230/LITES.8.2.3},
annote = {Keywords: timed automaton, higher-dimensional automaton, precubical set, real time, non-interleaving concurrency, hybrid automaton}
}
Document
A Hybrid Programming Language for Formal Modeling and Verification of Hybrid Systems
Abstract
Designing and modeling complex cyber-physical systems (CPS) faces the double challenge of combined discrete-continuous dynamics and concurrent behavior. Existing formal modeling and verification languages for CPS expose the underlying proof search technology. They lack high-level structuring elements and are not efficiently executable. The ensuing modeling gap renders formal CPS models hard to understand and to validate. We propose a high-level programming-based approach to formal modeling and verification of hybrid systems as a hybrid extension of an Active Objects language. Well-structured hybrid active programs and requirements allow automatic, reachability-preserving translation into differential dynamic logic, a logic for hybrid (discrete-continuous) programs. Verification is achieved by discharging the resulting formulas with the theorem prover KeYmaera X. We demonstrate the usability of our approach with case studies.
Cite as
Eduard Kamburjan, Stefan Mitsch, and Reiner Hähnle. A Hybrid Programming Language for Formal Modeling and Verification of Hybrid Systems. In LITES, Volume 8, Issue 2 (2022): Special Issue on Distributed Hybrid Systems. Leibniz Transactions on Embedded Systems, Volume 8, Issue 2, pp. 04:1-04:34, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@Article{kamburjan_et_al:LITES.8.2.4,
author = {Kamburjan, Eduard and Mitsch, Stefan and H\"{a}hnle, Reiner},
title = {{A Hybrid Programming Language for Formal Modeling and Verification of Hybrid Systems}},
journal = {Leibniz Transactions on Embedded Systems},
pages = {04:1--04:34},
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.4},
doi = {10.4230/LITES.8.2.4},
annote = {Keywords: Active Objects, Differential Dynamic Logic, Hybrid Systems}
}
Document
Bayesian Hybrid Automata: A Formal Model of Justified Belief in Interacting Hybrid Systems Subject to Imprecise Observation
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},
doi = {10.4230/LITES.8.2.5},
annote = {Keywords: }
}
Document
From Dissipativity Theory to Compositional Construction of Control Barrier Certificates
Abstract
This paper proposes a compositional framework based on dissipativity approaches to construct control barrier certificates for networks of continuous-time stochastic hybrid systems. The proposed scheme leverages the structure of the interconnection topology and a notion of so-called control storage certificates to construct control barrier certificates compositionally. By utilizing those certificates, one can compositionally synthesize state-feedback controllers for interconnected systems enforcing safety specifications over a finite-time horizon. In particular, we leverage dissipativity-type compositionality conditions to construct control barrier certificates for interconnected systems based on corresponding control storage certificates computed for subsystems. Using those constructed control barrier certificates, one can quantify upper bounds on probabilities that interconnected systems reach certain unsafe regions in finite-time horizons. We employ a systematic technique based on the sum-of-squares optimization program to search for storage certificates of subsystems together with their corresponding safety controllers. We demonstrate our proposed results by applying them to a temperature regulation in a circular building containing 1000 rooms. To show the applicability of our approaches to dense networks, we also apply our proposed techniques to a fully-interconnected network.
Cite as
Ameneh Nejati and Majid Zamani. From Dissipativity Theory to Compositional Construction of Control Barrier Certificates. In LITES, Volume 8, Issue 2 (2022): Special Issue on Distributed Hybrid Systems. Leibniz Transactions on Embedded Systems, Volume 8, Issue 2, pp. 06:1-06:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@Article{nejati_et_al:LITES.8.2.6,
author = {Nejati, Ameneh and Zamani, Majid},
title = {{From Dissipativity Theory to Compositional Construction of Control Barrier Certificates}},
journal = {Leibniz Transactions on Embedded Systems},
pages = {06:1--06:17},
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.6},
doi = {10.4230/LITES.8.2.6},
annote = {Keywords: Compositional barrier certificates, Stochastic hybrid systems, Dissipativity theory, Large-scale networks, Formal controller synthesis}
}
Document
Real-Time Verification for Distributed Cyber-Physical Systems
Abstract
Safety-critical distributed cyber-physical systems (CPSs) have been found in a wide range of applications. Notably, they have displayed a great deal of utility in intelligent transportation, where autonomous vehicles communicate and cooperate with each other via a high-speed communication network. Such systems require an ability to identify maneuvers in real-time that cause dangerous circumstances and ensure the implementation always meets safety-critical requirements. In this paper, we propose a real-time decentralized reachability approach for safety verification of a distributed multi-agent CPS with the underlying assumption that all agents are time-synchronized with a low degree of error. In the proposed approach, each agent periodically computes its local reachable set and exchanges this reachable set with the other agents with the goal of verifying the system safety. Our method, implemented in Java, takes advantages of the timing information and the reachable set information that are available in the exchanged messages to reason about the safety of the whole system in a decentralized manner. Any particular agent can also perform local safety verification tasks based on their local clocks by analyzing the messages it receives. We applied the proposed method to verify, in real-time, the safety properties of a group of quadcopters performing a distributed search mission.
Cite as
Hoang-Dung Tran, Luan Viet Nguyen, Patrick Musau, Weiming Xiang, and Taylor T. Johnson. Real-Time Verification for Distributed Cyber-Physical Systems. In LITES, Volume 8, Issue 2 (2022): Special Issue on Distributed Hybrid Systems. Leibniz Transactions on Embedded Systems, Volume 8, Issue 2, pp. 07:1-07:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@Article{tran_et_al:LITES.8.2.7,
author = {Tran, Hoang-Dung and Nguyen, Luan Viet and Musau, Patrick and Xiang, Weiming and Johnson, Taylor T.},
title = {{Real-Time Verification for Distributed Cyber-Physical Systems}},
journal = {Leibniz Transactions on Embedded Systems},
pages = {07:1--07:19},
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.7},
doi = {10.4230/LITES.8.2.7},
annote = {Keywords: Verification, Reachability Analysis, Distributed Cyber-Physical Systems}
}