Document Open Access Logo

A Logic for Fresh Labelled Transition Systems

Authors Mohamed H. Bandukara , Nikos Tzevelekos

PDF

File

Thumbnail PDF
PDF
LIPIcs.CSL.2026.23.pdf
  • Filesize: 1.03 MB
  • 24 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Automata over infinite objects
  • Theory of computation → Modal and temporal logics
Keywords
  • Nominal Transition Systems
  • Hennessy-Milner Logic
  • Modal Mu-Calculus
  • Register Automata
  • Nominal Sets
  • Parity Games

Metrics

Abstract

We introduce a Hennessy-Milner logic with recursion for Fresh Labelled Transition Systems (FLTSs). These are nominal labelled transition systems which keep track of the history, i.e. of data values seen so far, and can model fresh data generation. In particular, FLTSs generalise the computations of Fresh-Register Automata, which in turn can be seen as a "regular" class of history-tracking automata operating on infinite input alphabets. The logic we introduce is a modal mu-calculus equipped with infinite disjunctions over arbitrary and fresh data values respectively, while its recursion is parameterised on vectors of data values. It can express a variety of properties, such as the existence of an infinite path of distinct data values, the absence of paths where values are repeated, or the existence of a finite path where some taint property is violated. We study the model-checking problem and its complexity via a reduction to parity games and, using nominal sets techniques, provide an exponential upper bound for it.

Cite As Get BibTex

Mohamed H. Bandukara and Nikos Tzevelekos. A Logic for Fresh Labelled Transition Systems. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 23:1-23:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.CSL.2026.23

Author Details

Mohamed H. Bandukara
  • Queen Mary University of London, UK
Nikos Tzevelekos
  • Queen Mary University of London, UK

Funding

  • Bandukara, Mohamed H.: supported by EPSRC DTP EP/R513106/1.

