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

^*此作品的通讯作者

软件工程学院

CAS - Institute of Software
University of Chinese Academy of Sciences

科研成果: 书/报告/会议事项章节 › 会议稿件 › 同行评审

1 引用（Scopus）

摘要

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.

源语言	英语
主期刊名	Dependable Software Engineering
主期刊副标题	Theories, Tools, and Applications - 3rd International Symposium, SETTA 2017, Proceedings
编辑	Ji Wang, Kim Guldstrand Larsen, Oleg Sokolsky
出版商	Springer Verlag
页	216-231
页数	16
ISBN（印刷版）	9783319694825
DOI	https://doi.org/10.1007/978-3-319-69483-2_13
出版状态	已出版 - 2017
活动	3rd International Symposium on Dependable Software Engineering: Theories, Tools and Applications, SETTA 2017 - Changsha, 中国期限: 23 10月 2017 → 25 10月 2017

出版系列

姓名	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
卷	10606 LNCS
ISSN（印刷版）	0302-9743
ISSN（电子版）	1611-3349

会议

会议	3rd International Symposium on Dependable Software Engineering: Theories, Tools and Applications, SETTA 2017
国家/地区	中国
市	Changsha
时期	23/10/17 → 25/10/17

访问文件

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

其它文件与链接

链接到 Scopus 的出版物

引用此

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

Fu, Chen ; Deng, Yuxin ; Jansen, David N. 等. / On equivalence checking of nondeterministic finite automata. Dependable Software Engineering: Theories, Tools, and Applications - 3rd International Symposium, SETTA 2017, Proceedings. 编辑 / Ji Wang ; Kim Guldstrand Larsen ; Oleg Sokolsky. Springer Verlag, 2017. 页码 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. 在 J Wang, KG Larsen & O Sokolsky (编辑), 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), 卷 10606 LNCS, Springer Verlag, 页码 216-231, 3rd International Symposium on Dependable Software Engineering: Theories, Tools and Applications, SETTA 2017, Changsha, 中国, 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. 等.
Dependable Software Engineering: Theories, Tools, and Applications - 3rd International Symposium, SETTA 2017, Proceedings. 编辑 / Ji Wang; Kim Guldstrand Larsen; Oleg Sokolsky. Springer Verlag, 2017. 页码 216-231 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); 卷 10606 LNCS).

科研成果: 书/报告/会议事项章节 › 会议稿件 › 同行评审

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. 在 Wang J, Larsen KG, Sokolsky O, 编辑, Dependable Software Engineering: Theories, Tools, and Applications - 3rd International Symposium, SETTA 2017, Proceedings. Springer Verlag. 2017. 页码 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

摘要

出版系列

会议

访问文件

其它文件与链接

指纹

引用此