Bineet Ghosh
Abstract
Reachable set computation is one of the primary techniques for safety verification of linear dynamical systems. In reality the underlying dynamics have uncertainties like parameter variations or modeling uncertainties. Therefore, the reachable set computation must consider the uncertainties in the dynamics to be useful i.e. the computed reachable set should be over or under approximation if not exact. This paper presents a technique to compute reachable set of linear dynamical systems with uncertainties. First, we introduce a construct called support of a matrix. Using this construct, we present a set of sufficient conditions for which reachable set for uncertain linear system can be computed efficiently; and safety verification can be performed using bi-linear programming. Finally, given a linear dynamical system, we compute robust reachable set, which accounts for all possible uncertainties that can be handled by the sufficient conditions presented. Experimental evaluation on benchmarks reveal that our algorithm is computationally very efficient.
- Matthias Althoff, Bruce H. Krogh, and Olaf Stursberg. 2011. Analyzing reachability of linear dynamic systems with parametric uncertainties. In Modeling, Design, and Simulation of Systems with Uncertainties. Springer, 69--94.Google Scholar
- Matthias Althoff, Olaf Stursberg, and Martin Buss. 2007. Reachability analysis of linear systems with uncertain parameters and inputs. In 2007 46th IEEE Conference on Decision and Control. IEEE, 726--732.Google ScholarCross Ref
- Matthias Althoff, Olaf Stursberg, and Martin Buss. 2008. Reachability analysis of nonlinear systems with uncertain parameters using conservative linearization. In Proc. of the 47th IEEE Conference on Decision and Control.Google ScholarCross Ref
- Hongxu Chen, Sayan Mitra, and Guangyu Tian. 2014. Motor-transmission drive system: A benchmark example for safety verification. In ARCH@CPSWeek. 9--18.Google Scholar
- Xin Chen, Erika Ábrahám, and Sriram Sankaranarayanan. 2013. Flow*: An analyzer for non-linear hybrid systems. In Computer Aided Verification - 25th International Conference, CAV 2013. Proceedings.Google Scholar
- Alongkrit Chutinan and Bruce H. Krogh. 2003. Computational techniques for hybrid system verification. IEEE Transactions on Automatic Control 48, 1 (2003), 64--75.Google ScholarCross Ref
- C. Combastel and S. A. Raka. 2011. On computing envelopes for discrete-time linear systems with affine parametric uncertainties and bounded inputs. IFAC Proceedings Volumes 44, 1 (2011), 4525--4533. 18th IFAC World Congress.Google Scholar
- Tommaso Dreossi. 2017. Sapo: Reachability computation and parameter synthesis of polynomial dynamical systems. In Proceedings of the 20th International Conference on Hybrid Systems: Computation and Control (HSCC’17).Google ScholarDigital Library
- Parasara Sridhar Duggirala, Sayan Mitra, Mahesh Viswanathan, and Matthew Potok. 2015. C2E2: A verification tool for stateflow models. In 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'15).Google ScholarDigital Library
- Parasara Sridhar Duggirala and Mahesh Viswanathan. 2016. Parsimonious, simulation based verification of linear systems. In International Conference on Computer Aided Verification. Springer, 477--494.Google ScholarCross Ref
- Goran Frehse. 2005. PHAVer: Algorithmic verification of hybrid systems past HyTech. In International Workshop on Hybrid Systems: Computation and Control. Springer, 258--273.Google ScholarDigital Library
- Goran Frehse, Colas Le Guernic, Alexandre Donzé, Scott Cotton, Rajarshi Ray, Olivier Lebeltel, Rodolfo Ripado, Antoine Girard, Thao Dang, and Oded Maler. 2011. SpaceEx: Scalable verification of hybrid systems. In International Conference on Computer Aided Verification. Springer, 379--395.Google ScholarDigital Library
- Mituhiro Fukuda and Masakazu Kojima. 2001. Branch-and-cut algorithms for the bilinear matrix inequality eigenvalue problem. Computational Optimization and Applications 19, 1 (2001), 79--105.Google ScholarDigital Library
- Victor Gan, Guy A. Dumont, and Ian Mitchell. 2014. Benchmark problem: A PK/PD model and safety constraints for anesthesia delivery. In ARCH@CPSWeek. 1--8.Google Scholar
- Antoine Girard. 2005. Reachability of uncertain linear systems using zonotopes. In International Workshop on Hybrid Systems: Computation and Control. Springer, 291--305.Google ScholarDigital Library
- Keat-Choon Goh, Michael G. Safonov, and George P. Papavassilopoulos. 1995. Global optimization for the biaffine matrix inequality problem. Journal of Global Optimization 7, 4 (1995), 365--380.Google ScholarCross Ref
- Michael Green and David J. N. Limebeer. 2012. Linear Robust Control. Courier Corporation.Google Scholar
- Shahab Kaynama and C. Tomlin. 2014. Benchmark: Flight envelope protection in autonomous quadrotors. In Workshop on Applied Verification for Continuous and Hybrid Systems.Google Scholar
- Pramod P. Khargonekar, Ian R. Petersen, and Kemin Zhou. 1990. Robust stabilization of uncertain linear systems: Quadratic stabilizability and H/sup infinity/control theory. IEEE Trans. Automat. Control 35, 3 (1990), 356--361.Google ScholarCross Ref
- Olaf Knüppel. 1994. PROFIL/BIAS—a fast interval library. Computing 53, 3--4 (1994), 277--287.Google ScholarCross Ref
- Alexander B. Kurzhanski and Pravin Varaiya. 2000. Ellipsoidal techniques for reachability analysis: Internal approximation. Systems 8 Control Letters 41, 3 (2000), 201--211.Google Scholar
- Ratan Lal and Pavithra Prabhakar. 2015. Bounded error flowpipe computation of parameterized linear systems. In Proceedings of the 12th International Conference on Embedded Software. IEEE Press, 237--246.Google ScholarDigital Library
- Ibtissem Ben Makhlouf and Stefan Kowalewski. 2014. Networked cooperative platoon of vehicles for testing methods and verification tools. In ARCH@CPSWeek. 37--42.Google Scholar
- Pierre-Jean Meyer, Alex Devonport, and Murat Arcak. 2019. TIRA: Toolbox for interval reachability analysis. arXiv preprint arXiv:1902.05204 (2019).Google Scholar
- Ramon E. Moore. 1979. Methods and Applications of Interval Analysis. Vol. 2. Siam.Google ScholarDigital Library
- Mohamed Serry and Gunther Reissig. 2018. Hyper-rectangular over-approximations of reachable sets for linear uncertain systems. In 2018 IEEE Conference on Decision and Control (CDC). IEEE, 6275--6282.Google ScholarDigital Library
- Kemin Zhou, John Comstock Doyle, Keith Glover, et al. 1996. Robust and Optimal Control. Vol. 40. Prentice hall New Jersey.Google Scholar
Index Terms
- Robust Reachable Set: Accounting for Uncertainties in Linear Dynamical Systems
Recommendations
Reachable set computation for uncertain time-varying linear systems
HSCC '11: Proceedings of the 14th international conference on Hybrid systems: computation and controlThis paper presents a method for using set-based approximations to the Peano-Baker series to compute overapproximations of reachable sets for linear systems with uncertain, time-varying parameters and inputs. Alternative representations for sets of ...
Handling loops in bounded model checking of C programs via k-induction
The first attempts to apply the k-induction method to software verification are only recent. In this paper, we present a novel proof by induction algorithm, which is built on the top of a symbolic context-bounded model checker and uses an iterative ...
SBMC: symmetric bounded model checking
VECoS'10: Proceedings of the Fourth international conference on Verification and Evaluation of Computer and Communication SystemsThis paper deals with systems verification techniques, using Bounded Model Checking (BMC). We present a new approach that combines BMC with symmetry reduction techniques. Our goal is to reduce the number of transition sequences, which can be handled by ...
Comments