{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,14]],"date-time":"2026-10-14T22:47:42Z","timestamp":1792018062367,"version":"4.4.0"},"publisher-location":"Cham","reference-count":39,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031308222","type":"print"},{"value":"9783031308239","type":"electronic"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,4,22]],"date-time":"2023-04-22T00:00:00Z","timestamp":1682121600000},"content-version":"vor","delay-in-days":111,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>HyperLTL is a temporal logic that can express hyperproperties, i.e., properties that relate multiple execution traces of a system. Such properties are becoming increasingly important and naturally occur, e.g., in information-flow control, robustness, mutation testing, path planning, and causality checking. Thus far, complete model checking tools for HyperLTL have been limited to alternation-free formulas, i.e., formulas that use only universal or only existential trace quantification. Properties involving quantifier alternations could only be handled in an incomplete way, i.e., the verification might fail even though the property holds. In this paper, we present , an explicit-state automata-based model checker that supports full HyperLTL and is complete for properties with arbitrary quantifier alternations. We show that language inclusion checks can be integrated into HyperLTL verification, which allows  to benefit from a range of existing inclusion-checking tools. We evaluate  on a broad set of benchmarks drawn from different areas in the literature and compare it with existing (incomplete) methods for HyperLTL verification.<\/jats:p>","DOI":"10.1007\/978-3-031-30823-9_8","type":"book-chapter","created":{"date-parts":[[2023,4,21]],"date-time":"2023-04-21T16:19:12Z","timestamp":1682093952000},"page":"145-163","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":29,"title":["AutoHyper: Explicit-State Model Checking for HyperLTL"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6234-5651","authenticated-orcid":false,"given":"Raven","family":"Beutner","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4280-8441","authenticated-orcid":false,"given":"Bernd","family":"Finkbeiner","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2023,4,22]]},"reference":[{"key":"8_CR1","doi-asserted-by":"publisher","unstructured":"Babiak, T., Blahoudek, F., Duret-Lutz, A., Klein, J., Kret\u00ednsk\u00fd, J., M\u00fcller, D., Parker, D., Strejcek, J.: The Hanoi omega-automata format. In: International Conference on Computer Aided Verification, CAV 2015. LNCS, vol.\u00a09206. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_31","DOI":"10.1007\/978-3-319-21690-4_31"},{"key":"8_CR2","unstructured":"Baier, C., Katoen, J.P.: Principles of model checking. MIT press (2008)"},{"key":"8_CR3","doi-asserted-by":"publisher","unstructured":"Barthe, G., D\u2019Argenio, P.R., Rezk, T.: Secure information flow by self-composition. Math. Struct. Comput. Sci. 21(6) (2011). https:\/\/doi.org\/10.1017\/S0960129511000193","DOI":"10.1017\/S0960129511000193"},{"key":"8_CR4","doi-asserted-by":"publisher","unstructured":"Beutner, R.: AutoHyper: Explicit-state model checking for HyperLTL (2023). https:\/\/doi.org\/10.5281\/zenodo.7309986","DOI":"10.5281\/zenodo.7309986"},{"key":"8_CR5","doi-asserted-by":"publisher","unstructured":"Beutner, R., Carral, D., Finkbeiner, B., Hofmann, J., Kr\u00f6tzsch, M.: Deciding hyperproperties combined with functional specifications. In: Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2022. ACM (2022). https:\/\/doi.org\/10.1145\/3531130.3533369","DOI":"10.1145\/3531130.3533369"},{"key":"8_CR6","doi-asserted-by":"publisher","unstructured":"Beutner, R., Finkbeiner, B.: A temporal logic for strategic hyperproperties. In: International Conference on Concurrency Theory, CONCUR 2021. LIPIcs, vol.\u00a0203. Schloss Dagstuhl (2021). https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2021.24","DOI":"10.4230\/LIPIcs.CONCUR.2021.24"},{"key":"8_CR7","doi-asserted-by":"publisher","unstructured":"Beutner, R., Finkbeiner, B.: Prophecy variables for hyperproperty verification. In: IEEE Computer Security Foundations Symposium, CSF 2022. IEEE (2022). https:\/\/doi.org\/10.1109\/CSF54842.2022.00030, https:\/\/arxiv.org\/abs\/2206.01797","DOI":"10.1109\/CSF54842.2022.00030"},{"key":"8_CR8","doi-asserted-by":"publisher","unstructured":"Beutner, R., Finkbeiner, B.: Software verification of hyperproperties beyond k-safety. In: International Conference on Computer Aided Verification, CAV 2022. LNCS, vol. 13371. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-13185-1_17","DOI":"10.1007\/978-3-031-13185-1_17"},{"key":"8_CR9","doi-asserted-by":"publisher","unstructured":"Beutner, R., Finkbeiner, B.: AutoHyper: Explicit-state model checking for HyperLTL. CoRR abs\/2301.11229 (2023). https:\/\/doi.org\/10.48550\/arXiv.2301.11229","DOI":"10.48550\/arXiv.2301.11229"},{"key":"8_CR10","doi-asserted-by":"publisher","unstructured":"Beutner, R., Finkbeiner, B.: HyperATL*: A logic for hyperproperties in multi-agent systems. CoRR abs\/2203.07283 (2023). https:\/\/doi.org\/10.48550\/arXiv.2203.07283","DOI":"10.48550\/arXiv.2203.07283"},{"key":"8_CR11","doi-asserted-by":"publisher","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic model checking without BDDs. In: International Conference on Tools and Algorithms for Construction and Analysis of Systems, TACAS 1999. LNCS, vol.\u00a01579. Springer (1999). https:\/\/doi.org\/10.1007\/3-540-49059-0_14","DOI":"10.1007\/3-540-49059-0_14"},{"key":"8_CR12","doi-asserted-by":"publisher","unstructured":"Brayton, R.K., Mishchenko, A.: ABC: an academic industrial-strength verification tool. In: International Conference on Computer Aided Verification, CAV 2010. LNCS, vol.\u00a06174. Springer (2010). https:\/\/doi.org\/10.1007\/978-3-642-14295-6_5","DOI":"10.1007\/978-3-642-14295-6_5"},{"key":"8_CR13","doi-asserted-by":"publisher","unstructured":"Cimatti, A., Clarke, E.M., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: An opensource tool for symbolic model checking. In: International Conference on Computer Aided Verification, CAV 2002,Copenhagen. LNCS, vol.\u00a02404. Springer (2002). https:\/\/doi.org\/10.1007\/3-540-45657-0_29","DOI":"10.1007\/3-540-45657-0_29"},{"key":"8_CR14","doi-asserted-by":"publisher","unstructured":"Clarke, E.M., Kroening, D., Ouaknine, J., Strichman, O.: Completeness and complexity of bounded model checking. In: International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2004. LNCS, vol.\u00a02937. Springer (2004). https:\/\/doi.org\/10.1007\/978-3-540-24622-0_9","DOI":"10.1007\/978-3-540-24622-0_9"},{"key":"8_CR15","doi-asserted-by":"publisher","unstructured":"Clarkson, M.R., Finkbeiner, B., Koleini, M., Micinski, K.K., Rabe, M.N., S\u00e1nchez, C.: Temporal logics for hyperproperties. In: International Conference on Principles of Security and Trust, POST 2014. LNCS, vol.\u00a08414. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-642-54792-8_15","DOI":"10.1007\/978-3-642-54792-8_15"},{"key":"8_CR16","doi-asserted-by":"publisher","unstructured":"Clarkson, M.R., Schneider, F.B.: Hyperproperties. In: IEEE Computer Security Foundations Symposium, CSF 2008. IEEE (2008). https:\/\/doi.org\/10.1109\/CSF.2008.7","DOI":"10.1109\/CSF.2008.7"},{"key":"8_CR17","doi-asserted-by":"publisher","unstructured":"Clemente, L., Mayr, R.: Efficient reduction of nondeterministic automata with application to language inclusion testing. Log. Methods Comput. Sci. 15(1) (2019). https:\/\/doi.org\/10.23638\/LMCS-15(1:12)2019","DOI":"10.23638\/LMCS-15(1:12)2019"},{"key":"8_CR18","doi-asserted-by":"publisher","unstructured":"Coenen, N., Finkbeiner, B., Frenkel, H., Hahn, C., Metzger, N., Siber, J.: Temporal causality in reactive systems. In: International Symposium on Automated Technology for Verification and Analysis, ATVA 2022. LNCS, vol. 13505. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-19992-9_13","DOI":"10.1007\/978-3-031-19992-9_13"},{"key":"8_CR19","doi-asserted-by":"publisher","unstructured":"Coenen, N., Finkbeiner, B., S\u00e1nchez, C., Tentrup, L.: Verifying hyperliveness. In: International Conference on Computer Aided Verification, CAV 2019. LNCS, vol. 11561. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_7","DOI":"10.1007\/978-3-030-25540-4_7"},{"key":"8_CR20","doi-asserted-by":"publisher","unstructured":"Copty, F., Fix, L., Fraer, R., Giunchiglia, E., Kamhi, G., Tacchella, A., Vardi, M.Y.: Benefits of bounded model checking at an industrial setting. In: International Conference on Computer Aided Verification, CAV 2001. LNCS, vol.\u00a02102. Springer (2001). https:\/\/doi.org\/10.1007\/3-540-44585-4_43","DOI":"10.1007\/3-540-44585-4_43"},{"key":"8_CR21","doi-asserted-by":"publisher","unstructured":"Courcoubetis, C., Vardi, M.Y., Wolper, P., Yannakakis, M.: Memory-efficient algorithms for the verification of temporal properties. Formal Methods Syst. Des. 1(2\/3) (1992). https:\/\/doi.org\/10.1007\/BF00121128","DOI":"10.1007\/BF00121128"},{"key":"8_CR22","doi-asserted-by":"publisher","unstructured":"D\u2019Argenio, P.R., Barthe, G., Biewer, S., Finkbeiner, B., Hermanns, H.: Is your software on dope? - formal analysis of surreptitiously \"enhanced\" programs. In: European Symposium on Programming, ESOP 2017. LNCS, vol. 10201. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-662-54434-1_4","DOI":"10.1007\/978-3-662-54434-1_4"},{"key":"8_CR23","doi-asserted-by":"publisher","unstructured":"Doherty, S., Detlefs, D., Groves, L., Flood, C.H., Luchangco, V., Martin, P.A., Moir, M., Shavit, N., Jr., G.L.S.: DCAS is not a silver bullet for nonblocking algorithm design. In: Annual ACM Symposium on Parallelism in Algorithms and Architectures, SPAA 2004. ACM (2004). https:\/\/doi.org\/10.1145\/1007912.1007945","DOI":"10.1145\/1007912.1007945"},{"key":"8_CR24","doi-asserted-by":"publisher","unstructured":"Doveri, K., Ganty, P., Mazzocchi, N.: FORQ-based language inclusion formal testing. In: International Conference on Computer Aided Verification, CAV 2022. LNCS, vol. 13372. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-13188-2_6","DOI":"10.1007\/978-3-031-13188-2_6"},{"key":"8_CR25","doi-asserted-by":"publisher","unstructured":"Doveri, K., Ganty, P., Parolini, F., Ranzato, F.: Inclusion testing of B\u00fcchi automata based on well-quasiorders. In: International Conference on Concurrency Theory, CONCUR 2021. LIPIcs, vol.\u00a0203. Schloss Dagstuhl (2021). https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2021.3","DOI":"10.4230\/LIPIcs.CONCUR.2021.3"},{"key":"8_CR26","doi-asserted-by":"publisher","unstructured":"Duret-Lutz, A., Renault, E., Colange, M., Renkin, F., Aisse, A.G., Schlehuber-Caissier, P., Medioni, T., Martin, A., Dubois, J., Gillard, C., Lauko, H.: From Spot 2.0 to Spot 2.10: What\u2019s new? In: International Conference on Computer Aided Verification, CAV 2022. LNCS, vol. 13372. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-13188-2_9","DOI":"10.1007\/978-3-031-13188-2_9"},{"key":"8_CR27","doi-asserted-by":"publisher","unstructured":"Fellner, A., Befrouei, M.T., Weissenbacher, G.: Mutation testing with hyperproperties. Softw. Syst. Model. 20(2) (2021). https:\/\/doi.org\/10.1007\/s10270-020-00850-1","DOI":"10.1007\/s10270-020-00850-1"},{"key":"8_CR28","doi-asserted-by":"crossref","unstructured":"Fienberg, S.E.: A brief history of statistical models for network analysis and open challenges. Journal of Computational and Graphical Statistics 21(4) (2012)","DOI":"10.1080\/10618600.2012.738106"},{"key":"8_CR29","doi-asserted-by":"publisher","unstructured":"Finkbeiner, B., Rabe, M.N., S\u00e1nchez, C.: Algorithms for model checking HyperLTL and HyperCTL*. In: International Conference on Computer Aided Verification, CAV 2015. LNCS, vol.\u00a09206. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_3","DOI":"10.1007\/978-3-319-21690-4_3"},{"key":"8_CR30","doi-asserted-by":"publisher","unstructured":"Herlihy, M., Wing, J.M.: Linearizability: A correctness condition for concurrent objects. ACM Trans. Program. Lang. Syst. 12(3) (1990). https:\/\/doi.org\/10.1145\/78969.78972","DOI":"10.1145\/78969.78972"},{"key":"8_CR31","doi-asserted-by":"publisher","unstructured":"Hsu, T., S\u00e1nchez, C., Bonakdarpour, B.: Bounded model checking for hyperproperties. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2021. LNCS, vol. 12651. Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-72016-2_6","DOI":"10.1007\/978-3-030-72016-2_6"},{"key":"8_CR32","doi-asserted-by":"publisher","unstructured":"Jamroga, W., Mauw, S., Melissen, M.: Fairness in non-repudiation protocols. In: International Workshop on Security and Trust Management, STM 2011. LNCS, vol.\u00a07170. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-29963-6_10","DOI":"10.1007\/978-3-642-29963-6_10"},{"key":"8_CR33","doi-asserted-by":"publisher","unstructured":"Lamport, L.: A new solution of dijkstra\u2019s concurrent programming problem. Commun. ACM 17(8) (1974). https:\/\/doi.org\/10.1145\/361082.361093","DOI":"10.1145\/361082.361093"},{"key":"8_CR34","doi-asserted-by":"publisher","unstructured":"McCullough, D.: Noninterference and the composability of security properties. In: IEEE Symposium on Security and Privacy, SP 1988. IEEE (1988). https:\/\/doi.org\/10.1109\/SECPRI.1988.8110","DOI":"10.1109\/SECPRI.1988.8110"},{"key":"8_CR35","doi-asserted-by":"crossref","unstructured":"Piterman, N.: From nondeterministic B\u00fcchi and Streett automata to deterministic parity automata. Log. Methods Comput. Sci. 3(3) (2007). 10.2168\/LMCS-3(3:5)2007","DOI":"10.2168\/LMCS-3(3:5)2007"},{"key":"8_CR36","unstructured":"Rabe, M.N.: A temporal logic approach to Information-flow control. Ph.D. thesis, Saarland University (2016)"},{"key":"8_CR37","doi-asserted-by":"publisher","unstructured":"Smith, G., Volpano, D.M.: Secure information flow in a multi-threaded imperative language. In: ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 1998. ACM (1998). https:\/\/doi.org\/10.1145\/268946.268975","DOI":"10.1145\/268946.268975"},{"key":"8_CR38","doi-asserted-by":"publisher","unstructured":"Tsai, M., Tsay, Y., Hwang, Y.: GOAL for games, omega-automata, and logics. In: International Conference on Computer Aided Verification, CAV 2013. LNCS, vol.\u00a08044. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_62","DOI":"10.1007\/978-3-642-39799-8_62"},{"key":"8_CR39","doi-asserted-by":"publisher","unstructured":"Wang, Y., Nalluri, S., Pajic, M.: Hyperproperties for robotics: Planning via HyperLTL. In: IEEE International Conference on Robotics and Automation, ICRA 2020. IEEE (2020). https:\/\/doi.org\/10.1109\/ICRA40945.2020.9196874","DOI":"10.1109\/ICRA40945.2020.9196874"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-30823-9_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T17:06:05Z","timestamp":1781024765000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-30823-9_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031308222","9783031308239"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-30823-9_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"22 April 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Paris","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 April 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 April 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2023\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}