Abstract
We introduce an approximate bisimulation-based framework that gives an upper bound of the Skorokhod metric between a switched system with delays and its delay-free model. To establish the approximate bisimulation relation, we rely on an incremental stability assumption. We showcase our framework using an example of a boost DC-DC converter. The obtained upper bound of the Skorokhod metric can be used to reduce the reachability analysis (or the safety controller synthesis) of the switched system with delays to that of the delay-free model.
The authors are supported by JST ERATO HASUO Metamathematics for Systems Design Project (No. JPMJER1603), and JSPS Grant-in-Aid No. 15KT0012. K.K. is supported by JSPS under JSPS Grants-in-Aid for JSPS Research Fellows No. 15J05580. The results of this paper are part of K.K.’s Ph.D. thesis [15].
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
- 2.
In the formalization of Sect. 2, the set P of modes is declared as \(\{1, \cdots , m\}\). Here we instead use \(P = \{{\textit{ON}}, {\textit{OFF}}\}\) for readability.
References
Abbas, H., Fainekos, G.E.: Towards composition of conformant systems. CoRR abs/1511.05273 (2015)
Abbas, H., Mittelmann, H.D., Fainekos, G.E.: Formal property verification in a conformance testing framework. In: Twelfth ACM/IEEE International Conference on Formal Methods and Models for Codesign, MEMOCODE 2014, Lausanne, Switzerland, 19–21 October 2014, pp. 155–164 (2014)
Angeli, D.: A Lyapunov approach to incremental stability properties. IEEE Trans. Autom. Control 47(3), 410–421 (2002)
Beccuti, A.G., Papafotiou, G., Morari, M.: Optimal control of the boost dc-dc converter. In: Proceedings of the 44th IEEE Conference on Decision and Control, pp. 4457–4462, December 2005
Borri, A., Pola, G., Di Benedetto, M.D.: A symbolic approach to the design of nonlinear networked control systems. In: Proceedings of the 15th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2012, pp. 255–264. ACM, New York (2012)
Davoren, J.M.: Epsilon-tubes and generalized Skorokhod metrics for hybrid paths spaces. In: Majumdar, R., Tabuada, P. (eds.) HSCC 2009. LNCS, vol. 5469, pp. 135–149. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-00602-9_10
Deshmukh, J.V., Majumdar, R., Prabhu, V.S.: Quantifying conformance using the Skorokhod metric. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9207, pp. 234–250. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21668-3_14
Frehse, G., et al.: SpaceEx: scalable verification of hybrid systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 379–395. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22110-1_30
Girard, A.: Controller synthesis for safety and reachability via approximate bisimulation. Automatica 48(5), 947–953 (2012)
Girard, A., Pappas, G.J.: Approximation metrics for discrete and continuous systems. IEEE Trans. Autom. Control 52(5), 782–798 (2007)
Girard, A., Pappas, G.J.: Approximate bisimulation: a bridge between computer science and control theory. Eur. J. Control 17(5–6), 568–578 (2011)
Girard, A., Pola, G., Tabuada, P.: Approximately bisimilar symbolic models for incrementally stable switched systems. IEEE Trans. Autom. Control 55(1), 116–126 (2010)
Khatib, M.A., Girard, A., Dang, T.: Verification and synthesis of timing contracts for embedded controllers. In: Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control, HSCC 2016, Vienna, Austria, 12–14 April 2016, pp. 115–124 (2016)
Kido, K., Sedwards, S., Hasuo, I.: Bounding Errors Due to Switching Delays in Incrementally Stable Switched Systems (Extended Version). ArXiv e-prints, December 2017
Kido, K.: Reachability analysis of hybrid systems via predicate and relational abstraction. Ph.D. thesis, The University of Tokyo (2018)
Majumdar, R., Prabhu, V.S.: Computing the Skorokhod distance between polygonal traces. In: Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, HSCC 2015, pp. 199–208. ACM, New York (2015)
Majumdar, R., Prabhu, V.S.: Computing distances between reach flowpipes. In: Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control, HSCC 2016, pp. 267–276. ACM, New York (2016)
Pola, G., Girard, A., Tabuada, P.: Approximately bisimilar symbolic models for nonlinear control systems. Automatica 44(10), 2508–2516 (2008)
Pola, G., Pepe, P., Benedetto, M.D.D.: Alternating approximately bisimilar symbolic models for nonlinear control systems with unknown time-varying delays. In: Proceedings of the 49th IEEE Conference on Decision and Control, CDC 2010, Atlanta, Georgia, USA, 15–17 December 2010, pp. 7649–7654 (2010)
Ramadge, P.J., Wonham, W.M.: Supervisory control of a class of discrete event processes. SIAM J. Control Optim. 25(1), 206–230 (1987)
Zamani, M., Mazo Jr., M., Khaled, M., Abate, A.: Symbolic abstractions of networked control systems. IEEE Trans. Control Netw. Syst. PP(99), 1 (2017)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this paper
Cite this paper
Kido, K., Sedwards, S., Hasuo, I. (2019). Switching Delays and the Skorokhod Distance in Incrementally Stable Switched Systems. In: Chamberlain, R., Taha, W., Törngren, M. (eds) Cyber Physical Systems. Design, Modeling, and Evaluation. CyPhy 2017. Lecture Notes in Computer Science(), vol 11267. Springer, Cham. https://doi.org/10.1007/978-3-030-17910-6_9
Download citation
DOI: https://doi.org/10.1007/978-3-030-17910-6_9
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-17909-0
Online ISBN: 978-3-030-17910-6
eBook Packages: Computer ScienceComputer Science (R0)