{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T08:56:37Z","timestamp":1743152197403,"version":"3.40.3"},"publisher-location":"Cham","reference-count":50,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031757778"},{"type":"electronic","value":"9783031757785"}],"license":[{"start":{"date-parts":[[2024,11,18]],"date-time":"2024-11-18T00:00:00Z","timestamp":1731888000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,11,18]],"date-time":"2024-11-18T00:00:00Z","timestamp":1731888000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"DOI":"10.1007\/978-3-031-75778-5_17","type":"book-chapter","created":{"date-parts":[[2024,11,17]],"date-time":"2024-11-17T12:09:20Z","timestamp":1731845360000},"page":"351-373","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Urgency Annotations for\u00a0Alternating Choices"],"prefix":"10.1007","author":[{"given":"Eren","family":"Keskin","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Roland","family":"Meyer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"S\u00f6ren","family":"van der Wall","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,11,18]]},"reference":[{"issue":"POPL","key":"17_CR1","first-page":"34:1","volume":"3","author":"K Batz","year":"2019","unstructured":"Batz, K., Kaminski, B.L., Katoen, J., Matheja, C., Noll, T.: Quantitative separation logic: a logic for reasoning about probabilistic pointer programs. PACMPL 3(POPL), 34:1-34:29 (2019)","journal-title":"PACMPL"},{"issue":"POPL","key":"17_CR2","first-page":"1","volume":"5","author":"K Batz","year":"2021","unstructured":"Batz, K., Kaminski, B.L., Katoen, J., Matheja, C.: Relatively complete verification of probabilistic programs: an expressive language for expectation-based reasoning. PACMPL 5(POPL), 1\u201330 (2021)","journal-title":"PACMPL"},{"issue":"OOPSLA1","key":"17_CR3","first-page":"1","volume":"6","author":"K Batz","year":"2022","unstructured":"Batz, K., Gallus, A., Kaminski, B.L., Katoen, J., Winkler, T.: Weighted programming: a programming paradigm for specifying mathematical models. PACMPL 6(OOPSLA1), 1\u201330 (2022)","journal-title":"PACMPL"},{"issue":"POPL","key":"17_CR4","first-page":"1957","volume":"7","author":"K Batz","year":"2023","unstructured":"Batz, K., Kaminski, B.L., Katoen, J., Matheja, C., Verscht, L.: A calculus for amortized expected runtimes. PACMPL 7(POPL), 1957\u20131986 (2023)","journal-title":"PACMPL"},{"issue":"OOPSLA2","key":"17_CR5","first-page":"2052","volume":"7","author":"P Schr\u00f6er","year":"2023","unstructured":"Schr\u00f6er, P., Batz, K., Kaminski, B.L., Katoen, J., Matheja, C.: A deductive verification infrastructure for probabilistic programs. PACMPL 7(OOPSLA2), 2052\u20132082 (2023)","journal-title":"PACMPL"},{"issue":"OOPSLA1","key":"17_CR6","first-page":"696","volume":"7","author":"S Feng","year":"2023","unstructured":"Feng, S., Chen, M., Su, H., Kaminski, B.L., Katoen, J., Zhan, N.: Lower bounds for possibly divergent probabilistic programs. PACMPL 7(OOPSLA1), 696\u2013726 (2023)","journal-title":"PACMPL"},{"issue":"POPL","key":"17_CR7","first-page":"2792","volume":"8","author":"K Batz","year":"2024","unstructured":"Batz, K., Biskup, T.J., Katoen, J., Winkler, T.: Programmatic strategy synthesis: resolving nondeterminism in probabilistic programs. PACMPL 8(POPL), 2792\u20132820 (2024)","journal-title":"PACMPL"},{"key":"17_CR8","unstructured":"Terui, K.: Semantic evaluation, intersection types and complexity of simply typed lambda calculus. In: RTA, ser. LIPIcs, vol.\u00a015. Dagstuhl, pp. 323\u2013338 (2012)"},{"key":"17_CR9","doi-asserted-by":"crossref","unstructured":"Aehlig, K.: A finite semantics of simply-typed lambda terms for infinite runs of automata. LMCS 3(3) (2007)","DOI":"10.2168\/LMCS-3(3:1)2007"},{"key":"17_CR10","doi-asserted-by":"crossref","unstructured":"Salvati, S., Walukiewicz, I.: Using models to model-check recursive schemes. LMCS 11(2) (2015)","DOI":"10.2168\/LMCS-11(2:7)2015"},{"key":"17_CR11","unstructured":"Milner, R.: An algebraic definition of simulation between programs. In: IJCAI. Kaufmann, pp. 481\u2013489 (1971)"},{"key":"17_CR12","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: FOCS, pp. 46\u201357. IEEE (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"17_CR13","unstructured":"Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: LICS, pp. 332\u2013344. IEEE (1986)"},{"key":"17_CR14","doi-asserted-by":"crossref","unstructured":"Emerson, E.A., Jutla, C.S.: Tree automata, mu-calculus and determinacy. In: FOCS, pp. 368\u2013377. IEEE (1991)","DOI":"10.1109\/SFCS.1991.185392"},{"issue":"1","key":"17_CR15","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0304-3975(77)90053-6","volume":"4","author":"R Milner","year":"1977","unstructured":"Milner, R.: Fully abstract models of typed $$\\lambda $$-calculi. TCS 4(1), 1\u201322 (1977)","journal-title":"TCS"},{"issue":"1","key":"17_CR16","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1145\/322234.322243","volume":"28","author":"AK Chandra","year":"1981","unstructured":"Chandra, A.K., Kozen, D., Stockmeyer, L.J.: Alternation. JACM 28(1), 114\u2013133 (1981)","journal-title":"JACM"},{"issue":"2","key":"17_CR17","first-page":"274","volume":"29","author":"JH Reif","year":"1984","unstructured":"Reif, J.H.: The complexity of two-player games of incomplete information. JCSS 29(2), 274\u2013301 (1984)","journal-title":"JCSS"},{"key":"17_CR18","doi-asserted-by":"crossref","unstructured":"Bozzelli, L.: New results on pushdown module checking with imperfect information. In: GandALF, ser. EPTCS, vol.\u00a054, pp. 162\u2013177 (2011)","DOI":"10.4204\/EPTCS.54.12"},{"key":"17_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/978-3-030-72019-3_13","volume-title":"Programming Languages and Systems","author":"G Jaber","year":"2021","unstructured":"Jaber, G., Murawski, A.S.: Complete trace models of state and control. In: ESOP 2021. LNCS, vol. 12648, pp. 348\u2013374. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-72019-3_13"},{"key":"17_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"395","DOI":"10.1007\/978-3-540-92687-0_27","volume-title":"Logical Foundations of Computer Science","author":"A Seth","year":"2008","unstructured":"Seth, A.: Games on multi-stack pushdown systems. In: Artemov, S., Nerode, A. (eds.) LFCS 2009. LNCS, vol. 5407, pp. 395\u2013408. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-92687-0_27"},{"issue":"6","key":"17_CR21","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. JCS 18(6), 1157\u20131210 (2010)","journal-title":"JCS"},{"key":"17_CR22","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"},{"key":"17_CR23","unstructured":"Keskin, E., Meyer, R., van\u00a0der Wall, S.: Urgency annotations for alternating choices. https:\/\/arxiv.org\/abs\/2305.02967"},{"issue":"2","key":"17_CR24","first-page":"363","volume":"102","author":"DA Martin","year":"1975","unstructured":"Martin, D.A.: Borel determinacy. AMATH 102(2), 363\u2013371 (1975)","journal-title":"AMATH"},{"issue":"1","key":"17_CR25","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1145\/2455.2460","volume":"32","author":"M Hennessy","year":"1985","unstructured":"Hennessy, M., Milner, R.: Algebraic laws for nondeterminism and concurrency. JACM 32(1), 137\u2013161 (1985)","journal-title":"JACM"},{"key":"17_CR26","unstructured":"Bergstra, J.A., Ponse, A., Smolka, S.A. (eds.): Handbook of Process Algebra. Elsevier (2001)"},{"key":"17_CR27","unstructured":"Birkhoff, G.: Lattice Theory. AMS (1967)"},{"issue":"2","key":"17_CR28","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1147\/rd.32.0114","volume":"3","author":"MO Rabin","year":"1959","unstructured":"Rabin, M.O., Scott, D.S.: Finite automata and their decision problems. IBM J. Res. Dev. 3(2), 114\u2013125 (1959)","journal-title":"IBM J. Res. Dev."},{"key":"17_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-540-31980-1_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Qadeer","year":"2005","unstructured":"Qadeer, S., Rehof, J.: Context-bounded model checking of concurrent software. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 93\u2013107. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-31980-1_7"},{"key":"17_CR30","unstructured":"Meyer, R., van\u00a0der Wall, S.: On the complexity of multi-pushdown games. In: FSTTCS, ser. LIPIcs, vol. 182, pp. 52:1\u201352:35. Dagstuhl (2020)"},{"issue":"2","key":"17_CR31","doi-asserted-by":"publisher","first-page":"416","DOI":"10.1145\/349214.349241","volume":"22","author":"G Ramalingam","year":"2000","unstructured":"Ramalingam, G.: Context-sensitive synchronization-sensitive analysis is undecidable. TOPLAS 22(2), 416\u2013430 (2000)","journal-title":"TOPLAS"},{"key":"17_CR32","doi-asserted-by":"crossref","unstructured":"Barthe, G., D\u2019Argenio, P.R., Rezk, T.: Secure information flow by self-composition. In: CSFW, pp. 100\u2013114. IEEE (2004)","DOI":"10.1109\/CSFW.2004.1310735"},{"key":"17_CR33","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":"17_CR34","unstructured":"Gutsfeld, J.O., M\u00fcller-Olm, M., Ohrem, C.: Deciding asynchronous hyperproperties for recursive programs. CoRR, vol. abs\/2201.12859 (2022)"},{"key":"17_CR35","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"308","DOI":"10.1007\/978-3-031-30823-9_16","volume-title":"TACAS 2023","author":"A Bajwa","year":"2023","unstructured":"Bajwa, A., Zhang, M., Chadha, R., Viswanathan, M.: Stack-aware hyperproperties. In: Sankaranarayanan, S., Sharygina, N. (eds.) TACAS 2023. LNCS, vol. 13993, pp. 308\u2013325. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-30823-9_16"},{"key":"17_CR36","unstructured":"Rabe, M.N.: A temporal logic approach to information-flow control. Ph.D. dissertation, Saarland University (2016)"},{"key":"17_CR37","volume-title":"Two approaches to interprocedural data flow analysis","author":"M Sharir","year":"1978","unstructured":"Sharir, M., Pnueli, A.: Two approaches to interprocedural data flow analysis. New York Univ. Comput. Sci. Dept, New York, NY (1978)"},{"issue":"2","key":"17_CR38","first-page":"234","volume":"164","author":"I Walukiewicz","year":"2001","unstructured":"Walukiewicz, I.: Pushdown processes: games and model-checking. IC 164(2), 234\u2013263 (2001)","journal-title":"IC"},{"key":"17_CR39","unstructured":"Hol\u00edk, L., Meyer, R., Muskalla, S.: Summaries for context-free games. In: FSTTCS, ser. LIPIcs, vol.\u00a065. Dagstuhl, pp. 41:1\u201341:16 (2016)"},{"key":"17_CR40","unstructured":"Hague, M., Meyer, R., Muskalla, S., Zimmermann, M.: Parity to safety in polynomial time for pushdown and collapsible pushdown systems. In: MFCS, ser. LIPIcs, vol. 117, pp. 57:1\u201357:15. Dagstuhl (2018)"},{"key":"17_CR41","doi-asserted-by":"crossref","unstructured":"Cleaveland, R., L\u00fcttgen, G., Natarajan, V.: Priority in process algebra. In: Handbook of Process Algebra, pp. 711\u2013765. Elsevier (2001)","DOI":"10.1016\/B978-044482830-9\/50030-8"},{"key":"17_CR42","doi-asserted-by":"crossref","unstructured":"Chandra, A.K., Stockmeyer, L.J.: Alternation. In: FOCS, pp. 98\u2013108. IEEE (1976)","DOI":"10.1109\/SFCS.1976.4"},{"issue":"1","key":"17_CR43","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1145\/321312.321326","volume":"13","author":"A Salomaa","year":"1966","unstructured":"Salomaa, A.: Two complete axiom systems for the algebra of regular events. JACM 13(1), 158\u2013169 (1966)","journal-title":"JACM"},{"issue":"3","key":"17_CR44","first-page":"439","volume":"28","author":"R Milner","year":"1984","unstructured":"Milner, R.: A complete inference system for a class of regular behaviours. JCSS 28(3), 439\u2013466 (1984)","journal-title":"JCSS"},{"key":"17_CR45","unstructured":"Pitts, A., Stark, I.: Operational reasoning for functions with local state. In: Higher Order Operational Techniques in Semantics, pp. 227\u2013273. CUP (1998)"},{"key":"17_CR46","unstructured":"McNaughton, R., Papert, S.A.: Counter-Free Automata. MIT Press (1971)"},{"key":"17_CR47","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/978-3-319-94111-0_8","volume-title":"Model Checking Software","author":"A Pommellet","year":"2018","unstructured":"Pommellet, A., Touili, T.: Model-checking HyperLTL for pushdown systems. In: Gallardo, M.M., Merino, P. (eds.) SPIN 2018. LNCS, vol. 10869, pp. 133\u2013152. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-94111-0_8"},{"key":"17_CR48","first-page":"1","volume":"223","author":"B Aminof","year":"2013","unstructured":"Aminof, B., Legay, A., Murano, A., Serre, O., Vardi, M.Y.: Pushdown module checking with imperfect information. IC 223, 1\u201317 (2013)","journal-title":"IC"},{"key":"17_CR49","unstructured":"Salvati, S., Walukiewicz, I.: A model for behavioural properties of higher-order programs. In: CSL, ser. LIPIcs, vol.\u00a041, pp. 229\u2013243. Dagstuhl (2015)"},{"issue":"4","key":"17_CR50","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1142\/S0218196793000287","volume":"3","author":"T Wilke","year":"1993","unstructured":"Wilke, T.: An algebraic theory for regular languages of finite and infinite words. Algebra Compu. 3(4), 447\u2013489 (1993)","journal-title":"Algebra Compu."}],"container-title":["Lecture Notes in Computer Science","Principles of Verification: Cycling the Probabilistic Landscape"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-75778-5_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,17]],"date-time":"2024-11-17T13:03:27Z","timestamp":1731848607000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-75778-5_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,11,18]]},"ISBN":["9783031757778","9783031757785"],"references-count":50,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-75778-5_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024,11,18]]},"assertion":[{"value":"18 November 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}