skip to main content
10.1145/2429069.2429124acmconferencesArticle/Chapter ViewAbstractPublication PagespoplConference Proceedingsconference-collections
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

Recommendations

Comments

Information & Contributors

Information

Published In

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
  • 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
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]

Sponsors

In-Cooperation

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 23 January 2013

Permissions

Request permissions for this article.

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

Conference

POPL '13
Sponsor:

Acceptance Rates

Overall Acceptance Rate 860 of 4,328 submissions, 20%

Upcoming Conference

POPL '26

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)On algorithms verifying initial-and-final-state opacity: Complexity, special cases, and comparisonAutomatica10.1016/j.automatica.2025.112171174(112171)Online publication date: Apr-2025
  • (2024)KATch: A Fast Symbolic Verifier for NetKATProceedings of the ACM on Programming Languages10.1145/36564548:PLDI(1905-1928)Online publication date: 20-Jun-2024
  • (2024)Relating behaviour of data-aware process modelsData & Knowledge Engineering10.1016/j.datak.2024.102363154:COnline publication date: 1-Nov-2024
  • (2024)On Concurrent Program Algebra and Demonic AutomataTheoretical Aspects of Computing – ICTAC 202410.1007/978-3-031-77019-7_7(114-131)Online publication date: 25-Nov-2024
  • (2024)Language Equivalence from Nondeterministic to Weighted Automata—and BackLeveraging Applications of Formal Methods, Verification and Validation. REoCAS Colloquium in Honor of Rocco De Nicola10.1007/978-3-031-73709-1_6(75-93)Online publication date: 9-Oct-2024
  • (2024)Mata: A Fast and Simple Finite Automata LibraryTools and Algorithms for the Construction and Analysis of Systems10.1007/978-3-031-57249-4_7(130-151)Online publication date: 5-Apr-2024
  • (2024)A Uniform Framework for Language Inclusion ProblemsTaming the Infinities of Concurrency10.1007/978-3-031-56222-8_9(155-171)Online publication date: 20-Mar-2024
  • (2023)Fast Coalgebraic Bisimilarity MinimizationProceedings of the ACM on Programming Languages10.1145/35712457:POPL(1514-1541)Online publication date: 11-Jan-2023
  • (2023)Kater: Automating Weak Memory Model Metatheory and Consistency CheckingProceedings of the ACM on Programming Languages10.1145/35712127:POPLOnline publication date: 11-Jan-2023
  • (2023)Up-to techniques for behavioural metrics via fibrationsMathematical Structures in Computer Science10.1017/S0960129523000166(1-40)Online publication date: 10-Jul-2023
  • 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