skip to main content
research-article

Checking NFA equivalence with bisimulations up to congruence

Published: 23 January 2013 Publication History

Abstract

We introduce bisimulation up to congruence as a technique for proving language equivalence of non-deterministic finite automata. Exploiting this technique, we devise an optimisation of the classical algorithm by Hopcroft and Karp. We compare our approach to the recently introduced antichain algorithms, by analysing and relating the two underlying coinductive proof methods. We give concrete examples where we exponentially improve over antichains; experimental results moreover show non negligible improvements.

Supplementary Material

JPG File (r2d3_talk2.jpg)
MP4 File (r2d3_talk2.mp4)

References

[1]
P. A. Abdulla, Y.-F. Chen, L. Holík, R. Mayr, and T. Vojnar. When simulation meets antichains. TACAS, vol. 6015 of phLNCS, pages 158--174. Springer, 2010.
[2]
A. V. Aho, J. E. Hopcroft, and J. D. Ullman. The Design and Analysis of Computer Algorithms. Addison-Wesley, 1974.
[3]
A. Aiken and B. R. Murphy. Implementing regular tree expressions. FPCA, vol. 523 of phLNCS, pages 427--447. Springer, 1991.
[4]
J. C. M. Baeten, J. A. Bergstra, and J. W. Klop. Decidability of bisimulation equivalence for processes generating context-free languages. PARLE (II), vol. 259 of phLNCS, pages 94--111. Springer, 1987.
[5]
F. Bartels. phOn generalized coinduction and probabilistic specification formats. PhD thesis, Vrije Universiteit Amsterdam, 2004.
[6]
F. Bonchi and D. Pous. Extended version of this abstract, with omitted proofs. http://hal.inria.fr/hal-00639716/, 2012\natexlaba.
[7]
F. Bonchi and D. Pous. Web appendix for this paper. http://perso.ens-lyon.fr/damien.pous/hknt, 2012\natexlabb.
[8]
A. Bouajjani, P. Habermehl, and T. Vojnar. Abstract regular model checking. Proc. CAV, vol. 3114 of LNCS. Springer, 2004.
[9]
R. E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Trans. Computers, 35 (8): 677--691, 1986.
[10]
D. Caucal. Graphes canoniques de graphes algébriques. ITA, 24: 339--352, 1990.
[11]
S. Christensen, H. Hüttel, and C. Stirling. Bisimulation equivalence is decidable for all context-free processes. phInformation and Computation, 121 (2): 143--148, 1995.
[12]
L. Doyen and J.-F. Raskin. Antichain Algorithms for Finite Automata. TACAS, vol. 6015 of LNCS. Springer, 2010.
[13]
J.-C. Fernandez, L. Mounier, C. Jard, and T. Jéron. On-the-fly verification of finite transition systems. Formal Methods in System Design, 1 (2/3): 251--273, 1992.
[14]
M. R. Henzinger, T. A. Henzinger, and P. W. Kopke. Computing simulations on finite and infinite graphs. FOCS, pages 453--462. IEEE Computer Society, 1995.
[15]
Y. Hirshfeld, M. Jerrum, and F. Moller. A polynomial algorithm for deciding bisimilarity of normed context-free processes. phTheoretical Computer Science, 158 (1&2): 143--159, 1996.
[16]
L. Holík and J.vSimávcek. Optimizing an LTS-Simulation Algorithm. phComputing and Informatics, 2010 (7): 1337--1348, 2010.
[17]
J. E. Hopcroft. An n log n algorithm for minimizing in a finite automaton. International Symposium of Theory of Machines and Computations, pages 189--196. Academic Press, 1971.
[18]
J. E. Hopcroft and R. M. Karp. A linear algorithm for testing equivalence of finite automata. TR 114, Cornell Univ., December 1971.
[19]
J. E. Hopcroft and J. D. Ullman. phIntroduction to Automata Theory, Languages and Computation. Addison-Wesley, 1979.
[20]
H. Hosoya, J. Vouillon, and B. C. Pierce. Regular expression types for XML. ACM Trans. Program. Lang. Syst., 27 (1): 46--90, 2005.
[21]
et al.(2012)Lengál, Simácek, and Vojnar}LengalSV12O. Lengál, J. Simácek, and T. Vojnar. Vata: A library for efficient manipulation of non-deterministic tree automata. TACAS, vol. 7214 of LNCS, pages 79--94. Springer, 2012.
[22]
M. Lenisa. From set-theoretic coinduction to coalgebraic coinduction: some results, some problems. ENTCS, 19: 2--22, 1999.
[23]
D. Lucanu and G. Rosu. Circular coinduction with special contexts. ICFEM, vol. 5885 of LNCS, pages 639--659. Springer, 2009.
[24]
A. Meyer and L. J. Stockmeyer. Word problems requiring exponential time. STOC, pages 1--9. ACM, 1973.
[25]
R. Milner. Communication and Concurrency. Prentice Hall, 1989.
[26]
D. Pous. Complete lattices and up-to techniques. APLAS, vol. 4807 of LNCS, pages 351--366. Springer, 2007.
[27]
J. Rutten. Automata and coinduction (an exercise in coalgebra). CONCUR, vol. 1466 of LNCS, pages 194--218. Springer, 1998.
[28]
D. Sangiorgi. On the bisimulation proof method. Mathematical Structures in Computer Science, 8: 447--479, 1998.
[29]
D. Sangiorgi. Introduction to Bisimulation and Coinduction. Cambridge University Press, 2011.
[30]
D. Tabakov and M. Vardi. Experimental evaluation of classical automata constructions. LPAR, vol. 3835 of LNCS, pages 396--411. Springer, 2005.
[31]
M. D. Wulf, L. Doyen, T. A. Henzinger, and J.-F. Raskin. Antichains: A new algorithm for checking universality of finite automata. CAV, vol. 4144 of LNCS, pages 17--30. Springer, 2006.

