{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T22:06:50Z","timestamp":1784844410607,"version":"3.55.0"},"publisher-location":"Cham","reference-count":25,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030591519","type":"print"},{"value":"9783030591526","type":"electronic"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"vor","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":[[2020]]},"DOI":"10.1007\/978-3-030-59152-6_27","type":"book-chapter","created":{"date-parts":[[2020,10,11]],"date-time":"2020-10-11T23:02:35Z","timestamp":1602457355000},"page":"484-500","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":21,"title":["Probabilistic Hyperproperties of Markov Decision Processes"],"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":"Hazem","family":"Torfah","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2020,10,12]]},"reference":[{"key":"27_CR1","doi-asserted-by":"crossref","unstructured":"Abraham, E., Bartocci, E., Bonakdarpour, B., Dobe, O.: Probabilistic hyperproperties with nondeterminism. In: Proceedings of Automated Technology for Verification and Analysis, ATVA 2020 (2020)","DOI":"10.1007\/978-3-030-59152-6_29"},{"key":"27_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1007\/978-3-319-99154-2_2","volume-title":"Quantitative Evaluation of Systems","author":"E \u00c1brah\u00e1m","year":"2018","unstructured":"\u00c1brah\u00e1m, E., Bonakdarpour, B.: HyperPCTL: a temporal logic for probabilistic hyperproperties. In: McIver, A., Horvath, A. (eds.) QEST 2018. LNCS, vol. 11024, pp. 20\u201335. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-99154-2_2"},{"key":"27_CR3","doi-asserted-by":"crossref","unstructured":"Aminof, B., Kwiatkowska, M., Maubert, B., Murano, A., Rubin, S.: Probabilistic strategy logic. In: Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence, IJCAI 2019, pp. 32\u201338 (2019)","DOI":"10.24963\/ijcai.2019\/5"},{"key":"27_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-16265-7_1","volume-title":"Integrated Formal Methods","author":"C Baier","year":"2010","unstructured":"Baier, C.: On model checking techniques for randomized distributed systems. In: M\u00e9ry, D., Merz, S. (eds.) IFM 2010. LNCS, vol. 6396, pp. 1\u201311. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-16265-7_1"},{"key":"27_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/978-3-540-78499-9_21","volume-title":"Foundations of Software Science and Computational Structures","author":"C Baier","year":"2008","unstructured":"Baier, C., Bertrand, N., Gr\u00f6\u00dfer, M.: On decision problems for probabilistic B\u00fcchi automata. In: Amadio, R. (ed.) FoSSaCS 2008. LNCS, vol. 4962, pp. 287\u2013301. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78499-9_21"},{"issue":"4","key":"27_CR6","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1007\/s00236-012-0156-0","volume":"49","author":"C Baier","year":"2012","unstructured":"Baier, C., Br\u00e1zdil, T., Gr\u00f6\u00dfer, M., Kucera, A.: Stochastic game logic. Acta Inform. 49(4), 203\u2013224 (2012). https:\/\/doi.org\/10.1007\/s00236-012-0156-0","journal-title":"Acta Inform."},{"key":"27_CR7","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"27_CR8","unstructured":"Br\u00e1zdil, T., Brozek, V., Forejt, V., Kucera, A.: Stochastic games with branching-time winning objectives. In: Proceedings of 21th IEEE Symposium on Logic in Computer Science (LICS 2006), pp. 349\u2013358. IEEE Computer Society (2006)"},{"key":"27_CR9","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. LNCS, vol. 8414, pp. 265\u2013284. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54792-8_15"},{"issue":"6","key":"27_CR10","doi-asserted-by":"publisher","first-page":"1157","DOI":"10.3233\/JCS-2009-0393","volume":"18","author":"MR Clarkson","year":"2010","unstructured":"Clarkson, M.R., Schneider, F.B.: Hyperproperties. J. Comput. Secur. 18(6), 1157\u20131210 (2010)","journal-title":"J. Comput. Secur."},{"key":"27_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/978-3-030-25540-4_7","volume-title":"Computer Aided Verification","author":"N Coenen","year":"2019","unstructured":"Coenen, N., Finkbeiner, B., S\u00e1nchez, C., Tentrup, L.: Verifying hyperliveness. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11561, pp. 121\u2013139. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_7"},{"key":"27_CR12","doi-asserted-by":"crossref","unstructured":"Dimitrova, R., Finkbeiner, B., Torfah, H.: Probabilistic hyperproperties of Markov decision processes. CoRR arxiv:2005.03362 (2020)","DOI":"10.1007\/978-3-030-59152-6_27"},{"key":"27_CR13","doi-asserted-by":"publisher","first-page":"338","DOI":"10.1007\/978-1-4419-5906-5_752","volume-title":"Encyclopedia of Cryptography and Security","author":"C Dwork","year":"2011","unstructured":"Dwork, C.: Differential privacy. In: van Tilborg, H.C.A., Jajodia, S. (eds.) Encyclopedia of Cryptography and Security, 2nd edn., pp. 338\u2013340. Springer, Boston (2011). https:\/\/doi.org\/10.1007\/978-1-4419-5906-5_752","edition":"2"},{"key":"27_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"289","DOI":"10.1007\/978-3-319-96145-3_16","volume-title":"Computer Aided Verification","author":"B Finkbeiner","year":"2018","unstructured":"Finkbeiner, B., Hahn, C., Lukert, P., Stenger, M., Tentrup, L.: Synthesizing reactive systems from hyperproperties. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10981, pp. 289\u2013306. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96145-3_16"},{"key":"27_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"564","DOI":"10.1007\/978-3-319-63390-9_29","volume-title":"Computer Aided Verification","author":"B Finkbeiner","year":"2017","unstructured":"Finkbeiner, B., Hahn, C., Stenger, M.: EAHyper: satisfiability, implication, and equivalence checking of hyperproperties. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 564\u2013570. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63390-9_29"},{"key":"27_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1007\/978-3-319-21690-4_3","volume-title":"Computer Aided Verification","author":"B Finkbeiner","year":"2015","unstructured":"Finkbeiner, B., Rabe, M.N., S\u00e1nchez, C.: Algorithms for model checking HyperLTL and HyperCTL$$^*$$. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 30\u201348. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_3"},{"key":"27_CR17","doi-asserted-by":"crossref","unstructured":"Goguen, J.A., Meseguer, J.: Security policies and security models. In: 1982 IEEE Symposium on Security and Privacy. IEEE Computer Society (1982)","DOI":"10.1109\/SP.1982.10014"},{"issue":"3\u20134","key":"27_CR18","doi-asserted-by":"publisher","first-page":"255","DOI":"10.3233\/JCS-1992-13-405","volume":"1","author":"JW Gray","year":"1992","unstructured":"Gray, J.W.: Toward a mathematical foundation for information flow security. J. Comput. Secur. 1(3\u20134), 255\u2013294 (1992)","journal-title":"J. Comput. Secur."},{"key":"27_CR19","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/978-3-319-57685-5_3","volume-title":"Formal System Verification","author":"M Kwiatkowska","year":"2018","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Probabilistic model checking: advances and applications. In: Drechsler, R. (ed.) Formal System Verification, pp. 73\u2013121. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-57685-5_3"},{"key":"27_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/978-3-642-22110-1_47","volume-title":"Computer Aided Verification","author":"M Kwiatkowska","year":"2011","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585\u2013591. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_47"},{"key":"27_CR21","unstructured":"O\u2019Neill, K.R., Clarkson, M.R., Chong, S.: Information-flow security for interactive programs. In: 19th IEEE Computer Security Foundations Workshop, (CSFW-19 2006), pp. 190\u2013201. IEEE Computer Society (2006)"},{"key":"27_CR22","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science, pp. 46\u201357. IEEE Computer Society (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"27_CR23","unstructured":"Sabelfeld, A., Sands, D.: Probabilistic noninterference for multi-threaded programs. In: Proceedings of the 13th IEEE Computer Security Foundations Workshop, CSFW 2000, pp. 200\u2013214. IEEE Computer Society (2000)"},{"issue":"1","key":"27_CR24","doi-asserted-by":"publisher","first-page":"231","DOI":"10.3233\/JCS-1999-72-305","volume":"7","author":"DM Volpano","year":"1999","unstructured":"Volpano, D.M., Smith, G.: Probabilistic noninterference in a concurrent language. J. Comput. Secur. 7(1), 231\u2013253 (1999)","journal-title":"J. Comput. Secur."},{"issue":"5s","key":"27_CR25","first-page":"1","volume":"18","author":"Y Wang","year":"2019","unstructured":"Wang, Y., Zarei, M., Bonakdarpour, B., Pajic, M.: Statistical verification of hyperproperties for cyber-physical systems. ACM Trans. Embed. Comput. Syst. 18(5s), 1\u201323 (2019)","journal-title":"ACM Trans. Embed. Comput. Syst."}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-59152-6_27","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,7]],"date-time":"2021-04-07T23:48:22Z","timestamp":1617839302000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-59152-6_27"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030591519","9783030591526"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-59152-6_27","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"12 October 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ATVA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Automated Technology for Verification and Analysis","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Hanoi","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Vietnam","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"19 October 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23 October 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"atva2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/fit.uet.vnu.edu.vn\/atva2020\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"easychair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"75","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"27","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"36% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"6","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}