Advertisement

Switching Delays and the Skorokhod Distance in Incrementally Stable Switched Systems

  • Kengo Kido
  • Sean Sedwards
  • Ichiro HasuoEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11267)

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.

References

  1. 1.
    Abbas, H., Fainekos, G.E.: Towards composition of conformant systems. CoRR abs/1511.05273 (2015)Google Scholar
  2. 2.
    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)Google Scholar
  3. 3.
    Angeli, D.: A Lyapunov approach to incremental stability properties. IEEE Trans. Autom. Control 47(3), 410–421 (2002)MathSciNetCrossRefGoogle Scholar
  4. 4.
    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 2005Google Scholar
  5. 5.
    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)Google Scholar
  6. 6.
    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_10CrossRefzbMATHGoogle Scholar
  7. 7.
    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_14CrossRefGoogle Scholar
  8. 8.
    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_30CrossRefGoogle Scholar
  9. 9.
    Girard, A.: Controller synthesis for safety and reachability via approximate bisimulation. Automatica 48(5), 947–953 (2012)MathSciNetCrossRefGoogle Scholar
  10. 10.
    Girard, A., Pappas, G.J.: Approximation metrics for discrete and continuous systems. IEEE Trans. Autom. Control 52(5), 782–798 (2007)MathSciNetCrossRefGoogle Scholar
  11. 11.
    Girard, A., Pappas, G.J.: Approximate bisimulation: a bridge between computer science and control theory. Eur. J. Control 17(5–6), 568–578 (2011)MathSciNetCrossRefGoogle Scholar
  12. 12.
    Girard, A., Pola, G., Tabuada, P.: Approximately bisimilar symbolic models for incrementally stable switched systems. IEEE Trans. Autom. Control 55(1), 116–126 (2010)MathSciNetCrossRefGoogle Scholar
  13. 13.
    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)Google Scholar
  14. 14.
    Kido, K., Sedwards, S., Hasuo, I.: Bounding Errors Due to Switching Delays in Incrementally Stable Switched Systems (Extended Version). ArXiv e-prints, December 2017Google Scholar
  15. 15.
    Kido, K.: Reachability analysis of hybrid systems via predicate and relational abstraction. Ph.D. thesis, The University of Tokyo (2018)Google Scholar
  16. 16.
    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)Google Scholar
  17. 17.
    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)Google Scholar
  18. 18.
    Pola, G., Girard, A., Tabuada, P.: Approximately bisimilar symbolic models for nonlinear control systems. Automatica 44(10), 2508–2516 (2008)MathSciNetCrossRefGoogle Scholar
  19. 19.
    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)Google Scholar
  20. 20.
    Ramadge, P.J., Wonham, W.M.: Supervisory control of a class of discrete event processes. SIAM J. Control Optim. 25(1), 206–230 (1987)MathSciNetCrossRefGoogle Scholar
  21. 21.
    Zamani, M., Mazo Jr., M., Khaled, M., Abate, A.: Symbolic abstractions of networked control systems. IEEE Trans. Control Netw. Syst. PP(99), 1 (2017)Google Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  1. 1.University of TokyoTokyoJapan
  2. 2.JSPS Research FellowTokyoJapan
  3. 3.University of WaterlooWaterlooCanada
  4. 4.National Institute of InformaticsTokyoJapan
  5. 5.The Graduate University for Advanced Studies (SOKENDAI)TokyoJapan

Personalised recommendations