Vol. 8 No. 2 (2022): Special Issue on Distributed Hybrid Systems
Special Issue on Distributed Hybrid Systems

Safety Verification of Networked Control Systems by Complex Zonotopes

Arvind Adimoolam
Indian Institute of Technology Kanpur, Rajeev Motwani Building, Kalyanpur, Kanpur, India
Thao Dang
VERIMAG, CNRS/University Grenoble Alpes, Bâtiment IMAG, 700 Avenue Centrale, Grenoble, France

Published 2022-12-07


  • Safety Verification,
  • Networked Control System,
  • Reachability Analysis,
  • Complex Zonotope

How to Cite

Adimoolam, A. and Dang, T. 2022. Safety Verification of Networked Control Systems by Complex Zonotopes. Leibniz Transactions on Embedded Systems. 8, 2 (Dec. 2022), 01:1–01:22. DOI:https://doi.org/10.4230/LITES.8.2.1.


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.