On equivalence checking of nondeterministic finite automata

Chen Fu; Yuxin Deng; David N. Jansen; Lijun Zhang

doi:10.1007/978-3-319-69483-2_13

On equivalence checking of nondeterministic finite automata

Chen Fu^*
, Yuxin Deng
, David N. Jansen
, Lijun Zhang

^*Corresponding author for this work

Software Engineering Institute

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

1 Scopus citations

Abstract

We provide a comparative study of some typical algorithms for language equivalence in nondeterministic finite automata and various combinations of optimization techniques. We find that their practical efficiency mostly depends on the density and the alphabet size of the automaton under consideration. Based on our experiments, we suggest to use HKC (Hopcroft and Karp’s algorithm up to congruence) [4] if the density is large and the alphabet is small; otherwise, we recommend the antichain algorithm (Wulf, Doyen, Henzinger, Raskin) [6]. Bisimulation equivalence and memoisation both pay off in general. When comparing highly structured automata over a large alphabet, one should use symbolic algorithms.

Original language	English
Title of host publication	Dependable Software Engineering
Subtitle of host publication	Theories, Tools, and Applications - 3rd International Symposium, SETTA 2017, Proceedings
Editors	Ji Wang, Kim Guldstrand Larsen, Oleg Sokolsky
Publisher	Springer Verlag
Pages	216-231
Number of pages	16
ISBN (Print)	9783319694825
DOIs	https://doi.org/10.1007/978-3-319-69483-2_13
State	Published - 2017
Event	3rd International Symposium on Dependable Software Engineering: Theories, Tools and Applications, SETTA 2017 - Changsha, China Duration: 23 Oct 2017 → 25 Oct 2017

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	10606 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	3rd International Symposium on Dependable Software Engineering: Theories, Tools and Applications, SETTA 2017
Country/Territory	China
City	Changsha
Period	23/10/17 → 25/10/17

Access to Document

10.1007/978-3-319-69483-2_13

Cite this

Fu, C., Deng, Y., Jansen, D. N., & Zhang, L. (2017). On equivalence checking of nondeterministic finite automata. In J. Wang, K. G. Larsen, & O. Sokolsky (Eds.), Dependable Software Engineering: Theories, Tools, and Applications - 3rd International Symposium, SETTA 2017, Proceedings (pp. 216-231). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10606 LNCS). Springer Verlag. https://doi.org/10.1007/978-3-319-69483-2_13

Fu, Chen ; Deng, Yuxin ; Jansen, David N. et al. / On equivalence checking of nondeterministic finite automata. Dependable Software Engineering: Theories, Tools, and Applications - 3rd International Symposium, SETTA 2017, Proceedings. editor / Ji Wang ; Kim Guldstrand Larsen ; Oleg Sokolsky. Springer Verlag, 2017. pp. 216-231 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{8b2595bc01344b4d85d67b0c8706f6f1,

title = "On equivalence checking of nondeterministic finite automata",

abstract = "We provide a comparative study of some typical algorithms for language equivalence in nondeterministic finite automata and various combinations of optimization techniques. We find that their practical efficiency mostly depends on the density and the alphabet size of the automaton under consideration. Based on our experiments, we suggest to use HKC (Hopcroft and Karp{\textquoteright}s algorithm up to congruence) [4] if the density is large and the alphabet is small; otherwise, we recommend the antichain algorithm (Wulf, Doyen, Henzinger, Raskin) [6]. Bisimulation equivalence and memoisation both pay off in general. When comparing highly structured automata over a large alphabet, one should use symbolic algorithms.",

author = "Chen Fu and Yuxin Deng and Jansen, \{David N.\} and Lijun Zhang",

note = "Publisher Copyright: {\textcopyright} 2017, Springer International Publishing AG.; 3rd International Symposium on Dependable Software Engineering: Theories, Tools and Applications, SETTA 2017 ; Conference date: 23-10-2017 Through 25-10-2017",

year = "2017",

doi = "10.1007/978-3-319-69483-2\_13",

language = "英语",

isbn = "9783319694825",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "216--231",

editor = "Ji Wang and Larsen, \{Kim Guldstrand\} and Oleg Sokolsky",

booktitle = "Dependable Software Engineering",

address = "德国",

}

Fu, C, Deng, Y, Jansen, DN & Zhang, L 2017, On equivalence checking of nondeterministic finite automata. in J Wang, KG Larsen & O Sokolsky (eds), Dependable Software Engineering: Theories, Tools, and Applications - 3rd International Symposium, SETTA 2017, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 10606 LNCS, Springer Verlag, pp. 216-231, 3rd International Symposium on Dependable Software Engineering: Theories, Tools and Applications, SETTA 2017, Changsha, China, 23/10/17. https://doi.org/10.1007/978-3-319-69483-2_13

On equivalence checking of nondeterministic finite automata. / Fu, Chen; Deng, Yuxin; Jansen, David N. et al.
Dependable Software Engineering: Theories, Tools, and Applications - 3rd International Symposium, SETTA 2017, Proceedings. ed. / Ji Wang; Kim Guldstrand Larsen; Oleg Sokolsky. Springer Verlag, 2017. p. 216-231 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10606 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - On equivalence checking of nondeterministic finite automata

AU - Fu, Chen

AU - Deng, Yuxin

AU - Jansen, David N.

AU - Zhang, Lijun

PY - 2017

Y1 - 2017

N2 - We provide a comparative study of some typical algorithms for language equivalence in nondeterministic finite automata and various combinations of optimization techniques. We find that their practical efficiency mostly depends on the density and the alphabet size of the automaton under consideration. Based on our experiments, we suggest to use HKC (Hopcroft and Karp’s algorithm up to congruence) [4] if the density is large and the alphabet is small; otherwise, we recommend the antichain algorithm (Wulf, Doyen, Henzinger, Raskin) [6]. Bisimulation equivalence and memoisation both pay off in general. When comparing highly structured automata over a large alphabet, one should use symbolic algorithms.

AB - We provide a comparative study of some typical algorithms for language equivalence in nondeterministic finite automata and various combinations of optimization techniques. We find that their practical efficiency mostly depends on the density and the alphabet size of the automaton under consideration. Based on our experiments, we suggest to use HKC (Hopcroft and Karp’s algorithm up to congruence) [4] if the density is large and the alphabet is small; otherwise, we recommend the antichain algorithm (Wulf, Doyen, Henzinger, Raskin) [6]. Bisimulation equivalence and memoisation both pay off in general. When comparing highly structured automata over a large alphabet, one should use symbolic algorithms.

UR - https://www.scopus.com/pages/publications/85032698428

U2 - 10.1007/978-3-319-69483-2_13

DO - 10.1007/978-3-319-69483-2_13

M3 - 会议稿件

AN - SCOPUS:85032698428

SN - 9783319694825

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 216

EP - 231

BT - Dependable Software Engineering

A2 - Wang, Ji

A2 - Larsen, Kim Guldstrand

A2 - Sokolsky, Oleg

PB - Springer Verlag

T2 - 3rd International Symposium on Dependable Software Engineering: Theories, Tools and Applications, SETTA 2017

Y2 - 23 October 2017 through 25 October 2017

ER -

Fu C, Deng Y, Jansen DN, Zhang L. On equivalence checking of nondeterministic finite automata. In Wang J, Larsen KG, Sokolsky O, editors, Dependable Software Engineering: Theories, Tools, and Applications - 3rd International Symposium, SETTA 2017, Proceedings. Springer Verlag. 2017. p. 216-231. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-319-69483-2_13

On equivalence checking of nondeterministic finite automata

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this