References

  1. Fides Aarts, Paul Fiterau-Brostean, Harco Kuppens, and Frits Vaandrager. Learning register automata with fresh value generation. In ICTAC Proceedings, pages 165-183, 2015. URL: https://doi.org/10.1007/978-3-319-25150-9_11.
  2. M. H. Bandukara and Nikos Tzevelekos. On-the-fly bisimilarity checking for fresh-register automata. In Wei Dong and Jean-Pierre Talpin, editors, Dependable Software Engineering. Theories, Tools, and Applications - 8th International Symposium, SETTA 2022, Beijing, China, October 27-29, 2022, Proceedings, volume 13649 of Lecture Notes in Computer Science, pages 187-204. Springer, 2022. URL: https://doi.org/10.1007/978-3-031-21213-0_12.
  3. M. H. Bandukara and Nikos Tzevelekos. On-the-fly bisimulation equivalence checking for fresh-register automata. J. Syst. Archit., 145:103010, 2023. URL: https://doi.org/10.1016/J.SYSARC.2023.103010.
  4. Martin Berger, Kohei Honda, and Nobuko Yoshida. Completeness and logical full abstraction in modal logics for typed mobile processes. In Luca Aceto, Ivan Damgård, Leslie Ann Goldberg, Magnús M. Halldórsson, Anna Ingólfsdóttir, and Igor Walukiewicz, editors, Automata, Languages and Programming, 35th International Colloquium, ICALP 2008, Reykjavik, Iceland, July 7-11, 2008, Proceedings, Part II - Track B: Logic, Semantics, and Theory of Programming & Track C: Security and Cryptography Foundations, volume 5126 of Lecture Notes in Computer Science, pages 99-111. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-70583-3_9.
  5. Mikolaj Bojanczyk, Bartek Klin, and Slawomir Lasota. Automata theory in nominal sets. Log. Methods Comput. Sci., 10(3), 2014. URL: https://doi.org/10.2168/LMCS-10(3:4)2014.
  6. Benedikt Bollig, Peter Habermehl, Martin Leucker, and Benjamin Monmege. A Robust Class of Data Languages and an Application to Learning. LMCS, 10(4), 2014. URL: https://doi.org/10.2168/LMCS-10(4:19)2014.
  7. Julian C. Bradfield and Perdita Stevens. Observational μ-calculus. Technical Report RS-99-5, BRICS (Basic Research in Computer Science), University of Aarhus, Denmark, 1999. URL: https://tidsskrift.dk/brics/article/view/21701.
  8. Julian C. Bradfield and Colin Stirling. Modal mu-calculi. In Patrick Blackburn, J. F. A. K. van Benthem, and Frank Wolter, editors, Handbook of Modal Logic, volume 3 of Studies in logic and practical reasoning, pages 721-756. North-Holland, 2007. URL: https://doi.org/10.1016/S1570-2464(07)80015-2.
  9. Julian C. Bradfield and Igor Walukiewicz. The mu-calculus and model checking. In Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem, editors, Handbook of Model Checking, pages 871-919. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-10575-8_26.
  10. Cristian S. Calude, Sanjay Jain, Bakhadyr Khoussainov, Wei Li, and Frank Stephan. Deciding parity games in quasi-polynomial time. SIAM J. Comput., 51(2):17-152, 2022. URL: https://doi.org/10.1137/17M1145288.
  11. Mads Dam. Model checking mobile processes. Inf. Comput., 129(1):35-51, 1996. URL: https://doi.org/10.1006/INCO.1996.0072.
  12. Mads Dam. Proof systems for π-calculus logics. In Ruy J. G. B. de Queiroz, editor, Logic for Concurrency and Synchronisation, volume 18 of Trends in Logic, pages 145-212. Kluwer, 2003. URL: https://doi.org/10.1007/0-306-48088-3_4.
  13. N.G de Bruijn. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the church-rosser theorem. Indagationes Mathematicae (Proceedings), 75(5):381-392, 1972. URL: https://doi.org/10.1016/1385-7258(72)90034-0.
  14. Stéphane Demri and Ranko Lazic. LTL with the freeze quantifier and register automata. ACM Trans. Comput. Log., 10(3):16:1-16:30, 2009. URL: https://doi.org/10.1145/1507244.1507246.
  15. Clovis Eberhart and Bartek Klin. History-dependent nominal μ-calculus. In 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019, Vancouver, BC, Canada, June 24-27, 2019, pages 1-13. IEEE, 2019. URL: https://doi.org/10.1109/LICS.2019.8785736.
  16. E. Allen Emerson and Charanjit S. Jutla. Tree automata, mu-calculus and determinacy (extended abstract). In 32nd Annual Symposium on Foundations of Computer Science, San Juan, Puerto Rico, 1-4 October 1991, pages 368-377. IEEE Computer Society, 1991. URL: https://doi.org/10.1109/SFCS.1991.185392.
  17. E. Allen Emerson, Charanjit S. Jutla, and A. Prasad Sistla. On model checking for the μ-calculus and its fragments. Theor. Comput. Sci., 258(1-2):491-522, 2001. URL: https://doi.org/10.1016/S0304-3975(00)00034-7.
  18. Diego Figueira and Luc Segoufin. Future-looking logics on data words and trees. In Rastislav Královic and Damian Niwinski, editors, Mathematical Foundations of Computer Science 2009, 34th International Symposium, MFCS 2009, Novy Smokovec, High Tatras, Slovakia, August 24-28, 2009. Proceedings, volume 5734 of Lecture Notes in Computer Science, pages 331-343. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-03816-7_29.
  19. Murdoch Gabbay and Andrew M. Pitts. A new approach to abstract syntax with variable binding. Formal Aspects Comput., 13(3-5):341-363, 2002. URL: https://doi.org/10.1007/S001650200016.
  20. Radu Grigore, Dino Distefano, Rasmus Lerchedahl Petersen, and Nikos Tzevelekos. Runtime verification based on register automata. In TACAS Proceedings, pages 260-276, 2013. URL: https://doi.org/10.1007/978-3-642-36742-7_19.
  21. Orna Grumberg, Orna Kupferman, and Sarai Sheinvald. Variable automata over infinite alphabets. In LATA Proceedings, pages 561-572, 2010. URL: https://doi.org/10.1007/978-3-642-13089-2_47.
  22. Matthew Hennessy and Robin Milner. On observing nondeterminism and concurrency. In J. W. de Bakker and Jan van Leeuwen, editors, Automata, Languages and Programming, 7th Colloquium, Noordweijkerhout, The Netherlands, July 14-18, 1980, Proceedings, volume 85 of Lecture Notes in Computer Science, pages 299-309. Springer, 1980. URL: https://doi.org/10.1007/3-540-10003-2_79.
  23. Matthew Hennessy and Robin Milner. Algebraic laws for nondeterminism and concurrency. J. ACM, 32(1):137-161, January 1985. URL: https://doi.org/10.1145/2455.2460.
  24. Michael Kaminski and Nissim Francez. Finite-memory automata. Theoretical Computer Science, 134(2):329-363, 1994. URL: https://doi.org/10.1016/0304-3975(94)90242-9.
  25. Victor Khomenko and Roland Meyer. Checking pi-calculus structural congruence is graph isomorphism complete. In Ninth International Conference on Application of Concurrency to System Design, ACSD 2009, Augsburg, Germany, 1-3 July 2009, pages 70-79. IEEE Computer Society, 2009. URL: https://doi.org/10.1109/ACSD.2009.8.
  26. Bartek Klin and Mateusz Lelyk. Modal mu-calculus with atoms. In Valentin Goranko and Mads Dam, editors, 26th EACSL Annual Conference on Computer Science Logic, CSL 2017, August 20-24, 2017, Stockholm, Sweden, volume 82 of LIPIcs, pages 30:1-30:21. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. URL: https://doi.org/10.4230/LIPIcs.CSL.2017.30.
  27. Bartek Klin and Mateusz Lelyk. Scalar and vectorial mu-calculus with atoms. Log. Methods Comput. Sci., 15(4), 2019. URL: https://doi.org/10.23638/LMCS-15(4:5)2019.
  28. Vasileios Koutavas and Matthew Hennessy. First-order reasoning for higher-order concurrency. Comput. Lang. Syst. Struct., 38(3):242-277, 2012. URL: https://doi.org/10.1016/J.CL.2012.04.003.
  29. Dexter Kozen. Results on the propositional μ-calculus. Theoretical Computer Science, 27(3):333-354, 1983. Special Issue Ninth International Colloquium on Automata, Languages and Programming (ICALP) Aarhus, Summer 1982. URL: https://doi.org/10.1016/0304-3975(82)90125-6.
  30. Robin Milner, Joachim Parrow, and David Walker. A calculus of mobile processes, I and II. Inf. Comput., 100(1), 1992. URL: https://doi.org/10.1016/0890-5401(92)90008-4.
  31. Robin Milner, Joachim Parrow, and David Walker. Modal logics for mobile processes. Theor. Comput. Sci., 114(1):149-171, 1993. URL: https://doi.org/10.1016/0304-3975(93)90156-N.
  32. Andrzej Murawski, Steven Ramsay, and Nikos Tzevelekos. A contextual equivalence checker for IMJ*. In ATVA proceedings, pages 234-240, 2015. URL: https://doi.org/10.1007/978-3-319-24953-7_19.
  33. Andrzej S. Murawski, Steven J. Ramsay, and Nikos Tzevelekos. Bisimilarity in fresh-register automata. In LICS Proceedings, pages 156-167, 2015. URL: https://doi.org/10.1109/LICS.2015.24.
  34. Andrzej S. Murawski, Steven J. Ramsay, and Nikos Tzevelekos. Polynomial-time equivalence testing for deterministic fresh-register automata. In MFCS Proceedings, 2018. URL: https://doi.org/10.4230/LIPIcs.MFCS.2018.72.
  35. Andrzej S. Murawski and Nikos Tzevelekos. Algorithmic nominal game semantics. In ESOP Proceedings, pages 419-438, 2011. URL: https://doi.org/10.1007/978-3-642-19718-5_22.
  36. Rocco De Nicola and Michele Loreti. Multiple-labelled transition systems for nominal calculi and their logics. Math. Struct. Comput. Sci., 18(1):107-143, 2008. URL: https://doi.org/10.1017/S0960129507006585.
  37. Joachim Parrow, Johannes Borgström, Lars-Henrik Eriksson, Ramunas Gutkovas, and Tjark Weber. Modal logics for nominal transition systems. Log. Methods Comput. Sci., 17(1), 2021. URL: https://lmcs.episciences.org/7137.
  38. Marco Pistore. History-Dependent Automata. PhD thesis, Università di Pisa, 1999. Google Scholar
  39. Andrew M. Pitts. Nominal logic, a first order theory of names and binding. Inf. Comput., 186(2):165-193, 2003. URL: https://doi.org/10.1016/S0890-5401(03)00138-X.
  40. Davide Sangiorgi and David Walker. The Pi-Calculus - a theory of mobile processes. Cambridge University Press, 2001. URL: https://doi.org/10.1017/9781316134924.
  41. Thomas Schwentick. Automata for XML—a survey. JCSS, 73(3):289-315, 2007. URL: https://doi.org/10.1016/j.jcss.2006.10.003.
  42. Luc Segoufin. Automata and logics for words and trees over an infinite alphabet. In Zoltán Ésik, editor, Computer Science Logic, 20th International Workshop, CSL 2006, 15th Annual Conference of the EACSL, Szeged, Hungary, September 25-29, 2006, Proceedings, volume 4207 of Lecture Notes in Computer Science, pages 41-57. Springer, 2006. URL: https://doi.org/10.1007/11874683_3.
  43. Alfred Tarski. A lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics, 5(2):285-309, 1955. URL: https://doi.org/10.2140/pjm.1955.5.285.
  44. Nikos Tzevelekos. Fresh-register automata. In POPL Proceedings. ACM, 2011. URL: https://doi.org/10.1145/1926385.1926420.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact