{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,22]],"date-time":"2025-09-22T18:40:15Z","timestamp":1758566415100,"version":"3.44.0"},"reference-count":33,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2025,8,18]],"date-time":"2025-08-18T00:00:00Z","timestamp":1755475200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,8,18]],"date-time":"2025-08-18T00:00:00Z","timestamp":1755475200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100002702","name":"Aalborg University","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100002702","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Acta Informatica"],"published-print":{"date-parts":[[2025,9]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>HyperLTL model-checking enables the automated verification of information-flow properties for security-critical systems. However, it only provides a binary answer. Here, we consider the problem of computing counterexamples and explanations for HyperLTL model-checking, thereby considerably increasing its usefulness. Based on the maxim \u201ccounterexamples\/explanations are Skolem functions for the existentially quantified trace variables\u201d, we consider (Turing machine) computable Skolem functions. As not every finite transition system and formula have computable Skolem functions witnessing that the system satisfies the formula, we consider the problem of deciding whether such functions exist. Our main result shows that this problem is decidable by reducing it to solving multiplayer games with hierarchical imperfect information. Furthermore, our algorithm also computes transducers implementing such functions, if they exist.<\/jats:p>","DOI":"10.1007\/s00236-025-00499-7","type":"journal-article","created":{"date-parts":[[2025,8,18]],"date-time":"2025-08-18T05:43:06Z","timestamp":1755495786000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Tracy, traces, and transducers: computable counterexamples and explanations for HyperLTL model-checking"],"prefix":"10.1007","volume":"62","author":[{"given":"Sarah","family":"Winter","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Martin","family":"Zimmermann","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,8,18]]},"reference":[{"key":"499_CR1","doi-asserted-by":"publisher","unstructured":"\u00c1brah\u00e1m, E., Becker, B., Dehnert, C., Jansen, N., Katoen, J., Wimmer, R.: Counterexample generation for discrete-time Markov models: An introductory survey. In: Bernardo, M., Damiani, F., H\u00e4hnle, R., Johnsen, E.B., Schaefer, I. (eds.) SFM 2014. LNCS, vol. 8483, pp. 65\u2013121. Springer, (2014). https:\/\/doi.org\/10.1007\/978-3-319-07317-0_3","DOI":"10.1007\/978-3-319-07317-0_3"},{"key":"499_CR2","doi-asserted-by":"publisher","unstructured":"Arkhangel\u2019ski\u012d, A.V., Fedorchuk, V.V.: The basic concepts and constructions of general topology. In: Arkhangel\u2019ski\u012d, L.S. A.\u00a0V.and\u00a0Pontryagin (ed.) General Topology I: Basic Concepts and Constructions Dimension Theory, pp. 1\u201390. Springer, (1990). https:\/\/doi.org\/10.1007\/978-3-642-61265-7_1","DOI":"10.1007\/978-3-642-61265-7_1"},{"key":"499_CR3","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1016\/j.inffus.2019.12.012","volume":"58","author":"AB Arrieta","year":"2020","unstructured":"Arrieta, A.B., Rodr\u00edguez, N.D., Ser, J.D., Bennetot, A., Tabik, S., Barbado, A., Garc\u00eda, S., Gil-Lopez, S., Molina, D., Benjamins, R., Chatila, R., Herrera, F.: Explainable artificial intelligence (XAI): concepts, taxonomies, opportunities and challenges toward responsible AI. Inf. Fusion 58, 82\u2013115 (2020). https:\/\/doi.org\/10.1016\/j.inffus.2019.12.012","journal-title":"Inf. Fusion"},{"key":"499_CR4","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.: Principles of Model Checking. MIT Press (2008)"},{"issue":"8","key":"499_CR5","doi-asserted-by":"publisher","first-page":"669","DOI":"10.1007\/S00236-017-0306-5","volume":"55","author":"D Berwanger","year":"2018","unstructured":"Berwanger, D., Mathew, A.B., Bogaard, M.: Hierarchical information and the synthesis of distributed strategies. Acta Informatica 55(8), 669\u2013701 (2018). https:\/\/doi.org\/10.1007\/S00236-017-0306-5","journal-title":"Acta Informatica"},{"key":"499_CR6","doi-asserted-by":"publisher","unstructured":"Beutner, R., Finkbeiner, B.: Non-deterministic planning for hyperproperty verification. In: Bernardini, S., Muise, C. (eds.) ICAPS 2024, pp. 25\u201330. AAAI Press, (2024). https:\/\/doi.org\/10.1609\/ICAPS.V34I1.31457","DOI":"10.1609\/ICAPS.V34I1.31457"},{"key":"499_CR7","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1016\/S0065-2458(03)58003-2","volume":"58","author":"A Biere","year":"2003","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Strichman, O., Zhu, Y.: Bounded model checking. Adv. Comput. 58, 117\u2013148 (2003). https:\/\/doi.org\/10.1016\/S0065-2458(03)58003-2","journal-title":"Adv. Comput."},{"key":"499_CR8","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: Abadi, M., Kremer, S. (eds.) POST 2014. LNCS, vol. 8414, pp. 265\u2013284. Springer, (2014). https:\/\/doi.org\/10.1007\/978-3-642-54792-8_15","DOI":"10.1007\/978-3-642-54792-8_15"},{"issue":"5","key":"499_CR9","doi-asserted-by":"publisher","first-page":"752","DOI":"10.1145\/876638.876643","volume":"50","author":"EM Clarke","year":"2003","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. J. ACM 50(5), 752\u2013794 (2003). https:\/\/doi.org\/10.1145\/876638.876643","journal-title":"J. ACM"},{"key":"499_CR10","doi-asserted-by":"publisher","unstructured":"Clarke, E.M., Jha, S., Lu, Y., Veith, H.: Tree-like counterexamples in model checking. In: LICS 2002, pp. 19\u201329. IEEE Computer Society, (2002). https:\/\/doi.org\/10.1109\/LICS.2002.1029814","DOI":"10.1109\/LICS.2002.1029814"},{"issue":"6","key":"499_CR11","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). https:\/\/doi.org\/10.3233\/JCS-2009-0393","journal-title":"J. Comput. Secur."},{"key":"499_CR12","doi-asserted-by":"publisher","unstructured":"Coenen, N., Dachselt, R., Finkbeiner, B., Frenkel, H., Hahn, C., Horak, T., Metzger, N., Siber, J.: Explaining hyperproperty violations. In: Shoham, S., Vizel, Y. (eds.) CAV 2022, Part I. LNCS, vol. 13371, pp. 407\u2013429. Springer, (2022). https:\/\/doi.org\/10.1007\/978-3-031-13185-1_20","DOI":"10.1007\/978-3-031-13185-1_20"},{"key":"499_CR13","doi-asserted-by":"publisher","unstructured":"Damman, B., Han, T., Katoen, J.: Regular expressions for PCTL counterexamples. In: QEST 2008, pp. 179\u2013188. IEEE Computer Society, (2008). https:\/\/doi.org\/10.1109\/QEST.2008.11","DOI":"10.1109\/QEST.2008.11"},{"key":"499_CR14","doi-asserted-by":"publisher","unstructured":"Finkbeiner, B., Rabe, M.N., S\u00e1nchez, C.: Algorithms for Model Checking HyperLTL and HyperCTL$$^*$$. In: Kroening, D., Pasareanu, C.S. (eds.) CAV 2015, Part I. LNCS, vol. 9206, pp. 30\u201348. Springer, (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_3","DOI":"10.1007\/978-3-319-21690-4_3"},{"issue":"1 &2","key":"499_CR15","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1142\/S012905412348009X","volume":"35","author":"E Filiot","year":"2024","unstructured":"Filiot, E., Winter, S.: Synthesizing computable functions from rational specifications over infinite words. Int. J. Found. Comput. Sci. 35(1 &2), 179\u2013214 (2024). https:\/\/doi.org\/10.1142\/S012905412348009X","journal-title":"Int. J. Found. Comput. Sci."},{"issue":"5\u20136","key":"499_CR16","doi-asserted-by":"publisher","first-page":"519","DOI":"10.1007\/S10009-012-0228-Z","volume":"15","author":"B Finkbeiner","year":"2013","unstructured":"Finkbeiner, B., Schewe, S.: Bounded synthesis. Int. J. Softw. Tools Technol. Transf. 15(5\u20136), 519\u2013539 (2013). https:\/\/doi.org\/10.1007\/S10009-012-0228-Z","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"issue":"1\u20132","key":"499_CR17","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1007\/s00236-019-00358-2","volume":"57","author":"B Finkbeiner","year":"2020","unstructured":"Finkbeiner, B., Hahn, C., Lukert, P., Stenger, M., Tentrup, L.: Synthesis from hyperproperties. Acta Informatica 57(1\u20132), 137\u2013163 (2020). https:\/\/doi.org\/10.1007\/s00236-019-00358-2","journal-title":"Acta Informatica"},{"key":"499_CR18","doi-asserted-by":"publisher","unstructured":"Gr\u00e4del, E., Thomas, W., Wilke, T. (eds.): Automata, Logics, and Infinite Games: A Guide to Current Research. LNCS, vol. 2500. Springer, (2002). https:\/\/doi.org\/10.1007\/3-540-36387-4","DOI":"10.1007\/3-540-36387-4"},{"key":"499_CR19","doi-asserted-by":"publisher","unstructured":"Gurfinkel, A., Chechik, M.: Proof-like counter-examples. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 160\u2013175. Springer, (2003). https:\/\/doi.org\/10.1007\/3-540-36577-X_12","DOI":"10.1007\/3-540-36577-X_12"},{"key":"499_CR20","doi-asserted-by":"publisher","unstructured":"Holtmann, M., Kaiser, L., Thomas, W.: Degrees of lookahead in regular infinite games. Log. Methods Comput. Sci. 8(3) (2012) https:\/\/doi.org\/10.2168\/LMCS-8(3:24)2012","DOI":"10.2168\/LMCS-8(3:24)2012"},{"issue":"1","key":"499_CR21","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1109\/TVCG.2021.3114866","volume":"28","author":"T Horak","year":"2022","unstructured":"Horak, T., Coenen, N., Metzger, N., Hahn, C., Flemisch, T., M\u00e9ndez, J., Dimov, D., Finkbeiner, B., Dachselt, R.: Visual analysis of hyperproperties for understanding model checking results. IEEE Trans. Vis. Comput. Graph. 28(1), 357\u2013367 (2022). https:\/\/doi.org\/10.1109\/TVCG.2021.3114866","journal-title":"IEEE Trans. Vis. Comput. Graph."},{"key":"499_CR22","unstructured":"Hosch, F.A., Landweber, L.H.: Finite delay solutions for sequential conditions. In: ICALP 1972, pp. 45\u201360 (1972)"},{"key":"499_CR23","doi-asserted-by":"publisher","unstructured":"Han, T., Katoen, J.: Counterexamples in probabilistic model checking. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 72\u201386. Springer, (2007). https:\/\/doi.org\/10.1007\/978-3-540-71209-1_8","DOI":"10.1007\/978-3-540-71209-1_8"},{"key":"499_CR24","doi-asserted-by":"publisher","unstructured":"Klein, F., Zimmermann, M.: How much lookahead is needed to win infinite games? Log. Methods Comput. Sci. 12(3) (2016) https:\/\/doi.org\/10.2168\/LMCS-12(3:4)2016","DOI":"10.2168\/LMCS-12(3:4)2016"},{"key":"499_CR25","doi-asserted-by":"publisher","unstructured":"Kurshan, R.P.: Verification technology transfer. In: Grumberg, O., Veith, H. (eds.) 25 Years of Model Checking - History, Achievements, Perspectives. LNCS, vol. 5000, pp. 46\u201364. Springer, (2008). https:\/\/doi.org\/10.1007\/978-3-540-69850-0_3","DOI":"10.1007\/978-3-540-69850-0_3"},{"key":"499_CR26","doi-asserted-by":"publisher","unstructured":"Klein, F., Zimmermann, M.: Prompt delay. In: Lal, A., Akshay, S., Saurabh, S., Sen, S. (eds.) FSTTCS 2016. LIPIcs, vol. 65, pp. 43\u201314314. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, (2016). https:\/\/doi.org\/10.4230\/LIPICS.FSTTCS.2016.43","DOI":"10.4230\/LIPICS.FSTTCS.2016.43"},{"key":"499_CR27","doi-asserted-by":"publisher","unstructured":"Mascle, C., Zimmermann, M.: The keys to decidable HyperLTL satisfiability: Small models or very simple formulas. In: Fern\u00e1ndez, M., Muscholl, A. (eds.) CSL 2020. LIPIcs, vol. 152, pp. 29\u201312916. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, (2020). https:\/\/doi.org\/10.4230\/LIPIcs.CSL.2020.29","DOI":"10.4230\/LIPIcs.CSL.2020.29"},{"key":"499_CR28","doi-asserted-by":"publisher","unstructured":"Pnueli, A., Rosner, R.: Distributed reactive systems are hard to synthesize. In: FOCS 1990, Volume II, pp. 746\u2013757. IEEE Computer Society, (1990). https:\/\/doi.org\/10.1109\/FSCS.1990.89597","DOI":"10.1109\/FSCS.1990.89597"},{"key":"499_CR29","doi-asserted-by":"publisher","unstructured":"Pnueli, A.: The temporal logic of programs. In: FOCS 1977, pp. 46\u201357. IEEE, (1977). https:\/\/doi.org\/10.1109\/SFCS.1977.32","DOI":"10.1109\/SFCS.1977.32"},{"key":"499_CR30","unstructured":"Rabe, M.N.: A temporal logic approach to information-flow control. PhD thesis, Saarland University (2016). http:\/\/scidok.sulb.uni-saarland.de\/volltexte\/2016\/6387\/"},{"key":"499_CR31","doi-asserted-by":"publisher","unstructured":"Richard B\u00fcchi, J.: Symposium on decision problems: On a decision method in restricted second order arithmetic. In: Nagel, E., Suppes, P., Tarski, A. (eds.) Logic, Methodology and Philosophy of Science. Studies in Logic and the Foundations of Mathematics, vol. 44, pp. 1\u201311. Elsevier, (1966). https:\/\/doi.org\/10.1016\/S0049-237X(09)70564-6","DOI":"10.1016\/S0049-237X(09)70564-6"},{"issue":"1","key":"499_CR32","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1297658.1297659","volume":"9","author":"S Shoham","year":"2007","unstructured":"Shoham, S., Grumberg, O.: A game-based framework for CTL counterexamples and 3-valued abstraction-refinement. ACM Trans. Comput. Log. 9(1), 1 (2007). https:\/\/doi.org\/10.1145\/1297658.1297659","journal-title":"ACM Trans. Comput. Log."},{"key":"499_CR33","doi-asserted-by":"publisher","unstructured":"Winter, S., Zimmermann, M.: Prophecies all the way: Game-based model-checking for hyperqptl beyond $$\\forall ^*\\exists ^*$$. arXiv:2504.08575 (2025) https:\/\/doi.org\/10.48550\/ARXIV.2504.08575","DOI":"10.48550\/ARXIV.2504.08575"}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-025-00499-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s00236-025-00499-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-025-00499-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,22]],"date-time":"2025-09-22T18:02:32Z","timestamp":1758564152000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s00236-025-00499-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,8,18]]},"references-count":33,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2025,9]]}},"alternative-id":["499"],"URL":"https:\/\/doi.org\/10.1007\/s00236-025-00499-7","relation":{},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"type":"print","value":"0001-5903"},{"type":"electronic","value":"1432-0525"}],"subject":[],"published":{"date-parts":[[2025,8,18]]},"assertion":[{"value":"26 November 2024","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"16 July 2025","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"18 August 2025","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors declare no competing interests.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Competing interests"}}],"article-number":"31"}}