{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,1]],"date-time":"2026-06-01T18:27:37Z","timestamp":1780338457872,"version":"3.54.1"},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783662466773","type":"print"},{"value":"9783662466780","type":"electronic"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-662-46678-0_11","type":"book-chapter","created":{"date-parts":[[2015,4,1]],"date-time":"2015-04-01T13:42:21Z","timestamp":1427895741000},"page":"167-182","source":"Crossref","is-referenced-by-count":25,"title":["Unifying Hyper and Epistemic Temporal Logics"],"prefix":"10.1007","author":[{"given":"Laura","family":"Bozzelli","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Bastien","family":"Maubert","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Sophie","family":"Pinchinat","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"11_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"664","DOI":"10.1007\/978-3-540-71209-1_51","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R. Alur","year":"2007","unstructured":"Alur, R., \u010cern\u00fd, P., Chaudhuri, S.: Model checking on trees with path equivalences. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol.\u00a04424, pp. 664\u2013678. Springer, Heidelberg (2007)"},{"key":"11_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/11787006_10","volume-title":"Automata, Languages and Programming","author":"R. Alur","year":"2006","unstructured":"Alur, R., \u010cern\u00fd, P., Zdancewic, S.: Preserving secrecy under refinement. In: Bugliesi, M., Preneel, B., Sassone, V., Wegener, I. (eds.) ICALP 2006. LNCS, vol.\u00a04052, pp. 107\u2013118. Springer, Heidelberg (2006)"},{"key":"11_CR3","doi-asserted-by":"crossref","unstructured":"Balliu, M., Dam, M., Guernic, G.L.: Epistemic temporal logic for information flow security. In: Proc. PLAS, p. 6. ACM (2011)","DOI":"10.1145\/2166956.2166962"},{"key":"11_CR4","unstructured":"Bozzelli, L., Maubert, B., Pinchinat, S.: Unifying hyper and epistemic temporal logic. CoRR, abs\/1409.2711 (2014)"},{"issue":"6","key":"11_CR5","doi-asserted-by":"publisher","first-page":"421","DOI":"10.1007\/s10207-008-0058-x","volume":"7","author":"J. Bryans","year":"2008","unstructured":"Bryans, J., Koutny, M., Mazar\u00e9, L., Ryan, P.Y.A.: Opacity generalised to transition systems. Int. J. Inf. Sec.\u00a07(6), 421\u2013435 (2008)","journal-title":"Int. J. Inf. Sec."},{"key":"11_CR6","doi-asserted-by":"crossref","unstructured":"Clarkson, M.R., Finkbeiner, B., Koleini, M., Micinski, K.K., Rabe, M.N., S\u00e1nchez, C.: Temporal logics for hyperproperties. In: Abadi, M., Kremer, S. (eds.) POST 2014. LNCS, vol.\u00a08414, pp. 265\u2013284. Springer, Heidelberg (2014)","DOI":"10.1007\/978-3-642-54792-8_15"},{"issue":"6","key":"11_CR7","doi-asserted-by":"crossref","first-page":"1157","DOI":"10.3233\/JCS-2009-0393","volume":"18","author":"M. Clarkson","year":"2010","unstructured":"Clarkson, M., Schneider, F.: Hyperproperties. Journal of Computer Security\u00a018(6), 1157\u20131210 (2010)","journal-title":"Journal of Computer Security"},{"key":"11_CR8","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1007\/978-3-642-02734-5_8","volume-title":"Computational Logic in Multi-Agent Systems","author":"C. Dima","year":"2009","unstructured":"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.\u00a05405, pp. 117\u2013131. Springer, Heidelberg (2009)"},{"key":"11_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1007\/978-3-642-27940-9_12","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"R. Dimitrova","year":"2012","unstructured":"Dimitrova, R., Finkbeiner, B., Kov\u00e1cs, M., Rabe, M.N., Seidl, H.: Model checking information flow in reactive systems. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol.\u00a07148, pp. 169\u2013185. Springer, Heidelberg (2012)"},{"issue":"1","key":"11_CR10","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1145\/4904.4999","volume":"33","author":"E. Emerson","year":"1986","unstructured":"Emerson, E., Halpern, J.: \u201cSometimes\u201d and \u201cNot Never\u201d revisited: On branching versus linear time temporal logic. J. ACM\u00a033(1), 151\u2013178 (1986)","journal-title":"J. ACM"},{"key":"11_CR11","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/5803.001.0001","volume-title":"Reasoning about knowledge","author":"R. Fagin","year":"1995","unstructured":"Fagin, R., Halpern, J., Vardi, M.: Reasoning about knowledge, vol.\u00a04. MIT Press, Cambridge (1995)"},{"key":"11_CR12","doi-asserted-by":"crossref","unstructured":"Goguen, J., Meseguer, J.: Security policies and security models. In: IEEE Symposium on Security and Privacy, vol.\u00a012 (1982)","DOI":"10.1109\/SP.1982.10014"},{"key":"11_CR13","doi-asserted-by":"crossref","unstructured":"Halpern, J., O\u2019Neill, K.: Secrecy in multiagent systems. ACM Trans. Inf. Syst. Secur.\u00a012(1) (2008)","DOI":"10.1145\/1410234.1410239"},{"issue":"3","key":"11_CR14","doi-asserted-by":"publisher","first-page":"674","DOI":"10.1137\/S0097539797320906","volume":"33","author":"J. Halpern","year":"2004","unstructured":"Halpern, J., van der Meyden, R., Vardi, M.: Complete Axiomatizations for Reasoning about Knowledge and Time. SIAM J. Comput.\u00a033(3), 674\u2013703 (2004)","journal-title":"SIAM J. Comput."},{"issue":"3","key":"11_CR15","doi-asserted-by":"publisher","first-page":"981","DOI":"10.1016\/j.jcss.2011.08.006","volume":"78","author":"O. Kupferman","year":"2012","unstructured":"Kupferman, O., Pnueli, A., Vardi, M.: Once and for all. J. Comput. Syst. Sci.\u00a078(3), 981\u2013996 (2012)","journal-title":"J. Comput. Syst. Sci."},{"issue":"3","key":"11_CR16","doi-asserted-by":"publisher","first-page":"408","DOI":"10.1145\/377978.377993","volume":"2","author":"O. Kupferman","year":"2001","unstructured":"Kupferman, O., Vardi, M.: Weak alternating automata are not that weak. ACM Transactions on Computational Logic\u00a02(3), 408\u2013429 (2001)","journal-title":"ACM Transactions on Computational Logic"},{"issue":"2","key":"11_CR17","doi-asserted-by":"publisher","first-page":"312","DOI":"10.1145\/333979.333987","volume":"47","author":"O. Kupferman","year":"2000","unstructured":"Kupferman, O., Vardi, M., Wolper, P.: An Automata-Theoretic Approach to Branching-Time Model Checking. J. ACM\u00a047(2), 312\u2013360 (2000)","journal-title":"J. ACM"},{"issue":"1","key":"11_CR18","doi-asserted-by":"crossref","first-page":"37","DOI":"10.3233\/JCS-1992-1103","volume":"1","author":"J. McLean","year":"1992","unstructured":"McLean, J.: Proving noninterference and functional correctness using traces. Journal of Computer Security\u00a01(1), 37\u201358 (1992)","journal-title":"Journal of Computer Security"},{"key":"11_CR19","doi-asserted-by":"crossref","unstructured":"Milushev, D., Clarke, D.: Towards incrementalization of holistic hyperproperties. In: Degano, P., Guttman, J.D. (eds.) POST 2012. LNCS, vol.\u00a07215, pp. 329\u2013348. Springer, Heidelberg (2012)","DOI":"10.1007\/978-3-642-28641-4_18"},{"key":"11_CR20","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1016\/0304-3975(84)90049-5","volume":"32","author":"S. Miyano","year":"1984","unstructured":"Miyano, S., Hayashi, T.: Alternating finite automata on \u03c9-words. Theoretical Computer Science\u00a032, 321\u2013330 (1984)","journal-title":"Theoretical Computer Science"},{"key":"11_CR21","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: Proc. 18th FOCS, pp. 46\u201357. IEEE Computer Society (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"11_CR22","unstructured":"Shilov, N.V., Garanina, N.O.: Model checking knowledge and fixpoints. In: Proc. FICS. BRICS Notes Series, pp. 25\u201339 (2002)"},{"key":"11_CR23","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1016\/0304-3975(87)90008-9","volume":"49","author":"A. Sistla","year":"1987","unstructured":"Sistla, A., Vardi, M., Wolper, P.: The complementation problem for B\u00fcchi automata with appplications to temporal logic. Theoretical Computer Science\u00a049, 217\u2013237 (1987)","journal-title":"Theoretical Computer Science"},{"key":"11_CR24","doi-asserted-by":"crossref","unstructured":"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.\u00a01738, pp. 432\u2013445. Springer, Heidelberg (1999)","DOI":"10.1007\/3-540-46691-6_35"},{"issue":"1-2","key":"11_CR25","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1016\/S0304-3975(98)00009-7","volume":"200","author":"W. Zielonka","year":"1998","unstructured":"Zielonka, W.: Infinite games on finitely coloured graphs with applications to automata on infinite trees. Theoretical Computer Science\u00a0200(1-2), 135\u2013183 (1998)","journal-title":"Theoretical Computer Science"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-46678-0_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,21]],"date-time":"2025-05-21T19:57:38Z","timestamp":1747857458000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-46678-0_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783662466773","9783662466780"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-46678-0_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]}}}