Cited By

View all
  • (2025)Symbolic Automata: Omega-Regularity Modulo TheoriesProceedings of the ACM on Programming Languages10.1145/37048389:POPL(33-66)Online publication date: 9-Jan-2025
  • (2024)Systems of Fixpoint Equations: Abstraction, Games, Up-To Techniques and Local AlgorithmsInformation and Computation10.1016/j.ic.2024.105233(105233)Online publication date: Oct-2024
  • (2024)Equivalence of Data Petri Nets with ArithmeticBusiness Process Management Workshops10.1007/978-3-031-50974-2_31(409-421)Online publication date: 11-Jan-2024
  • Show More Cited By

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices
ACM SIGPLAN Notices  Volume 48, Issue 1
POPL '13
January 2013
561 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/2480359
Issue’s Table of Contents
  • cover image ACM Conferences
    POPL '13: Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages
    January 2013
    586 pages
    ISBN:9781450318327
    DOI:10.1145/2429069
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 23 January 2013
Published in SIGPLAN Volume 48, Issue 1

Check for updates

Author Tags

  1. antichain
  2. automata
  3. bisimulation
  4. coinduction
  5. congruence
  6. language equivalence
  7. up-to techniques

Qualifiers

  • Research-article

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)73
  • Downloads (Last 6 weeks)8
Reflects downloads up to 19 Feb 2025

Other Metrics

Citations

Cited By

View all
  • (2025)Symbolic Automata: Omega-Regularity Modulo TheoriesProceedings of the ACM on Programming Languages10.1145/37048389:POPL(33-66)Online publication date: 9-Jan-2025
  • (2024)Systems of Fixpoint Equations: Abstraction, Games, Up-To Techniques and Local AlgorithmsInformation and Computation10.1016/j.ic.2024.105233(105233)Online publication date: Oct-2024
  • (2024)Equivalence of Data Petri Nets with ArithmeticBusiness Process Management Workshops10.1007/978-3-031-50974-2_31(409-421)Online publication date: 11-Jan-2024
  • (2023)Automatic Decomposition of Reward Machines for Decentralized Multiagent Reinforcement Learning2023 62nd IEEE Conference on Decision and Control (CDC)10.1109/CDC49753.2023.10384224(5423-5430)Online publication date: 13-Dec-2023
  • (2022)Coalgebraic Semantics for Nominal AutomataCoalgebraic Methods in Computer Science10.1007/978-3-031-10736-8_3(45-66)Online publication date: 23-Jul-2022
  • (2021)Reward Machines for Cooperative Multi-Agent Reinforcement LearningProceedings of the 20th International Conference on Autonomous Agents and MultiAgent Systems10.5555/3463952.3464063(934-942)Online publication date: 3-May-2021
  • (2021)Learning Nondeterministic Real-Time AutomataACM Transactions on Embedded Computing Systems10.1145/347703020:5s(1-26)Online publication date: 22-Sep-2021
  • (2021)Complete Abstractions for Checking Language InclusionACM Transactions on Computational Logic10.1145/346267322:4(1-40)Online publication date: 8-Sep-2021
  • (2021)Efficient local computation of differential bisimulations via coupling and up-to methodsProceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science10.1109/LICS52264.2021.9470555(1-14)Online publication date: 29-Jun-2021
  • (2020)Synthesis of Partially Observed Jump-Diffusion Systems via Control Barrier FunctionsIEEE Control Systems Letters10.1109/LCSYS.2020.3001562(1-1)Online publication date: 2020
  • Show More Cited By

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media