Document Open Access Logo

A Complete Quantitative Axiomatisation of Behavioural Distance of Regular Expressions

Author Wojciech Różowski

PDF
Thumbnail PDF

File

LIPIcs.ICALP.2024.149.pdf
  • Filesize: 0.88 MB
  • 20 pages

Document Identifiers

Author Details

Wojciech Różowski
  • Department of Computer Science, University College London, UK

Funding

This work was partially supported by ERC grant Autoprobe (grant agreement 101002697).

Acknowledgements

The author wishes to thank Giorgio Bacci, Leo Lobski, Alexandra Silva and Mateo Torres-Ruiz for discussions and feedback, as well as anonymous reviewers for their comments.

Cite AsGet BibTex

Wojciech Różowski. A Complete Quantitative Axiomatisation of Behavioural Distance of Regular Expressions. In 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 297, pp. 149:1-149:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.ICALP.2024.149

Abstract

Deterministic automata have been traditionally studied through the point of view of language equivalence, but another perspective is given by the canonical notion of shortest-distinguishing-word distance quantifying the of states. Intuitively, the longer the word needed to observe a difference between two states, then the closer their behaviour is. In this paper, we give a sound and complete axiomatisation of shortest-distinguishing-word distance between regular languages. Our axiomatisation relies on a recently developed quantitative analogue of equational logic, allowing to manipulate rational-indexed judgements of the form e ≡_ε f meaning term e is approximately equivalent to term f within the error margin of ε. The technical core of the paper is dedicated to the completeness argument that draws techniques from order theory and Banach spaces to simplify the calculation of the behavioural distance to the point it can be then mimicked by axiomatic reasoning.

Subject Classification

ACM Subject Classification
  • Theory of computation → Regular languages
Keywords
  • Regular Expressions
  • Behavioural Distances
  • Quantitative Equational Theories

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

