HyperATL\(^*\): A logic for hyperproperties in multi-agent systems. (English) Zbl 07731924
Summary: Hyperproperties are system properties that relate multiple computation paths in a system and are commonly used to, e.g., define information-flow policies. In this paper, we study a novel class of hyperproperties that allow reasoning about strategic abilities in multi-agent systems. We introduce HyperATL\(^*\), an extension of computation tree logic with path variables and strategy quantifiers. Our logic supports quantification over paths in a system – as is possible in hyperlogics such as HyperCTL\(^*\) – but resolves the paths based on the strategic choices of a coalition of agents. This allows us to capture many previously studied (strategic) security notions in a unifying hyperlogic. Moreover, we show that HyperATL\(^*\) is particularly useful for specifying asynchronous hyperproperties, i.e., hyperproperties where the execution speed on the different computation paths depends on the choices of a scheduler. We show that finite-state model checking of HyperATL\(^*\) is decidable and present a model checking algorithm based on alternating automata. We establish that our algorithm is asymptotically optimal by proving matching lower bounds. We have implemented a prototype model checker for a fragment of HyperATL\(^*\) that can check various security properties in small finite-state systems.
Keywords:
hyperproperties; multi-agent systems; alternating-time temporal logic; HyperATL*; information-flow control; asynchronous hyperproperties; model checking; non-interference; HyperLTL; HyperCTL*References:
| [1] | R. Beutner and B. Finkbeiner Vol. 19:2 |
| [2] | Rajeev Alur, Thomas A. Henzinger, and Orna Kupferman. Alternating-time temporal logic. J. ACM, 49(5), 2002. doi:10.1145/585265.585270. · Zbl 1326.68181 · doi:10.1145/585265.585270 |
| [3] | + 98] Rajeev Alur, Thomas A. Henzinger, Freddy Y. C. Mang, Shaz Qadeer, Sriram K. Rajamani, and Serdar Tasiran. MOCHA: modularity in model checking. In International Conference on Computer Aided Verification, CAV 1998, volume 1427 of Lecture Notes in Computer Science. Springer, 1998. doi:10.1007/BFb0028774. · doi:10.1007/BFb0028774 |
| [4] | + 21] Jan Baumeister, Norine Coenen, Borzoo Bonakdarpour, Bernd Finkbeiner, and César Sánchez. A temporal logic for asynchronous hyperproperties. In International Conference on Computer Aided Verification, CAV 2021, volume 12759 of Lecture Notes in Computer Science. Springer, 2021. doi:10.1007/978-3-030-81685-8_33. · Zbl 1493.68205 · doi:10.1007/978-3-030-81685-8_33 |
| [5] | As alternating-time logics are evaluated over game structures, the satisfiability problem can either be stated as the search for a set of agents (containing the agents refereed to in the formula) and game structure over those agents or the search for a game structure given a fixed set of agents (as part of the input). See [WLWW06] for details in the context of ATL. We assume that the set of agents is provided with the input. 13:40 R. Beutner and B. Finkbeiner Vol. 19:2 |
| [6] | Raven Beutner, David Carral, Bernd Finkbeiner, Jana Hofmann, and Markus Krötzsch. Deciding hyperproperties combined with functional specifications. In Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2022. ACM, 2022. doi:10.1145/3531130.3533369. · doi:10.1145/3531130.3533369 |
| [7] | Gilles Barthe, Pedro R. D’Argenio, and Tamara Rezk. Secure information flow by self-composition. Math. Struct. Comput. Sci., 21(6), 2011. doi:10.1017/S0960129511000193. · Zbl 1252.68072 · doi:10.1017/S0960129511000193 |
| [8] | Raven Beutner and Bernd Finkbeiner. A temporal logic for strategic hyperproperties. In International Conference on Concurrency Theory, CONCUR 2021, volume 203 of LIPIcs. Schloss Dagstuhl, 2021. doi:10.4230/LIPIcs.CONCUR.2021.24. · Zbl 07730626 · doi:10.4230/LIPIcs.CONCUR.2021.24 |
| [9] | Raven Beutner and Bernd Finkbeiner. Prophecy variables for hyperproperty verification. In IEEE Computer Security Foundations Symposium, CSF 2022. IEEE, 2022. doi:10.1109/CSF54842. 2022.9919658. · Zbl 1514.68122 · doi:10.1109/CSF54842.2022.9919658 |
| [10] | Raven Beutner and Bernd Finkbeiner. Software verification of hyperproperties beyond k-safety. In International Conference on Computer Aided Verification, CAV 2022, volume 13371 of Lecture Notes in Computer Science. Springer, 2022. doi:10.1007/978-3-031-13185-1_17. · Zbl 1514.68122 · doi:10.1007/978-3-031-13185-1_17 |
| [11] | Raven Beutner and Bernd Finkbeiner. AutoHyper: Explicit-state model checking for HyperLTL. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2023, volume 13993 of Lecture Notes in Computer Science. Springer, 2023. doi:10.1007/978-3-031-30823-9_8. · Zbl 07777303 · doi:10.1007/978-3-031-30823-9_8 |
| [12] | Raven Beutner and Bernd Finkbeiner. Model checking omega-regular hyperproperties with AutoHyperQ. In International Conference on Logic for Programming, Artificial Intelligence and Reasoning, LPAR 2023, EPiC Series in Computing. EasyChair, 2023. · Zbl 07730626 |
| [13] | Raven Beutner, Bernd Finkbeiner, Hadar Frenkel, and Niklas Metzger. Second-order hyperprop-erties. In International Conference on Computer Aided Verification, CAV 2023, Lecture Notes in Computer Science. Springer, 2023. · Zbl 07787559 |
| [14] | Nils Bulling, Valentin Goranko, and Wojciech Jamroga. Logics for reasoning about strate-gic abilities in multi-player games. In Models of Strategic Reasoning -Logics, Games, and Communities, volume 8972 of Lecture Notes in Computer Science. Springer, 2015. doi: 10.1007/978-3-662-48540-8_4. · Zbl 1422.91116 · doi:10.1007/978-3-662-48540-8_4 |
| [15] | Udi Boker, Orna Kupferman, and Adin Rosenberg. Alternation removal in büchi automata. In International Colloquium on Automata, Languages and Programming, ICALP 2010, volume 6199 of Lecture Notes in Computer Science. Springer, 2010. doi:10.1007/978-3-642-14162-1_7. · Zbl 1288.68148 · doi:10.1007/978-3-642-14162-1_7 |
| [16] | Raphaël Berthon, Bastien Maubert, and Aniello Murano. Decidability results for ATL* with imperfect information and perfect recall. In Conference on Autonomous Agents and MultiAgent Systems, AAMAS 2017. ACM, 2017. · Zbl 1458.68113 |
| [17] | Laura Bozzelli, Bastien Maubert, and Sophie Pinchinat. Unifying hyper and epistemic temporal logics. In International Conference on Foundations of Software Science and Computation Structures, FoSSaCS 2015, volume 9034 of Lecture Notes in Computer Science. Springer, 2015. doi:10.1007/978-3-662-46678-0_11. · Zbl 1459.03019 · doi:10.1007/978-3-662-46678-0_11 |
| [18] | Laura Bozzelli, Adriano Peron, and César Sánchez. Asynchronous extensions of HyperLTL. In Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021. IEEE, 2021. doi:10.1109/LICS52264.2021.9470583. · doi:10.1109/LICS52264.2021.9470583 |
| [19] | Norine Coenen, Bernd Finkbeiner, Christopher Hahn, and Jana Hofmann. The hierarchy of hyperlogics. In Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019. IEEE, 2019. doi:10.1109/LICS.2019.8785713. · Zbl 1497.68291 · doi:10.1109/LICS.2019.8785713 |
| [20] | + 14] Michael R. Clarkson, Bernd Finkbeiner, Masoud Koleini, Kristopher K. Micinski, Markus N. Rabe, and César Sánchez. Temporal logics for hyperproperties. In International Conference on Principles of Security and Trust, POST 2014, volume 8414 of Lecture Notes in Computer Science. Springer, 2014. doi:10.1007/978-3-642-54792-8_15. · doi:10.1007/978-3-642-54792-8_15 |
| [21] | Norine Coenen, Bernd Finkbeiner, César Sánchez, and Leander Tentrup. Verifying hyperliveness. In International Conference on Computer Aided Verification, CAV 2019, volume 11561 of Lecture Notes in Computer Science. Springer, 2019. doi:10.1007/978-3-030-25540-4_7. · Zbl 1533.68147 · doi:10.1007/978-3-030-25540-4_7 |
| [22] | Krishnendu Chatterjee, Thomas A. Henzinger, and Nir Piterman. Strategy logic. Inf. Comput., 208(6), 2010. doi:10.1016/j.ic.2009.07.004. · Zbl 1151.03327 · doi:10.1016/j.ic.2009.07.004 |
| [23] | Michael R. Clarkson and Fred B. Schneider. Hyperproperties. J. Comput. Secur., 18(6), 2010. doi:10.3233/JCS-2009-0393. 13:41 · doi:10.3233/JCS-2009-0393 |
| [24] | Doron Drusinsky and David Harel. On the power of bounded concurrency I: finite automata. J. ACM, 41(3), 1994. doi:10.1145/176584.176587. · Zbl 0813.68138 · doi:10.1145/176584.176587 |
| [25] | Catalin Dima and Ferucio Laurentiu Tiplea. Model-checking ATL under imperfect information and perfect recall semantics is undecidable. CoRR, abs/1102.4225, 2011. arXiv:1102.4225. |
| [26] | E. Allen Emerson and Joseph Y. Halpern. “sometimes” and “not never” revisited: on branching versus linear time temporal logic. J. ACM, 33(1), 1986. doi:10.1145/4904.4999. · Zbl 0629.68020 · doi:10.1145/4904.4999 |
| [27] | Bernd Finkbeiner and Christopher Hahn. Deciding hyperproperties. In International Conference on Concurrency Theory, CONCUR 2016, volume 59 of LIPIcs. Schloss Dagstuhl, 2016. doi: 10.4230/LIPIcs.CONCUR.2016.13. [FHL + 18] Bernd Finkbeiner, Christopher Hahn, Philip Lukert, Marvin Stenger, and Leander Tentrup. Synthesizing reactive systems from hyperproperties. In International Conference on Computer Aided Verification, CAV 2018, volume 10981 of Lecture Notes in Computer Science. Springer, 2018. doi:10.1007/978-3-319-96145-3_16. · Zbl 1511.68153 · doi:10.1007/978-3-319-96145-3_16 |
| [28] | Ronald Fagin, Joseph Y. Halpern, Yoram Moses, and Moshe Y. Vardi. Reasoning About Knowledge. MIT Press, 1995. doi:10.7551/mitpress/5803.001.0001. · Zbl 0839.68095 · doi:10.7551/mitpress/5803.001.0001 |
| [29] | Marie Fortin, Louwe B. Kuijer, Patrick Totzke, and Martin Zimmermann. HyperLTL satisfiabil-ity is Σ 1 1 -complete, HyperCTL* satisfiability is Σ 2 1 -complete. In International Symposium on Mathematical Foundations of Computer Science, MFCS 2021, volume 202 of LIPIcs. Schloss Dagstuhl, 2021. doi:10.4230/LIPIcs.MFCS.2021.47. · Zbl 07724220 · doi:10.4230/LIPIcs.MFCS.2021.47 |
| [30] | Oliver Friedmann and Martin Lange. Solving parity games in practice. In International Sym-posium on Automated Technology for Verification and Analysis, ATVA 2009, volume 5799 of Lecture Notes in Computer Science. Springer, 2009. doi:10.1007/978-3-642-04761-9_15. · Zbl 1258.68077 · doi:10.1007/978-3-642-04761-9_15 |
| [31] | Bernd Finkbeiner, Christian Müller, Helmut Seidl, and Eugen Zalinescu. Verifying security poli-cies in multi-agent workflows with loops. In ACM Conference on Computer and Communications Security, CCS 2017. ACM, 2017. doi:10.1145/3133956.3134080. · doi:10.1145/3133956.3134080 |
| [32] | Bernd Finkbeiner, Markus N. Rabe, and César Sánchez. Algorithms for model checking HyperLTL and HyperCTL * . In International Conference on Computer Aided Verification, CAV 2015, volume 9206 of Lecture Notes in Computer Science. Springer, 2015. doi:10.1007/978-3-319-21690-4_3. · Zbl 1381.68161 · doi:10.1007/978-3-319-21690-4_3 |
| [33] | Bernd Finkbeiner and Martin Zimmermann. The first-order logic of hyperproperties. In Sympo-sium on Theoretical Aspects of Computer Science, STACS 2017, volume 66 of LIPIcs. Schloss Dagstuhl, 2017. doi:10.4230/LIPIcs.STACS.2017.30. · Zbl 1402.03036 · doi:10.4230/LIPIcs.STACS.2017.30 |
| [34] | Joseph A. Goguen and José Meseguer. Security policies and security models. In IEEE Symposium on Security and Privacy, SP 1982. IEEE, 1982. doi:10.1109/SP.1982.10014. · doi:10.1109/SP.1982.10014 |
| [35] | Jens Oliver Gutsfeld, Markus Müller-Olm, and Christoph Ohrem. Automata and fixpoints for asynchronous hyperproperties. Proc. ACM Program. Lang., 5(POPL), 2021. doi:10.1145/ 3434319. · Zbl 07559506 · doi:10.1145/3434319 |
| [36] | Christopher Hahn. Logical and deep learning methods for temporal reasoning. PhD thesis, Saarland University, 2021. doi:10.22028/D291-35192. · doi:10.22028/D291-35192 |
| [37] | Joseph Y. Halpern and Yoram Moses. Knowledge and common knowledge in a distributed environment. J. ACM, 37(3), 1990. doi:10.1145/79147.79161. · Zbl 0699.68115 · doi:10.1145/79147.79161 |
| [38] | Marieke Huisman, Pratik Worah, and Kim Sunesen. A temporal logic characterisation of observational determinism. In IEEE Computer Security Foundations Workshop, CSFW 2006. IEEE, 2006. doi:10.1109/CSFW.2006.6. · doi:10.1109/CSFW.2006.6 |
| [39] | Wojciech Jamroga and ThomasÅgotnes. What agents can achieve under incomplete information. In International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS 2006). ACM, 2006. doi:10.1145/1160633.1160672. · doi:10.1145/1160633.1160672 |
| [40] | Jan Kretínský, Tobias Meggendorfer, Salomon Sickert, and Christopher Ziegler. Rabinizer 4: From LTL to your favourite deterministic automaton. In International Conference on Computer Aided Verification, CAV 2018, volume 10981 of Lecture Notes in Computer Science. Springer, 2018. doi:10.1007/978-3-319-96145-3_30. · doi:10.1007/978-3-319-96145-3_30 |
| [41] | Daryl McCullough. Noninterference and the composability of security properties. In IEEE Symposium on Security and Privacy, SP 1988. IEEE, 1988. doi:10.1109/SECPRI.1988.8110. · doi:10.1109/SECPRI.1988.8110 |
| [42] | Satoru Miyano and Takeshi Hayashi. Alternating finite automata on omega-words. Theor. Comput. Sci., 32, 1984. doi:10.1016/0304-3975(84)90049-5. 13:42 R. Beutner and B. Finkbeiner Vol. 19:2 · Zbl 0544.68041 · doi:10.1016/0304-3975(84)90049-5 |
| [43] | Robin Milner. A Calculus of Communicating Systems, volume 92 of Lecture Notes in Computer Science. Springer, 1980. doi:10.1007/3-540-10235-3. · Zbl 0452.68027 · doi:10.1007/3-540-10235-3 |
| [44] | Fabio Mogavero, Aniello Murano, Giuseppe Perelli, and Moshe Y. Vardi. Reasoning about strategies: On the model-checking problem. ACM Trans. Comput. Log., 15(4), 2014. doi: 10.1145/2631917. · Zbl 1354.68178 · doi:10.1145/2631917 |
| [45] | Heiko Mantel and Henning Sudbrock. Flexible scheduler-independent security. In European Symposium on Research in Computer Security, ESORICS 2010, volume 6345 of Lecture Notes in Computer Science. Springer, 2010. doi:10.1007/978-3-642-15497-3_8. · doi:10.1007/978-3-642-15497-3_8 |
| [46] | David E. Muller, Ahmed Saoudi, and Paul E. Schupp. Weak alternating automata give a simple explanation of why most temporal and dynamic logics are decidable in exponential time. In Annual Symposium on Logic in Computer Science, LICS 1988. IEEE, 1988. doi: 10.1109/LICS.1988.5139. · doi:10.1109/LICS.1988.5139 |
| [47] | Christian Müller, Helmut Seidl, and Eugen Zalinescu. Inductive invariants for noninterference in multi-agent workflows. In IEEE Computer Security Foundations Symposium, CSF 2018. IEEE Computer Society, 2018. doi:10.1109/CSF.2018.00025. · doi:10.1109/CSF.2018.00025 |
| [48] | Amir Pnueli and Roni Rosner. On the synthesis of a reactive module. In Annual ACM Symposium on Principles of Programming Languages, POPL 1989. ACM Press, 1989. doi:10.1145/75277. 75293. · doi:10.1145/75277.75293 |
| [49] | Markus N. Rabe. A temporal logic approach to information-flow control. PhD thesis, Saarland University, 2016. |
| [50] | Andrei Sabelfeld. Confidentiality for multithreaded programs via bisimulation. In International Andrei Ershov Memorial Conference, PSI 2003, volume 2890 of Lecture Notes in Computer Science. Springer, 2003. doi:10.1007/978-3-540-39866-0_27. · doi:10.1007/978-3-540-39866-0_27 |
| [51] | Walter J. Savitch. Relationships between nondeterministic and deterministic tape complexities. J. Comput. Syst. Sci., 4(2), 1970. doi:10.1016/S0022-0000(70)80006-X. · Zbl 0188.33502 · doi:10.1016/S0022-0000(70)80006-X |
| [52] | Pierre-Yves Schobbens. Alternating-time logic with imperfect recall. Electron. Notes Theor. Comput. Sci., 85(2), 2004. doi:10.1016/S1571-0661(05)82604-0. · Zbl 1270.68287 · doi:10.1016/S1571-0661(05)82604-0 |
| [53] | Sven Schewe. ATL * satisfiability is 2EXPTIME-complete. In International Colloquium on Automata, Languages and Programming, ICALP 2008, volume 5126 of Lecture Notes in Computer Science. Springer, 2008. doi:10.1007/978-3-540-70583-3_31. · Zbl 1155.68447 · doi:10.1007/978-3-540-70583-3_31 |
| [54] | Andrei Sabelfeld and David Sands. Probabilistic noninterference for multi-threaded programs. In IEEE Computer Security Foundations Workshop, CSFW 2000. IEEE, 2000. doi:10.1109/ CSFW.2000.856937. · doi:10.1109/CSFW.2000.856937 |
| [55] | Colin Stirling. Modal and temporal logics for processes. In Banff Higher Order Workshop on Logics for Concurrency -Structure versus Automata, volume 1043 of Lecture Notes in Computer Science. Springer, 1995. doi:10.1007/3-540-60915-6_5. · Zbl 07869807 · doi:10.1007/3-540-60915-6_5 |
| [56] | Larry Joseph Stockmeyer. The complexity of decision problems in automata theory and logic. PhD thesis, Massachusetts Institute of Technology, 1974. |
| [57] | Wiebe van der Hoek and Michael J. Wooldridge. Cooperation, knowledge, and time: Alternating-time temporal epistemic logic and its applications. Stud Logica, 75(1), 2003. doi:10.1023/A: 1026185103185. · Zbl 1034.03013 · doi:10.1023/A:1026185103185 |
| [58] | Moshe Y. Vardi and Pierre Wolper. Reasoning about infinite computations. Inf. Comput., 115(1), 1994. doi:10.1006/inco.1994.1092. · Zbl 0827.03009 · doi:10.1006/inco.1994.1092 |
| [59] | J. Todd Wittbold and Dale M. Johnson. Information flow in nondeterministic systems. In IEEE Symposium on Security and Privacy, SP 1990. IEEE, 1990. doi:10.1109/RISP.1990.63846. · doi:10.1109/RISP.1990.63846 |
| [60] | Dirk Walther, Carsten Lutz, Frank Wolter, and Michael J. Wooldridge. ATL satisfiability is indeed EXPTIME-complete. J. Log. Comput., 16(6), 2006. doi:10.1093/logcom/exl009. · Zbl 1118.03010 · doi:10.1093/logcom/exl009 |
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.
