{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,1]],"date-time":"2026-06-01T18:27:24Z","timestamp":1780338444431,"version":"3.54.1"},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642279393","type":"print"},{"value":"9783642279409","type":"electronic"}],"license":[{"start":{"date-parts":[[2012,1,1]],"date-time":"2012-01-01T00:00:00Z","timestamp":1325376000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-27940-9_12","type":"book-chapter","created":{"date-parts":[[2012,1,19]],"date-time":"2012-01-19T07:29:29Z","timestamp":1326958169000},"page":"169-185","source":"Crossref","is-referenced-by-count":42,"title":["Model Checking Information Flow in Reactive Systems"],"prefix":"10.1007","author":[{"given":"Rayna","family":"Dimitrova","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Bernd","family":"Finkbeiner","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"M\u00e1t\u00e9","family":"Kov\u00e1cs","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Markus N.","family":"Rabe","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Helmut","family":"Seidl","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"12_CR1","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1994.1092","volume":"115","author":"M.Y. Vardi","year":"1994","unstructured":"Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. Inf. Comput.\u00a0115, 1\u201337 (1994)","journal-title":"Inf. Comput."},{"key":"12_CR2","doi-asserted-by":"publisher","first-page":"312","DOI":"10.1145\/333979.333987","volume":"47","author":"O. Kupferman","year":"2000","unstructured":"Kupferman, O., Vardi, M.Y., Wolper, P.: An automata-theoretic approach to branching-time model checking. J. ACM\u00a047, 312\u2013360 (2000)","journal-title":"J. ACM"},{"key":"12_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"471","DOI":"10.1007\/BFb0015261","volume-title":"Computer Science Today","author":"M.Y. Vardi","year":"1995","unstructured":"Vardi, M.Y.: Alternating Automata and Program Verification. In: van Leeuwen, J. (ed.) Computer Science Today. LNCS, vol.\u00a01000, pp. 471\u2013485. Springer, Heidelberg (1995)"},{"key":"12_CR4","doi-asserted-by":"crossref","unstructured":"Goguen, J.A., Meseguer, J.: Security policies and security models. In: IEEE Symposium on Security and Privacy, pp. 11\u201320 (1982)","DOI":"10.1109\/SP.1982.10014"},{"key":"12_CR5","unstructured":"Zdancewic, S., Myers, A.C.: Observational determinism for concurrent program security. In: Proc. 16th IEEE Computer Security Foundations Workshop (2003)"},{"key":"12_CR6","doi-asserted-by":"crossref","unstructured":"Broberg, N., Sands, D.: Paralocks \u2013 role-based information flow control and beyond. In: Proc. of POPL 2010 (2010)","DOI":"10.1145\/1706299.1706349"},{"key":"12_CR7","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.\u00a06012, pp. 64\u201384. Springer, Heidelberg (2010)"},{"key":"12_CR8","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":"12_CR9","doi-asserted-by":"publisher","first-page":"1157","DOI":"10.3233\/JCS-2009-0393","volume":"18","author":"M.R. Clarkson","year":"2010","unstructured":"Clarkson, M.R., Schneider, F.B.: Hyperproperties. Journal of Computer Security\u00a018, 1157\u20131210 (2010)","journal-title":"Journal of Computer Security"},{"key":"12_CR10","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.\u00a032, 321\u2013330 (1984)","journal-title":"Theor. Comput. Sci."},{"key":"12_CR11","doi-asserted-by":"crossref","unstructured":"Huisman, M., Worah, P., Sunesen, K.: A temporal logic characterisation of observational determinism. In: CSFW, p. 3. IEEE Computer Society (2006)","DOI":"10.1109\/CSFW.2006.6"},{"key":"12_CR12","doi-asserted-by":"crossref","unstructured":"Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.Y.: Reasoning About Knowledge. MIT Press (1995)","DOI":"10.7551\/mitpress\/5803.001.0001"},{"key":"12_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"432","DOI":"10.1007\/3-540-46691-6_35","volume-title":"Foundations of Software Technology and Theoretical Computer Science","author":"R. Meyden van der","year":"1999","unstructured":"van der Meyden, R., Shilov, N.V.: Model Checking Knowledge and Time in Systems with Perfect Recall. In: Pandu Rangan, C., Raman, V., Sarukkai, S. (eds.) FST TCS 1999. LNCS, vol.\u00a01738, pp. 432\u2013445. Springer, Heidelberg (1999)"},{"key":"12_CR14","unstructured":"Shilov, N.V., Garanina, N.O.: Model checking knowledge and fixpoints. In: FICS, pp. 25\u201339 (2002)"},{"key":"12_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1007\/978-3-540-72734-7_14","volume-title":"Logical Foundations of Computer Science","author":"K. Engelhardt","year":"2007","unstructured":"Engelhardt, K., Gammie, P., van der Meyden, R.: Model Checking Knowledge and Linear Time: PSPACE Cases. In: Artemov, S., Nerode, A. (eds.) LFCS 2007. LNCS, vol.\u00a04514, pp. 195\u2013211. Springer, Heidelberg (2007)"},{"key":"12_CR16","doi-asserted-by":"crossref","unstructured":"Balliu, M., Dam, M., Guernic, G.L.: Epistemic temporal logic for information flow security. In: Proc. PLAS 2011 (2011)","DOI":"10.1145\/2166956.2166962"},{"key":"12_CR17","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)"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-27940-9_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,18]],"date-time":"2025-03-18T23:24:40Z","timestamp":1742340280000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-27940-9_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642279393","9783642279409"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-27940-9_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012]]}}}