Advertisement

Linear Temporal Logic Satisfaction in Adversarial Environments Using Secure Control Barrier Certificates

  • Bhaskar RamasubramanianEmail author
  • Luyao Niu
  • Andrew Clark
  • Linda Bushnell
  • Radha Poovendran
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11836)

Abstract

This paper studies the satisfaction of a class of temporal properties for cyber-physical systems (CPSs) over a finite-time horizon in the presence of an adversary, in an environment described by discrete-time dynamics. The temporal logic specification is given in \(safe-LTL_F\), a fragment of linear temporal logic over traces of finite length. The interaction of the CPS with the adversary is modeled as a two-player zero-sum discrete-time dynamic stochastic game with the CPS as defender. We formulate a dynamic programming based approach to determine a stationary defender policy that maximizes the probability of satisfaction of a \(safe-LTL_F\) formula over a finite time-horizon under any stationary adversary policy. We introduce secure control barrier certificates (S-CBCs), a generalization of barrier certificates and control barrier certificates that accounts for the presence of an adversary, and use S-CBCs to provide a lower bound on the above satisfaction probability. When the dynamics of the evolution of the system state has a specific underlying structure, we present a way to determine an S-CBC as a polynomial in the state variables using sum-of-squares optimization. An illustrative example demonstrates our approach.

Keywords

Linear temporal logic \(safe-LTL_F\) Dynamic programming Secure control barrier certificate Sum-of-squares optimization 

