{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,1]],"date-time":"2026-06-01T18:29:40Z","timestamp":1780338580264,"version":"3.54.1"},"publisher-location":"Berlin, Heidelberg","reference-count":61,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642547911","type":"print"},{"value":"9783642547928","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-642-54792-8_15","type":"book-chapter","created":{"date-parts":[[2014,3,21]],"date-time":"2014-03-21T13:35:12Z","timestamp":1395408912000},"page":"265-284","source":"Crossref","is-referenced-by-count":206,"title":["Temporal Logics for Hyperproperties"],"prefix":"10.1007","author":[{"given":"Michael R.","family":"Clarkson","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Bernd","family":"Finkbeiner","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Masoud","family":"Koleini","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Kristopher K.","family":"Micinski","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Markus N.","family":"Rabe","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"C\u00e9sar","family":"S\u00e1nchez","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"15_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":"15_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":"15_CR3","unstructured":"Andersen, H.R.: A polyadic modal mu-calculus. Technical Report 1994-145, Technical University of Denmark, DTU (1994)"},{"key":"15_CR4","doi-asserted-by":"crossref","unstructured":"Balliu, M., Dam, M., Guernic, G.L.: Epistemic temporal logic for information flow security. In: Proc. Workshop on Programming Languages and Analysis for Security (June 2011)","DOI":"10.1145\/2166956.2166962"},{"issue":"2","key":"15_CR5","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1017\/S0956796804005453","volume":"15","author":"A. Banerjee","year":"2005","unstructured":"Banerjee, A., Naumann, D.A.: Stack-based access control and secure information flow. Journal of Functional Programming\u00a015(2), 131\u2013177 (2005)","journal-title":"Journal of Functional Programming"},{"key":"15_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.\u00a07734, pp. 29\u201343. Springer, Heidelberg (2013)"},{"key":"15_CR7","doi-asserted-by":"crossref","unstructured":"Barthe, G., D\u2019Argenio, P.R., Rezk, T.: Secure information flow by self-composition. In: Proc. IEEE Computer Security Foundations Workshop, pp. 100\u2013114 (June 2004)","DOI":"10.1109\/CSFW.2004.1310735"},{"key":"15_CR8","doi-asserted-by":"publisher","first-page":"721","DOI":"10.1016\/S1570-2464(07)80015-2","volume-title":"Handbook of Modal Logic","author":"J. Bradfield","year":"2007","unstructured":"Bradfield, J., Stirling, C.: Modal mu-calculi. In: Handbook of Modal Logic, pp. 721\u2013756. Elsevier, Amsterdam (2007)"},{"key":"15_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/11679219_7","volume-title":"Formal Aspects in Security and Trust","author":"J.W. Bryans","year":"2006","unstructured":"Bryans, J.W., Koutny, M., Mazar\u00e9, L., Ryan, P.Y.A.: Opacity generalised to transition systems. In: Dimitrakos, T., Martinelli, F., Ryan, P.Y.A., Schneider, S. (eds.) FAST 2005. LNCS, vol.\u00a03866, pp. 81\u201395. Springer, Heidelberg (2006)"},{"key":"15_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1007\/978-3-642-02138-1_12","volume-title":"Formal Techniques for Distributed Systems","author":"R. Chadha","year":"2009","unstructured":"Chadha, R., Delaune, S., Kremer, S.: Epistemic logic for the applied pi calculus. In: Lee, D., Lopes, A., Poetzsch-Heffter, A. (eds.) FMOODS 2009. LNCS, vol.\u00a05522, pp. 182\u2013197. Springer, Heidelberg (2009)"},{"key":"15_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"495","DOI":"10.1007\/3-540-48683-6_44","volume-title":"Computer Aided Verification","author":"A. Cimatti","year":"1999","unstructured":"Cimatti, A., Clarke, E., Giunchiglia, F., Roveri, M.: NuSMV: A new symbolic model verifier. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 495\u2013499. Springer, Heidelberg (1999)"},{"key":"15_CR12","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1016\/j.entcs.2004.01.018","volume":"112","author":"D. Clark","year":"2005","unstructured":"Clark, D., Hunt, S., Malacaria, P.: Quantified interference for a while language. Electronic Notes in Theoretical Computer Science\u00a0112, 149\u2013166 (2005)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"15_CR13","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 (January 2014), http:\/\/arxiv.org\/abs\/1401.4492","DOI":"10.1007\/978-3-642-54792-8_15"},{"issue":"5","key":"15_CR14","doi-asserted-by":"crossref","first-page":"655","DOI":"10.3233\/JCS-2009-0353","volume":"17","author":"M.R. Clarkson","year":"2009","unstructured":"Clarkson, M.R., Myers, A.C., Schneider, F.B.: Quantifying information flow with beliefs. Journal of Computer Security\u00a017(5), 655\u2013701 (2009)","journal-title":"Journal of Computer Security"},{"issue":"6","key":"15_CR15","doi-asserted-by":"crossref","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(6), 1157\u20131210 (2010)","journal-title":"Journal of Computer Security"},{"key":"15_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1007\/978-3-642-22110-1_26","volume-title":"Computer Aided Verification","author":"B. Cook","year":"2011","unstructured":"Cook, B., Koskinen, E., Vardi, M.: Temporal property verification as a program analysis task. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 333\u2013348. Springer, Heidelberg (2011)"},{"key":"15_CR17","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":"15_CR18","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1145\/4904.4999","volume":"33","author":"E.A. Emerson","year":"1986","unstructured":"Emerson, E.A., Halpern, J.Y.: \u201cSometimes\u201d and \u201cnot never\u201d revisited: On branching versus linear time temporal logic. Journal of the ACM\u00a033(1), 151\u2013178 (1986)","journal-title":"Journal of the ACM"},{"key":"15_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":"15_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1007\/3-540-45608-2_6","volume-title":"Foundations of Security Analysis and Design","author":"R. Focardi","year":"2001","unstructured":"Focardi, R., Gorrieri, R.: Classification of security properties (Part I: Information flow. In: Focardi, R., Gorrieri, R. (eds.) FOSAD 2000. LNCS, vol.\u00a02171, pp. 331\u2013396. Springer, Heidelberg (2001)"},{"key":"15_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/3-540-44585-4_6","volume-title":"Computer Aided Verification","author":"P. Gastin","year":"2001","unstructured":"Gastin, P., Oddoux, D.: Fast LTL to B\u00fcchi automata translation. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 53\u201365. Springer, Heidelberg (2001)"},{"key":"15_CR22","doi-asserted-by":"crossref","unstructured":"Gerth, R., Peled, D., Vardi, M.Y., Wolper, P.: Simple on-the-fly automatic verification of linear temporal logic. In: Proc. Protocol Specification, Testing and Verification, pp. 3\u201318 (June 1995)","DOI":"10.1007\/978-0-387-34892-6_1"},{"key":"15_CR23","doi-asserted-by":"crossref","unstructured":"Goguen, J.A., Meseguer, J.: Security policies and security models. In: Proc. IEEE Symposium on Security and Privacy, pp. 11\u201320 (April 1982)","DOI":"10.1109\/SP.1982.10014"},{"key":"15_CR24","unstructured":"Gray III, J.W.: Toward a mathematical foundation for information flow security. In: Proc. IEEE Symposium on Security and Privacy, pp. 210\u2013234 (May 1991)"},{"issue":"2","key":"15_CR25","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/s004460050043","volume":"11","author":"J.W. Gray III","year":"1998","unstructured":"Gray III, J.W., Syverson, P.F.: A logical approach to multilevel security of probabilistic systems. Distributed Computing\u00a011(2), 73\u201390 (1998)","journal-title":"Distributed Computing"},{"issue":"1","key":"15_CR26","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/1410234.1410239","volume":"12","author":"J.Y. Halpern","year":"2008","unstructured":"Halpern, J.Y., O\u2019Neill, K.R.: Secrecy in multiagent systems. ACM Transactions on Information and System Security\u00a012(1), 5:1\u20135:47 (2008)","journal-title":"ACM Transactions on Information and System Security"},{"issue":"6","key":"15_CR27","doi-asserted-by":"publisher","first-page":"399","DOI":"10.1007\/s10207-009-0086-1","volume":"8","author":"C. Hammer","year":"2009","unstructured":"Hammer, C., Snelting, G.: Flow-sensitive, context-sensitive, and object-sensitive information flow control based on program dependence graphs. International Journal of Information Security\u00a08(6), 399\u2013422 (2009)","journal-title":"International Journal of Information Security"},{"key":"15_CR28","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G.J. Holzmann","year":"1997","unstructured":"Holzmann, G.J.: The model checker SPIN. IEEE Transactions on Software Engineering\u00a023, 279\u2013295 (1997)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"15_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"148","DOI":"10.1007\/978-3-642-27375-9_9","volume-title":"Theory of Security and Applications","author":"M. Huisman","year":"2012","unstructured":"Huisman, M., Blondeel, H.-C.: Model-checking secure information flow for multi-threaded programs. In: M\u00f6dersheim, S., Palamidessi, C. (eds.) TOSCA 2011. LNCS, vol.\u00a06993, pp. 148\u2013165. Springer, Heidelberg (2012)"},{"key":"15_CR30","doi-asserted-by":"crossref","unstructured":"Huisman, M., Worah, P., Sunesen, K.: A temporal logic characterisation of observational determinism. In: Proc. IEEE Computer Security Foundations Workshop, pp. 3\u201315 (July 2006)","DOI":"10.1109\/CSFW.2006.6"},{"key":"15_CR31","doi-asserted-by":"crossref","unstructured":"K\u00f6pf, B., Basin, D.: An information-theoretic model for adaptive side-channel attacks. In: Proc. ACM Conference on Computer and Communications Security, pp. 286\u2013296 (October 2007)","DOI":"10.1145\/1315245.1315282"},{"issue":"2","key":"15_CR32","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1109\/TSE.1977.229904","volume":"3","author":"L. Lamport","year":"1977","unstructured":"Lamport, L.: Proving the correctness of multiprocess programs. IEEE Transactions on Software Engineering\u00a03(2), 125\u2013143 (1977)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"15_CR33","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0931-7","volume-title":"The Temporal Logic of Reactive and Concurrent Systems: Specification","author":"Z. Manna","year":"1992","unstructured":"Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer, New York (1992)"},{"key":"15_CR34","doi-asserted-by":"crossref","unstructured":"Mantel, H.: Possibilistic definitions of security\u2014an assembly kit. In: Proc. IEEE Computer Security Foundations Workshop, pp. 185\u2013199 (July 2000)","DOI":"10.1109\/CSFW.2000.856936"},{"key":"15_CR35","doi-asserted-by":"crossref","unstructured":"McCullough, D.: Noninterference and the composability of security properties. In: Proc. IEEE Symposium on Security and Privacy, pp. 177\u2013186 (April 1988)","DOI":"10.1109\/SECPRI.1988.8110"},{"issue":"6","key":"15_CR36","doi-asserted-by":"publisher","first-page":"563","DOI":"10.1109\/32.55085","volume":"16","author":"D. McCullough","year":"1990","unstructured":"McCullough, D.: A hookup theorem for multilevel security. Proc. IEEE Transactions on Software Engineering\u00a016(6), 563\u2013568 (1990)","journal-title":"Proc. IEEE Transactions on Software Engineering"},{"issue":"1","key":"15_CR37","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":"15_CR38","doi-asserted-by":"crossref","unstructured":"McLean, J.: A general theory of composition for trace sets closed under selective interleaving functions. In: Proc. IEEE Symposium on Security and Privacy, pp. 79\u201393 (April 1994)","DOI":"10.1109\/RISP.1994.296590"},{"key":"15_CR39","doi-asserted-by":"crossref","unstructured":"Millen, J.K.: Unwinding forward correctability. In: Proc. IEEE Computer Security Foundations Workshop, pp. 2\u201310 (June 1994)","DOI":"10.1109\/CSFW.1994.315952"},{"key":"15_CR40","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.) POST 2012. LNCS, vol.\u00a07215, pp. 329\u2013348. Springer, Heidelberg (2012)"},{"key":"15_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1007\/978-3-642-41488-6_17","volume-title":"Secure IT Systems","author":"D. Milushev","year":"2013","unstructured":"Milushev, D., Clarke, D.: Incremental hyperproperty model checking via games. In: Riis Nielson, H., Gollmann, D. (eds.) NordSec 2013. LNCS, vol.\u00a08208, pp. 247\u2013262. Springer, Heidelberg (2013)"},{"key":"15_CR42","unstructured":"Milushev, D.V.: Reasoning about Hyperproperties. PhD thesis, Katholieke Universiteit Leuven (June 2013)"},{"key":"15_CR43","doi-asserted-by":"crossref","unstructured":"Myers, A.C.: JFlow: Practical mostly-static information flow control. In: Proc. ACM Symposium on Principles of Programming Languages, pp. 228\u2013241 (1999)","DOI":"10.1145\/292540.292561"},{"key":"15_CR44","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: Proc. Foundations of Computer Science, pp. 46\u201357 (September 1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"15_CR45","unstructured":"Rogers, H.: Theory of Recursive Functions and Effective Computability. MIT Press, Cambridge (1987)"},{"key":"15_CR46","doi-asserted-by":"crossref","unstructured":"Roscoe, A.W.: CSP and determinism in security modelling. In: Proc. IEEE Symposium on Security and Privacy, pp. 114\u2013127 (May 1995)","DOI":"10.1109\/SECPRI.1995.398927"},{"key":"15_CR47","unstructured":"Ryan, P.Y.A., Peacock, T.: Opacity\u2014further insights on an information flow property. Technical Report CS-TR-958, Newcastle University (April 2006)"},{"issue":"1","key":"15_CR48","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1109\/JSAC.2002.806121","volume":"21","author":"A. Sabelfeld","year":"2003","unstructured":"Sabelfeld, A., Myers, A.C.: Language-based information-flow security. IEEE Journal on Selected Areas in Communications\u00a021(1), 5\u201319 (2003)","journal-title":"IEEE Journal on Selected Areas in Communications"},{"key":"15_CR49","doi-asserted-by":"crossref","unstructured":"Sabelfeld, A., Sands, D.: Dimensions and principles of declassification. In: Proc. IEEE Computer Security Foundations Workshop, pp. 255\u2013269 (2005)","DOI":"10.1109\/CSFW.2005.15"},{"key":"15_CR50","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1016\/0304-3975(87)90008-9","volume":"49","author":"A.P. Sistla","year":"1987","unstructured":"Sistla, A.P., Vardi, M.Y., 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":"15_CR51","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"288","DOI":"10.1007\/978-3-642-00596-1_21","volume-title":"Foundations of Software Science and Computational Structures","author":"G. Smith","year":"2009","unstructured":"Smith, G.: On the foundations of quantitative information flow. In: de Alfaro, L. (ed.) FOSSACS 2009. LNCS, vol.\u00a05504, pp. 288\u2013302. Springer, Heidelberg (2009)"},{"key":"15_CR52","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"352","DOI":"10.1007\/11547662_24","volume-title":"Static Analysis","author":"T. Terauchi","year":"2005","unstructured":"Terauchi, T., Aiken, A.: Secure information flow as a safety problem. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol.\u00a03672, pp. 352\u2013367. Springer, Heidelberg (2005)"},{"key":"15_CR53","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"466","DOI":"10.1007\/978-3-540-71209-1_35","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Y.-K. Tsay","year":"2007","unstructured":"Tsay, Y.-K., Chen, Y.-F., Tsai, M.-H., Wu, K.-N., Chan, W.-C.: GOAL: A graphical tool for manipulating B\u00fcchi automata and temporal formulae. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol.\u00a04424, pp. 466\u2013471. Springer, Heidelberg (2007)"},{"key":"15_CR54","doi-asserted-by":"crossref","unstructured":"van der Meyden, R.: Axioms for knowledge and time in distributed systems with perfect recall. In: Proc. IEEE Symposium on Logic in Computer Science, pp. 448\u2013457 (1993)","DOI":"10.1109\/LICS.1994.316046"},{"key":"15_CR55","doi-asserted-by":"crossref","unstructured":"van der Meyden, R., Wilke, T.: Preservation of epistemic properties in security protocol implementations. In: Proc. ACM Conference on Theoretical Aspects of Rationality and Knowledge, pp. 212\u2013221 (2007)","DOI":"10.1145\/1324249.1324278"},{"key":"15_CR56","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. Electronic Notes in Theoretical Computer Science\u00a0168, 61\u201375 (2007)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"15_CR57","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"238","DOI":"10.1007\/3-540-60915-6_6","volume-title":"Logics for Concurrency","author":"M.Y. Vardi","year":"1996","unstructured":"Vardi, M.Y.: An automata-theoretic approach to linear temporal logic. In: Moller, F., Birtwistle, G. (eds.) Logics for Concurrency. LNCS, vol.\u00a01043, pp. 238\u2013266. Springer, Heidelberg (1996)"},{"issue":"1","key":"15_CR58","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. Information and Computation\u00a0115(1), 1\u201337 (1994)","journal-title":"Information and Computation"},{"key":"15_CR59","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/3-540-44667-2_7","volume-title":"Lectures on Formal Methods and Performance Analysis","author":"P. Wolper","year":"2001","unstructured":"Wolper, P.: Constructing automata from temporal logic formulas: A tutorial. In: Brinksma, E., Hermanns, H., Katoen, J.-P. (eds.) FMPA 2000. LNCS, vol.\u00a02090, pp. 261\u2013277. Springer, Heidelberg (2001)"},{"key":"15_CR60","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1007\/978-3-642-15497-3_22","volume-title":"Computer Security \u2013 ESORICS 2010","author":"H. Yasuoka","year":"2010","unstructured":"Yasuoka, H., Terauchi, T.: On bounding problems of quantitative information flow. In: Gritzalis, D., Preneel, B., Theoharidou, M. (eds.) ESORICS 2010. LNCS, vol.\u00a06345, pp. 357\u2013372. Springer, Heidelberg (2010)"},{"key":"15_CR61","doi-asserted-by":"crossref","unstructured":"Zdancewic, S., Myers, A.C.: Observational determinism for concurrent program security. In: Proc. IEEE Computer Security Foundations Workshop, pp. 29\u201343 (June 2003)","DOI":"10.1109\/CSFW.2003.1212703"}],"container-title":["Lecture Notes in Computer Science","Principles of Security and Trust"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-54792-8_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,2]],"date-time":"2025-05-02T03:47:10Z","timestamp":1746157630000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-54792-8_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783642547911","9783642547928"],"references-count":61,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-54792-8_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014]]}}}