{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T05:22:08Z","timestamp":1776316928553,"version":"3.50.1"},"publisher-location":"Cham","reference-count":47,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319216898","type":"print"},{"value":"9783319216904","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":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-21690-4_3","type":"book-chapter","created":{"date-parts":[[2015,7,15]],"date-time":"2015-07-15T06:08:27Z","timestamp":1436940507000},"page":"30-48","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":116,"title":["Algorithms for Model Checking HyperLTL and HyperCTL $$^*$$"],"prefix":"10.1007","author":[{"given":"Bernd","family":"Finkbeiner","sequence":"first","affiliation":[]},{"given":"Markus N.","family":"Rabe","sequence":"additional","affiliation":[]},{"given":"C\u00e9sar","family":"S\u00e1nchez","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,7,16]]},"reference":[{"key":"3_CR1","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. 4052, pp. 107\u2013118. Springer, Heidelberg (2006)"},{"key":"3_CR2","unstructured":"Andersen, H.R.: A polyadic modal $$\\mu $$ -calculus. Technical report (1994)"},{"key":"3_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1007\/978-3-642-11957-6_5","volume-title":"Programming Languages and Systems","author":"A Askarov","year":"2010","unstructured":"Askarov, A., Myers, A.: A semantic framework for declassification and endorsement. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol. 6012, pp. 64\u201384. Springer, Heidelberg (2010)"},{"key":"3_CR4","doi-asserted-by":"crossref","unstructured":"Balliu, M., Dam, M., Le Guernic, G.: Epistemic temporal logic for information flow security. In: Proceedings of PLAS, ACM (2011)","DOI":"10.1145\/2166956.2166962"},{"key":"3_CR5","doi-asserted-by":"crossref","unstructured":"Banerjee, A., Naumann, D.A., Rosenberg, S.: Expressive declassification policies and modular static enforcement. In: Proceedings of S\u00a0&\u00a0P, pp. 339\u2013353, IEEE CS Press (2008)","DOI":"10.1109\/SP.2008.20"},{"key":"3_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1007\/978-3-642-35722-0_3","volume-title":"Logical Foundations of Computer Science","author":"G Barthe","year":"2013","unstructured":"Barthe, G., Crespo, J.M., Kunz, C.: Beyond 2-safety: asymmetric product programs for relational program verification. In: Artemov, S., Nerode, A. (eds.) LFCS 2013. LNCS, vol. 7734, pp. 29\u201343. Springer, Heidelberg (2013)"},{"key":"3_CR7","doi-asserted-by":"crossref","unstructured":"Barthe, G., D\u2019Argenio, P.R., Rezk, T.: Secure information flow by self-composition. In: Proceedings CSFW, pp. 100\u2013114, June 2004","DOI":"10.1109\/CSFW.2004.1310735"},{"key":"3_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1007\/3-540-48683-6_8","volume-title":"Computer Aided Verification","author":"A Biere","year":"1999","unstructured":"Biere, A., Clarke, E., Raimi, R., Zhu, Y.: Verifying safety properties of a PowerPC $$^{\\rm TM}$$ microprocessor using symbolic model checking without BDDs. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 60\u201371. Springer, Heidelberg (1999)"},{"key":"3_CR9","unstructured":"Biere, A., Heljanko, K., Wieringa, S.: AIGER 1.9 and beyond. http:\/\/fmv.jku.at\/hwmcc11\/beyond1.pdf (2011). Accessed Feb 6 2015. Via website: http:\/\/fmv.jku.at\/aiger\/"},{"key":"3_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1007\/978-3-642-18275-4_7","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"AR Bradley","year":"2011","unstructured":"Bradley, A.R.: SAT-based model checking without unrolling. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 70\u201387. Springer, Heidelberg (2011)"},{"key":"3_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/978-3-642-14295-6_5","volume-title":"Computer Aided Verification","author":"R Brayton","year":"2010","unstructured":"Brayton, R., Mishchenko, A.: ABC: an academic industrial-strength verification tool. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 24\u201340. Springer, Heidelberg (2010)"},{"key":"3_CR12","doi-asserted-by":"crossref","unstructured":"Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L.: Sequential circuit verification using symbolic model checking. In: Proceedings of DAC 1990, pp. 46\u201351, IEEE CS Press (1990)","DOI":"10.1145\/123186.123223"},{"key":"3_CR13","doi-asserted-by":"crossref","unstructured":"Claessen, K., E\u00e9n, N., Sterin, B.: A circuit approach to LTL model checking. In: Proceedings of FMCAD, pp. 53\u201360 (2013)","DOI":"10.1109\/FMCAD.2013.6679391"},{"key":"3_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/978-3-642-54792-8_15","volume-title":"Principles of Security and Trust","author":"MR Clarkson","year":"2014","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 (ETAPS 2014). LNCS, vol. 8414, pp. 265\u2013284. Springer, Heidelberg (2014)"},{"key":"3_CR15","doi-asserted-by":"crossref","unstructured":"Clarkson, M.R., Schneider, F.B.: Hyperproperties.In: Proceedings IEEE Symposium on Computer Security Foundations, pp. 51\u201365, June 2008","DOI":"10.1109\/CSF.2008.7"},{"key":"3_CR16","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. 7148, pp. 169\u2013185. Springer, Heidelberg (2012)"},{"issue":"1","key":"3_CR17","doi-asserted-by":"crossref","first-page":"101","DOI":"10.3233\/JCS-2010-0400","volume":"19","author":"D D\u2019Souza","year":"2011","unstructured":"D\u2019Souza, D., Holla, R., Raghavendra, K.R., Sprick, B.: Model-checking trace-based information flow properties. J. Comput. Secur. 19(1), 101\u2013138 (2011)","journal-title":"J. Comput. Secur."},{"key":"3_CR18","unstructured":"E\u00e9n, N., Mishchenko, A., Brayton, R.K.: Efficient implementation of property directed reachability. In: Proceedings of FMCAD, pp. 125\u2013134 (2011)"},{"key":"3_CR19","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.Y., Moses, Y., Vardi, M.Y.: Reasoning About Knowledge. MIT Press, Cambridge (1995)"},{"key":"3_CR20","first-page":"273","volume":"56","author":"B Finkbeiner","year":"2014","unstructured":"Finkbeiner, B., Rabe, M.N.: The linear-hyper-branching spectrum of temporal logics. IT Inf. Technol. 56, 273\u2013279 (2014)","journal-title":"IT Inf. Technol."},{"key":"3_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"479","DOI":"10.1007\/978-3-540-27813-9_41","volume-title":"Computer Aided Verification","author":"P Gammie","year":"2004","unstructured":"Gammie, P., van der Meyden, R.: MCK: model checking the logic of knowledge. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 479\u2013483. Springer, Heidelberg (2004)"},{"key":"3_CR22","doi-asserted-by":"crossref","unstructured":"Goguen, J.A., Meseguer, J.: Security policies and security models. In: Proceedings IEEE Symposium on Security and Privacy, pp. 11\u201320, IEEE CS Press (1982)","DOI":"10.1109\/SP.1982.10014"},{"key":"3_CR23","unstructured":"Huisman, M., Worah, P., Sunesen, K.: A temporal logic characterisation of observational determinism. In: Proceedings of CSFW, IEEE CS Press (2006)"},{"key":"3_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BFb0055036","volume-title":"Automata, Languages and Programming","author":"Y Kesten","year":"1998","unstructured":"Kesten, Y., Pnueli, A., Raviv, L.: Algorithmic verification of linear temporal logic specifications. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, pp. 1\u201316. Springer, Heidelberg (1998)"},{"issue":"3","key":"3_CR25","doi-asserted-by":"publisher","first-page":"408","DOI":"10.1145\/377978.377993","volume":"2","author":"O Kupferman","year":"2001","unstructured":"Kupferman, O., Vardi, M.Y.: Weak alternating automata are not that weak. ACM TOCL 2(3), 408\u2013429 (2001)","journal-title":"ACM TOCL"},{"issue":"8","key":"3_CR26","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1145\/361082.361093","volume":"17","author":"L Lamport","year":"1974","unstructured":"Lamport, L.: A new solution of Dijkstra\u2019s concurrent programming problem. Commun. ACM 17(8), 453\u2013455 (1974)","journal-title":"Commun. ACM"},{"key":"3_CR27","doi-asserted-by":"crossref","unstructured":"Lange, M., Lozes, \u00c9.: Model-checking the higher-dimensional modal mu-calculus. In: Proceedings of FICS, EPTCS, vol. 77, pp. 39\u201346 (2012)","DOI":"10.4204\/EPTCS.77.6"},{"key":"3_CR28","unstructured":"Lomuscio, A., Pecheur, C., Raimondi, F.: Automatic verification of knowledge and time with NuSMV. In: Proceedings of IJCAI, pp. 1384\u20131389 (2007)"},{"key":"3_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"682","DOI":"10.1007\/978-3-642-02658-4_55","volume-title":"Computer Aided Verification","author":"A Lomuscio","year":"2009","unstructured":"Lomuscio, A., Qu, H., Raimondi, F.: MCMAS: a model checker for the verification of multi-agent systems. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 682\u2013688. Springer, Heidelberg (2009)"},{"key":"3_CR30","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0931-7","volume-title":"The Temporal Logic of Reactive and Concurrent Systems","author":"Z Manna","year":"1992","unstructured":"Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems. Springer, New York (1992)"},{"key":"3_CR31","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-4222-2","volume-title":"Temporal Verification of Reactive Systems: Safety","author":"Z Manna","year":"1995","unstructured":"Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems: Safety. Springer, New York (1995)"},{"key":"3_CR32","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"336","DOI":"10.1007\/3-540-44898-5_18","volume-title":"Static Analysis","author":"KL McMillan","year":"2003","unstructured":"McMillan, K.L.: Craig interpolation and reachability analysis. In: Cousot, R. (ed.) SAS 2003. LNCS, vol. 2694, p. 336. Springer, Heidelberg (2003)"},{"key":"3_CR33","unstructured":"Meski, A., Penczek, W., Szreter, M., Wozna-Szczesniak, B., Zbrzezny, A.: Bounded model checking for knowledge and linear time. In: Proceedings of AAMAS, pp. 1447\u20131448, IFAAMAS (2012)"},{"key":"3_CR34","unstructured":"Milushev, D.: Reasoning about hyperproperties. Ph.D thesis, Faculty of Engineering, Katholieke Universiteit Leuven, Celestijnenlaan 200A, box 2402, B3001 Heverlee, Belgium, 6 (2013)"},{"key":"3_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"329","DOI":"10.1007\/978-3-642-28641-4_18","volume-title":"Principles of Security and Trust","author":"D Milushev","year":"2012","unstructured":"Milushev, D., Clarke, D.: Towards incrementalization of holistic hyperproperties. In: Degano, P., Guttman, J.D. (eds.) Principles of Security and Trust. LNCS, vol. 7215, pp. 329\u2013348. Springer, Heidelberg (2012)"},{"key":"3_CR36","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 omega-words. Theor. Comput. Sci. 32, 321\u2013330 (1984)","journal-title":"Theor. Comput. Sci."},{"key":"3_CR37","doi-asserted-by":"crossref","unstructured":"Muller, D.E., Saoudi, A., Schupp, P.E.: Weak alternating automata give a simple explanation of why most temporal and dynamic logics are decidable in exponential time. In: Proceedings of LICS, pp. 422\u2013427, IEEE CS Press (1988)","DOI":"10.1109\/LICS.1988.5139"},{"key":"3_CR38","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1016\/S0304-3975(98)00314-4","volume":"224","author":"M Otto","year":"1998","unstructured":"Otto, M.: Bisimulation-invariant PTIME and higher-dimensional $$\\mu $$ -calculus. Theor. Comput. Sci. 224, 237\u2013265 (1998)","journal-title":"Theor. Comput. Sci."},{"key":"3_CR39","doi-asserted-by":"crossref","unstructured":"Pencze, W., Lomuscio, A.: Verifying epistemic properties of multi-agent systems via bounded model checking. In: Proceedings of AAMAS, pp. 209\u2013216, IFAAMAS (2003)","DOI":"10.1145\/860575.860609"},{"key":"3_CR40","unstructured":"Rabe, M.N.: MCHyper: a model checker for hyperproperties. http:\/\/www.react.uni-saarland.de\/tools\/mchyper\/ (2015). Accessed Feb 6 2015"},{"key":"3_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/978-3-540-37621-7_9","volume-title":"Software Security - Theories and Systems","author":"A Sabelfeld","year":"2004","unstructured":"Sabelfeld, A., Myers, A.C.: A model for delimited information release. In: Futatsugi, K., Mizoguchi, F., Yonezaki, N. (eds.) ISSS 2003. LNCS, vol. 3233, pp. 174\u2013191. Springer, Heidelberg (2004)"},{"issue":"3","key":"3_CR42","doi-asserted-by":"publisher","first-page":"733","DOI":"10.1145\/3828.3837","volume":"32","author":"PA Sistla","year":"1985","unstructured":"Sistla, P.A., Clarke, E.M.: The complexity of propositional linear temporal logics. J. ACM 32(3), 733\u2013749 (1985)","journal-title":"J. ACM"},{"key":"3_CR43","unstructured":"Thielke, W.: Code geknackt. Link to article in media archive: http:\/\/www.focus.de\/finanzen\/news\/krankenkassen-code-geknackt_aid_148829.html (1994). Accessed Feb 6 2015"},{"key":"3_CR44","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1016\/j.entcs.2006.11.002","volume":"168","author":"R Meyden van der","year":"2007","unstructured":"van der Meyden, R., Zhang, C.: Algorithmic verification of noninterference properties. Electr. Notes Theor. Comput. Sci. 168, 61\u201375 (2007)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"3_CR45","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"471","DOI":"10.1007\/BFb0015261","volume-title":"Computer Science Today","author":"MY Vardi","year":"1995","unstructured":"Vardi, M.Y.: Alternating automata and program verification. In: van Leeuwen, J. (ed.) Computer Science Today. LNCS, vol. 1000, pp. 471\u2013485. Springer, Heidelberg (1995)"},{"key":"3_CR46","unstructured":"Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Proceedings of LICS 1986, pp. 332\u2013344, IEEE CS Press (1986)"},{"issue":"1","key":"3_CR47","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1994.1092","volume":"115","author":"MY Vardi","year":"1994","unstructured":"Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. Inf. Comput. 115(1), 1\u201337 (1994)","journal-title":"Inf. Comput."}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-21690-4_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,29]],"date-time":"2025-05-29T06:29:32Z","timestamp":1748500172000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-21690-4_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319216898","9783319216904"],"references-count":47,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-21690-4_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"16 July 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}