References

  1. 1.
    Abate, A., Prandini, M., Lygeros, J., Sastry, S.: Probabilistic reachability and safety for controlled discrete time stochastic hybrid systems. Automatica 44(11), 2724–2734 (2008)MathSciNetCrossRefGoogle Scholar
  2. 2.
    Ahmadi, M., Jansen, N., Wu, B., Topcu, U.: Control theory meets POMDPs: A hybrid systems approach. arXiv preprint arXiv:1905.08095 (2019)
  3. 3.
    Ahmadi, M., Wu, B., Lin, H., Topcu, U.: Privacy verification in POMDPs via barrier certificates. In: IEEE Conference on Decision and Control, pp. 5610–5615 (2018)Google Scholar
  4. 4.
    Alur, R., Feder, T., Henzinger, T.A.: The benefits of relaxing punctuality. J. ACM 43(1), 116–146 (1996)MathSciNetCrossRefGoogle Scholar
  5. 5.
    Ames, A.D., Coogan, S., Egerstedt, M., Notomista, G., Sreenath, K., Tabuada, P.: Control barrier functions: Theory and applications. In: European Control Conference, pp. 3420–3431 (2019)Google Scholar
  6. 6.
    Ames, A.D., Xu, X., Grizzle, J.W., Tabuada, P.: Control barrier function based quadratic programs for safety critical systems. IEEE Trans. Autom. Control 62(8), 3861–3876 (2016)MathSciNetCrossRefGoogle Scholar
  7. 7.
    Başar, T., Olsder, G.J.: Dynamic Noncooperative Game Theory, vol. 23. SIAM, Philadelphia (1999)zbMATHGoogle Scholar
  8. 8.
    Baheti, R., Gill, H.: Cyber-physical systems. Impact Control Technol. 12(1), 161–166 (2011)Google Scholar
  9. 9.
    Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, Cambridge (2008)zbMATHGoogle Scholar
  10. 10.
    Belta, C., Yordanov, B., Aydin Gol, E.: Formal Methods for Discrete-Time Dynamical Systems. SSDC, vol. 89. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-50763-7CrossRefzbMATHGoogle Scholar
  11. 11.
    Bertsekas, D.P.: Dynamic Programming and Optimal Control, Volumes I and II, 4th edn. Athena Scientific, Nashua (2015)Google Scholar
  12. 12.
    Bouyer, P., Laroussinie, F., Markey, N., Ouaknine, J., Worrell, J.: Timed temporal logics. In: Aceto, L., Bacci, G., Bacci, G., Ingólfsdóttir, A., Legay, A., Mardare, R. (eds.) Models, Algorithms, Logics and Tools. LNCS, vol. 10460, pp. 211–230. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-63121-9_11CrossRefGoogle Scholar
  13. 13.
    Breton, M., Alj, A., Haurie, A.: Sequential Stackelberg equilibria in two-person games. J. Optim. Theory Appl. 59(1), 71–97 (1988)MathSciNetCrossRefGoogle Scholar
  14. 14.
    Chow, C.S., Tsitsiklis, J.N.: An optimal one-way multigrid algorithm for discrete-time stochastic control. IEEE Trans. Autom. Control 36(8), 898–914 (1991)MathSciNetCrossRefGoogle Scholar
  15. 15.
    Cimatti, A., Clarke, E., Giunchiglia, F., Roveri, M.: NuSMV: A new symbolic model verifier. In: Halbwachs, N., Peled, D. (eds.) CAV 1999. LNCS, vol. 1633, pp. 495–499. Springer, Heidelberg (1999).  https://doi.org/10.1007/3-540-48683-6_44CrossRefGoogle Scholar
  16. 16.
    De Giacomo, G., Vardi, M.: Synthesis for LTL and LDL on finite traces. Int. Joint Conf. Artif. Intell. 15, 1558–1564 (2015)Google Scholar
  17. 17.
    De Giacomo, G., Vardi, M.Y.: Linear temporal logic and linear dynamic logic on finite traces. In: International Joint Conference on Artificial Intelligence, pp. 854–860 (2013)Google Scholar
  18. 18.
    Ding, J., Kamgarpour, M., Summers, S., Abate, A., Lygeros, J., Tomlin, C.: A stochastic games framework for verification and control of discrete time stochastic hybrid systems. Automatica 49(9), 2665–2674 (2013)MathSciNetCrossRefGoogle Scholar
  19. 19.
    Ding, X., Smith, S.L., Belta, C., Rus, D.: Optimal control of MDPs with linear temporal logic constraints. IEEE Trans. Autom. Control 59(5), 1244–1257 (2014)CrossRefGoogle Scholar
  20. 20.
    Farwell, J.P., Rohozinski, R.: Stuxnet and the future of cyber war. Survival 53(1), 23–40 (2011)CrossRefGoogle Scholar
  21. 21.
    Gordon, G.J.: Approximate solutions to Markov decision processes. School of Computer Science, Carnegie-Mellon University, Pittsburgh, PA, Technical report (1999)Google Scholar
  22. 22.
    Jagtap, P., Soudjani, S., Zamani, M.: Temporal logic verification of stochastic systems using barrier certificates. In: Lahiri, S.K., Wang, C. (eds.) ATVA 2018. LNCS, vol. 11138, pp. 177–193. Springer, Cham (2018).  https://doi.org/10.1007/978-3-030-01090-4_11CrossRefGoogle Scholar
  23. 23.
    Jagtap, P., Soudjani, S., Zamani, M.: Formal synthesis of stochastic systems via control barrier certificates. arXiv preprint arXiv:1905.04585 (2019)
  24. 24.
    Kolathaya, S., Ames, A.D.: Input-to-state safety with control barrier functions. Control Syst. Lett. 3(1), 108–113 (2018)CrossRefGoogle Scholar
  25. 25.
    Křetínský, J., Meggendorfer, T., Sickert, S., Ziegler, C.: Rabinizer 4: From LTL to your favourite deterministic automaton. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10981, pp. 567–577. Springer, Cham (2018).  https://doi.org/10.1007/978-3-319-96145-3_30CrossRefGoogle Scholar
  26. 26.
    Kupferman, O., Vardi, M.Y.: Model checking of safety properties. In: Halbwachs, N., Peled, D. (eds.) CAV 1999. LNCS, vol. 1633, pp. 172–183. Springer, Heidelberg (1999).  https://doi.org/10.1007/3-540-48683-6_17CrossRefGoogle Scholar
  27. 27.
    Kushner, H.J.: Stochastic Stability and Control. Academic Press, Cambridge (1967)zbMATHGoogle Scholar
  28. 28.
    Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: Verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585–591. Springer, Heidelberg (2011).  https://doi.org/10.1007/978-3-642-22110-1_47CrossRefGoogle Scholar
  29. 29.
    Lafferriere, G., Pappas, G.J., Yovine, S.: Symbolic reachability computation for families of linear vector fields. J. Symb. Comput. 32(3), 231–253 (2001)MathSciNetCrossRefGoogle Scholar
  30. 30.
    Lindemann, L., Dimarogonas, D.V.: Control barrier functions for signal temporal logic tasks. IEEE Control Syst. Lett. 3(1), 96–101 (2019)CrossRefGoogle Scholar
  31. 31.
    Maler, O., Nickovic, D.: Monitoring temporal properties of continuous signals. In: Lakhnech, Y., Yovine, S. (eds.) FORMATS/FTRTFT -2004. LNCS, vol. 3253, pp. 152–166. Springer, Heidelberg (2004).  https://doi.org/10.1007/978-3-540-30206-3_12CrossRefzbMATHGoogle Scholar
  32. 32.
    Niu, L., Clark, A.: Secure control under LTL constraints. In: IEEE American Control Conference, pp. 3544–3551 (2018)Google Scholar
  33. 33.
    Niu, L., Li, Z., Clark, A.: LQG reference tracking with safety and reachability guarantees under false data injection attacks. In: IEEE American Control Conference, pp. 2950–2957 (2019)Google Scholar
  34. 34.
    Parrilo, P.A.: Semidefinite programming relaxations for semialgebraic problems. Math. Programm. 96(2), 293–320 (2003)MathSciNetCrossRefGoogle Scholar
  35. 35.
    Pola, G., Manes, C., van der Schaft, A.J., Di Benedetto, M.D.: Bisimulation equivalence of discrete-time stochastic linear control systems. IEEE Trans. Autom. Control 63(7), 1897–1912 (2017)MathSciNetCrossRefGoogle Scholar
  36. 36.
    Prajna, S., Jadbabaie, A., Pappas, G.J.: A framework for worst-case and stochastic safety verification using barrier certificates. Trans. Autom. Control 52(8), 1415–1428 (2007)MathSciNetCrossRefGoogle Scholar
  37. 37.
    Prajna, S., Papachristodoulou, A., Parrilo, P.A.: Introducing SOSTOOLS: A general purpose sum of squares programming solver. In: IEEE Conference on Decision and Control, vol. 1, pp. 741–746 (2002)Google Scholar
  38. 38.
    Puterman, M.L.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley, Hoboken (2014)zbMATHGoogle Scholar
  39. 39.
    Ramasubramanian, B., Clark, A., Bushnell, L., Poovendran, R.: Secure control under partial observability under temporal logic constraints. In: IEEE American Control Conference, pp. 1181–1188 (2019)Google Scholar
  40. 40.
    Saha, I., Ramaithitima, R., Kumar, V., Pappas, G.J., Seshia, S.A.: Automated composition of motion primitives for multi-robot systems from safe LTL specifications. In: Proceedings of International Conference on Intelligent Robots and Systems, pp. 1525–1532 (2014)Google Scholar
  41. 41.
    Santoyo, C., Dutreix, M., Coogan, S.: Verification and control for finite-time safety of stochastic systems via barrier functions. In: IEEE Conference on Control Technology and Applications (2019)Google Scholar
  42. 42.
    Sharan, R., Burdick, J.: Finite state control of POMDPs with LTL specifications. In: IEEE American Control Conference, pp. 501–508 (2014)Google Scholar
  43. 43.
    Shoukry, Y., Martin, P., Tabuada, P., Srivastava, M.: Non-invasive spoofing attacks for anti-lock braking systems. In: Bertoni, G., Coron, J.-S. (eds.) CHES 2013. LNCS, vol. 8086, pp. 55–72. Springer, Heidelberg (2013).  https://doi.org/10.1007/978-3-642-40349-1_4CrossRefGoogle Scholar
  44. 44.
    Slay, J., Miller, M.: Lessons learned from the maroochy water breach. In: Goetz, E., Shenoi, S. (eds.) ICCIP 2007. IIFIP, vol. 253, pp. 73–82. Springer, Boston, MA (2008).  https://doi.org/10.1007/978-0-387-75462-8_6CrossRefGoogle Scholar
  45. 45.
    Steinhardt, J., Tedrake, R.: Finite-time regional verification of stochastic non-linear systems. Int. J. Robot. Res. 31(7), 901–923 (2012)CrossRefGoogle Scholar
  46. 46.
    Sullivan, J.E., Kamensky, D.: How cyber-attacks in Ukraine show the vulnerability of the US power grid. Electr. J. 30(3), 30–35 (2017)CrossRefGoogle Scholar
  47. 47.
    Tarjan, R.: Depth-first search and linear graph algorithms. SIAM J. Comput. 1(2), 146–160 (1972)MathSciNetCrossRefGoogle Scholar
  48. 48.
    Toh, K.C., Todd, M.J., Tütüncü, R.H.: SDPT3: A MATLAB software package for semidefinite programming. Optim. Methods Softw. 11, 545–581 (1999)MathSciNetCrossRefGoogle Scholar
  49. 49.
    Wongpiromsarn, T., Topcu, U., Lamperski, A.: Automata theory meets barrier certificates: Temporal logic verification of nonlinear systems. IEEE Trans. Autom. Control 61(11), 3344–3355 (2015)MathSciNetCrossRefGoogle Scholar
  50. 50.
    Yang, I.: A dynamic game approach to distributionally robust safety specifications for stochastic systems. Automatica 94, 94–101 (2018)MathSciNetCrossRefGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  • Bhaskar Ramasubramanian
    • 1
    Email author
  • Luyao Niu
    • 2
  • Andrew Clark
    • 2
  • Linda Bushnell
    • 1
  • Radha Poovendran
    • 1
  1. 1.Department of Electrical and Computer EngineeringUniversity of WashingtonSeattleUSA
  2. 2.Department of Electrical and Computer EngineeringWorcester Polytechnic InstituteWorcesterUSA

Personalised recommendations