Hacking Nondeterminism with Induction and Coinduction.
We introduce bisimulation up to congruence as a technique for proving language equivalence of nondeterministic finite automata. Exploiting this technique, we devise an optimization of the classic algorithm by Hopcroft and Karp. We compare our approach to the recently introduced antichain algorithms...
| Publicado en: | Communications of the ACM Vol. 58; no. 2; pp. 87 - 96 |
|---|---|
| Autores principales: | , |
| Formato: | Artículo |
| Publicado: |
Association for Computing Machinery
Feb2015
|
| Materias: | |
| Acceso en línea: | Ver este registro en EBSCOhost |
| fields | @attributes: recordID: 1 pdfLink: plink: https://search.ebscohost.com/login.aspx?direct=true&db=hlh&AN=100777474&site=ehost-live header: @attributes: shortDbName: hlh uiTerm: 100777474 longDbName: Humanities International Complete uiTag: AN controlInfo: bkinfo: jinfo: jid: 00010782 ACM jtl: Communications of the ACM issn: 00010782 maglogo: N pubinfo: dt: Feb2015 vid: 58 iid: 2 pid: 68 pub: Association for Computing Machinery artinfo: ui: 100777474 10.1145/2713167 ppf: 87 ppct: 9 formats: tig: atl: Hacking Nondeterminism with Induction and Coinduction. aug: au: Bonchi, Filippo Pous, Damien affil: Université de Lyon, UMR 5668, France su: Machine theory Algorithms Bisimulation Coinduction (Mathematics) Programming languages Program transformation sug: subj: Machine theory Algorithms Bisimulation Coinduction (Mathematics) Programming languages Program transformation ab: We introduce bisimulation up to congruence as a technique for proving language equivalence of nondeterministic finite automata. Exploiting this technique, we devise an optimization of the classic algorithm by Hopcroft and Karp. We compare our approach to the recently introduced antichain algorithms and we give concrete examples where we exponentially improve over antichains. Experimental results show significant improvements. pubtype: Periodical doctype: Article src: R language: English refInfo: copyright: @attributes: flag: Y dt: @attributes: year: 2015 holdings: @attributes: islocal: N |
|---|