References

  1. Giorgio Bacci, Giovanni Bacci, Kim G. Larsen, and Radu Mardare. Complete Axiomatization for the Total Variation Distance of Markov Chains. In Sam Staton, editor, Proceedings of the Thirty-Fourth Conference on the Mathematical Foundations of Programming Semantics, MFPS 2018, Dalhousie University, Halifax, Canada, June 6-9, 2018, volume 341 of Electronic Notes in Theoretical Computer Science, pages 27-39. Elsevier, 2018. URL: https://doi.org/10.1016/J.ENTCS.2018.03.014.
  2. Giorgio Bacci, Giovanni Bacci, Kim G. Larsen, and Radu Mardare. A Complete Quantitative Deduction system for the Bisimilarity Distance on Markov Chains. Log. Methods Comput. Sci., 14(4), 2018. URL: https://doi.org/10.23638/LMCS-14(4:15)2018.
  3. Giorgio Bacci, Giovanni Bacci, Kim G. Larsen, and Radu Mardare. Converging from branching to linear metrics on Markov chains. Math. Struct. Comput. Sci., 29(1):3-37, 2019. URL: https://doi.org/10.1017/S0960129517000160.
  4. Giorgio Bacci, Radu Mardare, Prakash Panangaden, and Gordon D. Plotkin. An Algebraic Theory of Markov Processes. In Anuj Dawar and Erich Grädel, editors, Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018, pages 679-688. ACM, 2018. URL: https://doi.org/10.1145/3209108.3209177.
  5. Paolo Baldan, Filippo Bonchi, Henning Kerstan, and Barbara König. Coalgebraic Behavioral Metrics. Log. Methods Comput. Sci., 14(3), 2018. URL: https://doi.org/10.23638/LMCS-14(3:20)2018.
  6. Harsh Beohar, Sebastian Gurke, Barbara König, and Karla Messing. Hennessy-Milner Theorems via Galois Connections. In Bartek Klin and Elaine Pimentel, editors, 31st EACSL Annual Conference on Computer Science Logic, CSL 2023, February 13-16, 2023, Warsaw, Poland, volume 252 of LIPIcs, pages 12:1-12:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPICS.CSL.2023.12.
  7. Harsh Beohar, Sebastian Gurke, Barbara König, Karla Messing, Jonas Forster, Lutz Schröder, and Paul Wild. Expressive Quantale-valued Logics for Coalgebras: an Adjunction-based Approach. CoRR, abs/2310.05711, 2023. URL: https://doi.org/10.48550/arXiv.2310.05711.
  8. Richard Blute, Josée Desharnais, Abbas Edalat, and Prakash Panangaden. Bisimulation for Labelled Markov Processes. In Proceedings, 12th Annual IEEE Symposium on Logic in Computer Science, Warsaw, Poland, June 29 - July 2, 1997, pages 149-158. IEEE Computer Society, 1997. URL: https://doi.org/10.1109/LICS.1997.614943.
  9. Filippo Bonchi, Barbara König, and Daniela Petrisan. Up-To Techniques for Behavioural Metrics via Fibrations. In Sven Schewe and Lijun Zhang, editors, 29th International Conference on Concurrency Theory, CONCUR 2018, September 4-7, 2018, Beijing, China, volume 118 of LIPIcs, pages 17:1-17:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. URL: https://doi.org/10.4230/LIPICS.CONCUR.2018.17.
  10. Janusz A. Brzozowski. Derivatives of Regular Expressions. J. ACM, 11(4):481-494, 1964. URL: https://doi.org/10.1145/321239.321249.
  11. Stanley Burris and H P Sankappanavar. A Course in Universal Algebra. Lecture Notes in Statistics. Springer, New York, NY, November 1981. Google Scholar
  12. Pedro R. D'Argenio, Daniel Gebler, and Matias David Lee. Axiomatizing Bisimulation Equivalences and Metrics from Probabilistic SOS rules. In Anca Muscholl, editor, Foundations of Software Science and Computation Structures - 17th International Conference, FOSSACS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings, volume 8412 of Lecture Notes in Computer Science, pages 289-303. Springer, 2014. URL: https://doi.org/10.1007/978-3-642-54830-7_19.
  13. Josée Desharnais, Vineet Gupta, Radha Jagadeesan, and Prakash Panangaden. Metrics for labelled markov processes. Theor. Comput. Sci., 318(3):323-354, 2004. URL: https://doi.org/10.1016/J.TCS.2003.09.013.
  14. Tiago Ferreira, Gerco van Heerdt, and Alexandra Silva. Tree-Based Adaptive Model Learning. In Nils Jansen, Mariëlle Stoelinga, and Petra van den Bos, editors, A Journey from Process Algebra via Timed Automata to Model Learning - Essays Dedicated to Frits Vaandrager on the Occasion of His 60th Birthday, volume 13560 of Lecture Notes in Computer Science, pages 164-179. Springer, 2022. URL: https://doi.org/10.1007/978-3-031-15629-8_10.
  15. Jonas Forster, Lutz Schröder, and Paul Wild. Quantitative Graded Semantics and Spectra of Behavioural Metrics. CoRR, abs/2306.01487, 2023. URL: https://doi.org/10.48550/arXiv.2306.01487.
  16. Alessandro Giacalone, Chi-Chang Jou, and Scott A. Smolka. Algebraic Reasoning for Probabilistic Concurrent Systems. In Manfred Broy and Cliff B. Jones, editors, Programming concepts and methods: Proceedings of the IFIP Working Group 2.2, 2.3 Working Conference on Programming Concepts and Methods, Sea of Galilee, Israel, 2-5 April, 1990, pages 443-458. North-Holland, 1990. Google Scholar
  17. Sergey Goncharov, Dirk Hofmann, Pedro Nora, Lutz Schröder, and Paul Wild. Kantorovich Functors and Characteristic Logics for Behavioural Distances. In Orna Kupferman and Pawel Sobocinski, editors, Foundations of Software Science and Computation Structures - 26th International Conference, FoSSaCS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 22-27, 2023, Proceedings, volume 13992 of Lecture Notes in Computer Science, pages 46-67. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-30829-1_3.
  18. John E. Hopcroft and Richard M. Karp. A Linear Algorithm for Testing Equivalence of Finite Automata, 1971. URL: https://api.semanticscholar.org/CorpusID:120207847.
  19. Dexter Kozen. A Completeness Theorem for Kleene Algebras and the Algebra of Regular Events. Inf. Comput., 110(2):366-390, 1994. URL: https://doi.org/10.1006/INCO.1994.1037.
  20. Marta Z. Kwiatkowska. A Metric for Traces. Inf. Process. Lett., 35(3):129-135, 1990. URL: https://doi.org/10.1016/0020-0190(90)90061-2.
  21. Kim G. Larsen, Uli Fahrenberg, and Claus R. Thrane. Metrics for weighted transition systems: Axiomatization and complexity. Theor. Comput. Sci., 412(28):3358-3369, 2011. URL: https://doi.org/10.1016/J.TCS.2011.04.003.
  22. Radu Mardare, Prakash Panangaden, and Gordon D. Plotkin. Quantitative Algebraic Reasoning. In Martin Grohe, Eric Koskinen, and Natarajan Shankar, editors, Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, New York, NY, USA, July 5-8, 2016, pages 700-709. ACM, 2016. URL: https://doi.org/10.1145/2933575.2934518.
  23. Radu Mardare, Prakash Panangaden, and Gordon D. Plotkin. Fixed-points for Quantitative Equational Logics. In 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021, Rome, Italy, June 29 - July 2, 2021, pages 1-13. IEEE, 2021. URL: https://doi.org/10.1109/LICS52264.2021.9470662.
  24. Robin Milner. A Complete Inference System for a Class of Regular Behaviours. J. Comput. Syst. Sci., 28(3):439-466, 1984. URL: https://doi.org/10.1016/0022-0000(84)90023-0.
  25. David Michael Ritchie Park. Concurrency and Automata on Infinite Sequences. In Theoretical Computer Science, 1981. URL: https://api.semanticscholar.org/CorpusID:206841958.
  26. Walter Rudin. Functional Analysis. International Series in Pure & Applied Mathematics. McGraw Hill Higher Education, Maidenhead, England, 2 edition, October 1990. Google Scholar
  27. Jan J. M. M. Rutten. Universal coalgebra: a theory of systems. Theor. Comput. Sci., 249(1):3-80, 2000. URL: https://doi.org/10.1016/S0304-3975(00)00056-6.
  28. Wojciech Różowski. A Complete Quantitative Axiomatisation of Behavioural Distance of Regular Expressions, 2024. URL: https://arxiv.org/abs/2404.13352.
  29. Wojciech Różowski, Tobias Kappé, Dexter Kozen, Todd Schmid, and Alexandra Silva. Probabilistic Guarded KAT Modulo Bisimilarity: Completeness and Complexity. In Kousha Etessami, Uriel Feige, and Gabriele Puppis, editors, 50th International Colloquium on Automata, Languages, and Programming, ICALP 2023, July 10-14, 2023, Paderborn, Germany, volume 261 of LIPIcs, pages 136:1-136:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPICS.ICALP.2023.136.
  30. Arto Salomaa. Two Complete Axiom Systems for the Algebra of Regular Events. J. ACM, 13(1):158-169, 1966. URL: https://doi.org/10.1145/321312.321326.
  31. Davide Sangiorgi. Coinduction and the duality with induction, pages 28-88. Cambridge University Press, 2011. Google Scholar
  32. Todd Schmid, Wojciech Różowski, Alexandra Silva, and Jurriaan Rot. Processes Parametrised by an Algebraic Theory. In Mikolaj Bojanczyk, Emanuela Merelli, and David P. Woodruff, editors, 49th International Colloquium on Automata, Languages, and Programming, ICALP 2022, July 4-8, 2022, Paris, France, volume 229 of LIPIcs, pages 132:1-132:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPICS.ICALP.2022.132.
  33. A.M Silva. Kleene coalgebra. PhD thesis, Radboud Universiteit Nijmegen, 2010. Google Scholar
  34. Steffen Smolka, Nate Foster, Justin Hsu, Tobias Kappé, Dexter Kozen, and Alexandra Silva. Guarded Kleene algebra with tests: verification of uninterpreted programs in nearly linear time. Proc. ACM Program. Lang., 4(POPL):61:1-61:28, 2020. URL: https://doi.org/10.1145/3371129.
  35. Eugene W. Stark and Scott A. Smolka. A complete axiom system for finite-state probabilistic processes. In Gordon D. Plotkin, Colin Stirling, and Mads Tofte, editors, Proof, Language, and Interaction, Essays in Honour of Robin Milner, pages 571-596. The MIT Press, 2000. Google Scholar
  36. Alfred Tarski. A lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics, 5(2):285-309, 1955. Google Scholar
  37. Franck van Breugel. On behavioural pseudometrics and closure ordinals. Inf. Process. Lett., 112(19):715-718, 2012. URL: https://doi.org/10.1016/J.IPL.2012.06.019.
  38. Franck van Breugel. Probabilistic bisimilarity distances. ACM SIGLOG News, 4(4):33-51, 2017. URL: https://doi.org/10.1145/3157831.3157837.
  39. Franck van Breugel and James Worrell. Towards Quantitative Verification of Probabilistic Transition Systems. In Fernando Orejas, Paul G. Spirakis, and Jan van Leeuwen, editors, Automata, Languages and Programming, 28th International Colloquium, ICALP 2001, Crete, Greece, July 8-12, 2001, Proceedings, volume 2076 of Lecture Notes in Computer Science, pages 421-432. Springer, 2001. URL: https://doi.org/10.1007/3-540-48224-5_35.
  40. Franck van Breugel and James Worrell. Approximating and computing behavioural distances in probabilistic transition systems. Theor. Comput. Sci., 360(1-3):373-385, 2006. URL: https://doi.org/10.1016/J.TCS.2006.05.021.
  41. Rob J. van Glabbeek. The Linear Time-Branching Time Spectrum (Extended Abstract). In Jos C. M. Baeten and Jan Willem Klop, editors, CONCUR '90, Theories of Concurrency: Unification and Extension, Amsterdam, The Netherlands, August 27-30, 1990, Proceedings, volume 458 of Lecture Notes in Computer Science, pages 278-297. Springer, 1990. URL: https://doi.org/10.1007/BFB0039066.
  42. Cédric Villani. Optimal Transport. Springer Berlin Heidelberg, 2009. URL: https://doi.org/10.1007/978-3-540-71050-9.
  43. Jana Wagemaker, Marcello M. Bonsangue, Tobias Kappé, Jurriaan Rot, and Alexandra Silva. Completeness and Incompleteness of Synchronous Kleene Algebra. In Graham Hutton, editor, Mathematics of Program Construction - 13th International Conference, MPC 2019, Porto, Portugal, October 7-9, 2019, Proceedings, volume 11825 of Lecture Notes in Computer Science, pages 385-413. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-33636-3_14.
  44. Paul Wild and Lutz Schröder. Characteristic Logics for Behavioural Hemimetrics via Fuzzy Lax Extensions. Log. Methods Comput. Sci., 18(2), 2022. URL: https://doi.org/10.46298/LMCS-18(2:19)2022.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

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