Abstract
In the literature, two powerful temporal logic formalisms have been proposed for expressing information-flow security requirements, that in general, go beyond regular properties. One is classic, based on the knowledge modalities of epistemic logic. The other one, the so-called hyper logic, is more recent and subsumes many proposals from the literature. In an attempt to better understand how these logics compare with each other, we consider the logic \(\text{\sffamily KCTL$^{*}$}\) (the extension of \(\text{\sffamily CTL$^{*}$}\) with knowledge modalities and synchronous perfect recall semantics) and \(\text{\sffamily HyperCTL$^{*}$}\). We first establish that \(\text{\sffamily KCTL$^{*}$}\) and \(\text{\sffamily HyperCTL$^{*}$}\) are expressively incomparable. Then, we introduce a natural linear past extension of \(\text{\sffamily HyperCTL$^{*}$}\), called \(\text{\sffamily HyperCTL$^{*}_{lp}$}\), that unifies \(\text{\sffamily KCTL$^{*}$}\) and \(\text{\sffamily HyperCTL$^{*}$}\). We show that the model-checking problem for \(\text{\sffamily HyperCTL$^{*}_{lp}$}\) is decidable, and we provide its exact computational complexity in terms of a new measure of path quantifiers’ alternation. For this, we settle open complexity issues for unrestricted quantified propositional temporal logic.
We acknowledge financial suppport from ERC project EPS 313360.
Chapter PDF
Similar content being viewed by others
References
Alur, R., Černý, P., Chaudhuri, S.: Model checking on trees with path equivalences. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 664–678. Springer, Heidelberg (2007)
Alur, R., Černý, P., Zdancewic, S.: Preserving secrecy under refinement. In: Bugliesi, M., Preneel, B., Sassone, V., Wegener, I. (eds.) ICALP 2006. LNCS, vol. 4052, pp. 107–118. Springer, Heidelberg (2006)
Balliu, M., Dam, M., Guernic, G.L.: Epistemic temporal logic for information flow security. In: Proc. PLAS, p. 6. ACM (2011)
Bozzelli, L., Maubert, B., Pinchinat, S.: Unifying hyper and epistemic temporal logic. CoRR, abs/1409.2711 (2014)
Bryans, J., Koutny, M., Mazaré, L., Ryan, P.Y.A.: Opacity generalised to transition systems. Int. J. Inf. Sec. 7(6), 421–435 (2008)
Clarkson, M.R., Finkbeiner, B., Koleini, M., Micinski, K.K., Rabe, M.N., Sánchez, C.: Temporal logics for hyperproperties. In: Abadi, M., Kremer, S. (eds.) POST 2014. LNCS, vol. 8414, pp. 265–284. Springer, Heidelberg (2014)
Clarkson, M., Schneider, F.: Hyperproperties. Journal of Computer Security 18(6), 1157–1210 (2010)
Dima, C.: Revisiting satisfiability and model-checking for CTLK with synchrony and perfect recall. In: Fisher, M., Sadri, F., Thielscher, M. (eds.) CLIMA IX. LNCS (LNAI), vol. 5405, pp. 117–131. Springer, Heidelberg (2009)
Dimitrova, R., Finkbeiner, B., Kovács, M., Rabe, M.N., Seidl, H.: Model checking information flow in reactive systems. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol. 7148, pp. 169–185. Springer, Heidelberg (2012)
Emerson, E., Halpern, J.: “Sometimes” and “Not Never” revisited: On branching versus linear time temporal logic. J. ACM 33(1), 151–178 (1986)
Fagin, R., Halpern, J., Vardi, M.: Reasoning about knowledge, vol. 4. MIT Press, Cambridge (1995)
Goguen, J., Meseguer, J.: Security policies and security models. In: IEEE Symposium on Security and Privacy, vol. 12 (1982)
Halpern, J., O’Neill, K.: Secrecy in multiagent systems. ACM Trans. Inf. Syst. Secur. 12(1) (2008)
Halpern, J., van der Meyden, R., Vardi, M.: Complete Axiomatizations for Reasoning about Knowledge and Time. SIAM J. Comput. 33(3), 674–703 (2004)
Kupferman, O., Pnueli, A., Vardi, M.: Once and for all. J. Comput. Syst. Sci. 78(3), 981–996 (2012)
Kupferman, O., Vardi, M.: Weak alternating automata are not that weak. ACM Transactions on Computational Logic 2(3), 408–429 (2001)
Kupferman, O., Vardi, M., Wolper, P.: An Automata-Theoretic Approach to Branching-Time Model Checking. J. ACM 47(2), 312–360 (2000)
McLean, J.: Proving noninterference and functional correctness using traces. Journal of Computer Security 1(1), 37–58 (1992)
Milushev, D., Clarke, D.: Towards incrementalization of holistic hyperproperties. In: Degano, P., Guttman, J.D. (eds.) POST 2012. LNCS, vol. 7215, pp. 329–348. Springer, Heidelberg (2012)
Miyano, S., Hayashi, T.: Alternating finite automata on ω-words. Theoretical Computer Science 32, 321–330 (1984)
Pnueli, A.: The temporal logic of programs. In: Proc. 18th FOCS, pp. 46–57. IEEE Computer Society (1977)
Shilov, N.V., Garanina, N.O.: Model checking knowledge and fixpoints. In: Proc. FICS. BRICS Notes Series, pp. 25–39 (2002)
Sistla, A., Vardi, M., Wolper, P.: The complementation problem for Büchi automata with appplications to temporal logic. Theoretical Computer Science 49, 217–237 (1987)
van der Meyden, R., Shilov, N.V.: Model checking knowledge and time in systems with perfect recall (extended abstract). In: Pandu Rangan, C., Raman, V., Sarukkai, S. (eds.) FSTTCS 1999. LNCS, vol. 1738, pp. 432–445. Springer, Heidelberg (1999)
Zielonka, W.: Infinite games on finitely coloured graphs with applications to automata on infinite trees. Theoretical Computer Science 200(1-2), 135–183 (1998)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bozzelli, L., Maubert, B., Pinchinat, S. (2015). Unifying Hyper and Epistemic Temporal Logics. In: Pitts, A. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 2015. Lecture Notes in Computer Science(), vol 9034. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-46678-0_11
Download citation
DOI: https://doi.org/10.1007/978-3-662-46678-0_11
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-46677-3
Online ISBN: 978-3-662-46678-0
eBook Packages: Computer ScienceComputer Science (R0)