×

Linear temporal logic satisfaction in adversarial environments using secure control barrier certificates. (English) Zbl 1440.68038

Alpcan, Tansu (ed.) et al., Decision and game theory for security. 10th international conference, GameSec 2019, Stockholm, Sweden, October 30 – November 1, 2019. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 11836, 385-403 (2019).
Summary: 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.
For the entire collection see [Zbl 1428.68003].

MSC:

68M25 Computer security
68Q60 Specification and verification (program logics, model checking, etc.)
91A80 Applications of game theory

Software:

PRISM; NuSMV; SDPT3; Sostools
PDFBibTeX XMLCite
Full Text: DOI arXiv

References:

[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) · Zbl 1152.93051 · doi:10.1016/j.automatica.2008.03.027
[2] Ahmadi, M., Jansen, N., Wu, B., Topcu, U.: Control theory meets POMDPs: A hybrid systems approach. arXiv preprint arXiv:1905.08095 (2019)
[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)
[4] Alur, R., Feder, T., Henzinger, T.A.: The benefits of relaxing punctuality. J. ACM 43(1), 116-146 (1996) · Zbl 0882.68021 · doi:10.1145/227595.227602
[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)
[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) · Zbl 1373.90092 · doi:10.1109/TAC.2016.2638961
[7] Başar, T., Olsder, G.J.: Dynamic Noncooperative Game Theory, vol. 23. SIAM, Philadelphia (1999) · Zbl 0946.91001
[8] Baheti, R., Gill, H.: Cyber-physical systems. Impact Control Technol. 12(1), 161-166 (2011)
[9] Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, Cambridge (2008) · Zbl 1179.68076
[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-7 · Zbl 1409.93003 · doi:10.1007/978-3-319-50763-7
[11] Bertsekas, D.P.: Dynamic Programming and Optimal Control, Volumes I and II, 4th edn. Athena Scientific, Nashua (2015)
[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_11 · Zbl 1431.03032 · doi:10.1007/978-3-319-63121-9_11
[13] Breton, M., Alj, A., Haurie, A.: Sequential Stackelberg equilibria in two-person games. J. Optim. Theory Appl. 59(1), 71-97 (1988) · Zbl 0631.90100 · doi:10.1007/BF00939867
[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) · Zbl 0752.93078 · doi:10.1109/9.133184
[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_44 · Zbl 1046.68587 · doi:10.1007/3-540-48683-6_44
[16] De Giacomo, G., Vardi, M.: Synthesis for LTL and LDL on finite traces. Int. Joint Conf. Artif. Intell. 15, 1558-1564 (2015)
[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)
[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) · Zbl 1364.93857 · doi:10.1016/j.automatica.2013.05.025
[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) · Zbl 1360.90276 · doi:10.1109/TAC.2014.2298143
[20] Farwell, J.P., Rohozinski, R.: Stuxnet and the future of cyber war. Survival 53(1), 23-40 (2011) · doi:10.1080/00396338.2011.555586
[21] Gordon, G.J.: Approximate solutions to Markov decision processes. School of Computer Science, Carnegie-Mellon University, Pittsburgh, PA, Technical report (1999)
[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_11 · Zbl 1517.68242 · doi:10.1007/978-3-030-01090-4_11
[23] Jagtap, P., Soudjani, S., Zamani, M.: Formal synthesis of stochastic systems via control barrier certificates. arXiv preprint arXiv:1905.04585 (2019)
[24] Kolathaya, S., Ames, A.D.: Input-to-state safety with control barrier functions. Control Syst. Lett. 3(1), 108-113 (2018) · doi:10.1109/LCSYS.2018.2853698
[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_30 · doi:10.1007/978-3-319-96145-3_30
[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_17 · Zbl 1046.68597 · doi:10.1007/3-540-48683-6_17
[27] Kushner, H.J.: Stochastic Stability and Control. Academic Press, Cambridge (1967) · Zbl 0244.93065
[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_47 · doi:10.1007/978-3-642-22110-1_47
[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) · Zbl 0983.93004 · doi:10.1006/jsco.2001.0472
[30] Lindemann, L., Dimarogonas, D.V.: Control barrier functions for signal temporal logic tasks. IEEE Control Syst. Lett. 3(1), 96-101 (2019) · doi:10.1109/LCSYS.2018.2853182
[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_12 · Zbl 1109.68518 · doi:10.1007/978-3-540-30206-3_12
[32] Niu, L., Clark, A.: Secure control under LTL constraints. In: IEEE American Control Conference, pp. 3544-3551 (2018)
[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)
[34] Parrilo, P.A.: Semidefinite programming relaxations for semialgebraic problems. Math. Programm. 96(2), 293-320 (2003) · Zbl 1043.14018 · doi:10.1007/s10107-003-0387-5
[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) · Zbl 1423.93367 · doi:10.1109/TAC.2017.2760515
[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) · Zbl 1366.93711 · doi:10.1109/TAC.2007.902736
[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)
[38] Puterman, M.L.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley, Hoboken (2014) · Zbl 0829.90134
[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)
[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)
[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)
[42] Sharan, R., Burdick, J.: Finite state control of POMDPs with LTL specifications. In: IEEE American Control Conference, pp. 501-508 (2014)
[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_4 · doi:10.1007/978-3-642-40349-1_4
[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_6 · doi:10.1007/978-0-387-75462-8_6
[45] Steinhardt, J., Tedrake, R.: Finite-time regional verification of stochastic non-linear systems. Int. J. Robot. Res. 31(7), 901-923 (2012) · doi:10.1177/0278364912444146
[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) · doi:10.1016/j.tej.2017.02.006
[47] Tarjan, R.: Depth-first search and linear graph algorithms. SIAM J. Comput. 1(2), 146-160 (1972) · Zbl 0251.05107 · doi:10.1137/0201010
[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) · Zbl 0997.90060 · doi:10.1080/10556789908805762
[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) · Zbl 1359.68200 · doi:10.1109/TAC.2015.2511722
[50] Yang, I. · Zbl 1400.93336 · doi:10.1016/j.automatica.2018.04.022
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.