Algorithms for Kleene algebra with converse
| Autor: | Damien Pous, Paul Brunet |
|---|---|
| Rok vydání: | 2016 |
| Předmět: |
060201 languages & linguistics
Bisimulation Discrete mathematics TheoryofComputation_COMPUTATIONBYABSTRACTDEVICES Logic Binary relation Transitive closure 06 humanities and the arts 02 engineering and technology Automata construction Theoretical Computer Science Decidability Kleene algebra TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES Computational Theory and Mathematics 0602 languages and literature 0202 electrical engineering electronic engineering information engineering 020201 artificial intelligence & image processing Regular expression Algorithm Computer Science::Formal Languages and Automata Theory Software PSPACE Mathematics |
| Zdroj: | Journal of Logical and Algebraic Methods in Programming. 85:574-594 |
| ISSN: | 2352-2208 |
| DOI: | 10.1016/j.jlamp.2015.07.005 |
| Popis: | The equational theory generated by all algebras of binary relations with operations of union, composition, converse and reflexive transitive closure was studied by Bernatsky, Bloom, Esik and Stefanescu in 1995. In particular, they obtained its decidability by using a particular automata construction. We show that deciding this equational theory is PSpace -complete, by providing a PSpace algorithm (the problem is easily shown to be PSpace -hard). We obtain other algorithms that are time-efficient in practice, despite not being PSpace . Our results use an alternative automata construction, inspired by the one from Bloom, Esik and Stefanescu. We relate those two constructions by exhibiting a bisimulation between the resulting deterministic automata, and by showing how our construction results in more sharing between states, thus producing smaller automata. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full Text from ScienceDirect