Geodesic
Using SAT solvers for synchronization issues in non-deterministic automata
Sibirskie èlektronnye matematičeskie izvestiâ, Tome 15 (2018), pp. 1426-1442.

Voir la notice de l'article provenant de la source Math-Net.Ru

We approach the problem of computing a $D_{3}$-synchronizing word of minimum length for a given nondeterministic automaton via its encoding as an instance of SAT and invoking a SAT solver. We also present some experimental results.
Keywords: nondeterministic automaton, synchronizing word, SAT, SAT-solver, random automaton. 
@article{SEMR_2018_15_a79,
     author = {H. Shabana and M. V. Volkov},
     title = {Using {SAT} solvers for synchronization issues in non-deterministic automata},
     journal = {Sibirskie \`elektronnye matemati\v{c}eskie izvesti\^a},
     pages = {1426--1442},
     publisher = {mathdoc},
     volume = {15},
     year = {2018},
     language = {en},
     url = {http://geodesic.mathdoc.fr/item/SEMR_2018_15_a79/}
}
TY  - JOUR
AU  - H. Shabana
AU  - M. V. Volkov
TI  - Using SAT solvers for synchronization issues in non-deterministic automata
JO  - Sibirskie èlektronnye matematičeskie izvestiâ
PY  - 2018
SP  - 1426
EP  - 1442
VL  - 15
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/SEMR_2018_15_a79/
LA  - en
ID  - SEMR_2018_15_a79
ER  - 
%0 Journal Article
%A H. Shabana
%A M. V. Volkov
%T Using SAT solvers for synchronization issues in non-deterministic automata
%J Sibirskie èlektronnye matematičeskie izvestiâ
%D 2018
%P 1426-1442
%V 15
%I mathdoc
%U http://geodesic.mathdoc.fr/item/SEMR_2018_15_a79/
%G en
%F SEMR_2018_15_a79
H. Shabana; M. V. Volkov. Using SAT solvers for synchronization issues in non-deterministic automata. Sibirskie èlektronnye matematičeskie izvestiâ, Tome 15 (2018), pp. 1426-1442. http://geodesic.mathdoc.fr/item/SEMR_2018_15_a79/

[1] C. H. Papadimitriou, Computational Complexity, Addison-Wesley, 1994 | MR | Zbl

[2] M. V. Volkov, “Synchronizing automata and the Černý conjecture”, Language and Automata Theory and Applications, Lect. Notes Comput. Sci., 5196, 2008, 11–27 | DOI | MR | Zbl

[3] J. Kari, M. V. Volkov, “Černý's conjecture and the Road Coloring Problem”, Handbook of Automata Theory, Chapter 15, v. I, ed. J.-É. Pin, EMS Publishing House (to appear)

[4] B. Imreh, M. Steinby, “Directable nondeterministic automata”, Acta Cybernetica, 14:1 (1999), 105–115 | MR | Zbl

[5] P. Martyugin, “A lower bound for the length of the shortest carefully synchronizing words”, Russ. Math., 54:1 (2010), 46–54 | DOI | MR | Zbl

[6] M. Ito, Algebraic Theory of Automata and Languages, World Scientific, 2004 | MR | Zbl

[7] V. D. Blondel, R. M. Jungers, A. Olshevsky, “On primitivity of sets of matrices”, Automatica J. IFAC, 61 (2015), 80–88 | DOI | MR | Zbl

[8] B. Gerencsér, V. V. Gusev, R. M. Jungers, “Primitive sets of nonnegative matrices and synchronizing automata”, SIAM J. Matrix Analysis and Applications, 39:1 (2018), 83–98 | DOI | MR | Zbl

[9] H. Don, H. Zantema, “Synchronizing non-deterministic finite automata”, J. Automata, Languages and Combinatorics, 23:4 (2018), 307–328 | DOI

[10] M. Steinby, Directable fuzzy and nondeterministic automata, 2017, arXiv: 1709.07719

[11] S. Sandberg, “Homing and synchronizing sequences”, Model-Based Testing of Reactive Systems, Lect. Notes Comput. Sci., 3472, 2005, 5–33 | DOI

[12] J.-E. Pin, “On two combinatorial problems arising from automata theory”, Ann. Discrete Math., 17 (1983), 535–548 | MR | Zbl

[13] Kibernetika, 1980, no. 2, 31–35 | DOI | MR | Zbl

[14] I. K. Rystsov, “Polynomial complete problems in automata theory”, Inf. Process. Lett., 16:3 (1983), 147–151 | DOI | MR | Zbl

[15] P. Martyugin, “Synchronization of automata with one undefined or ambiguous transition”, Implementation and Application of Automata, Lect. Notes Comput. Sci., 7381, 2012, 278–288 | DOI | MR | Zbl

[16] C. P. Gomes, H. Kautz, A. Sabharwal, B. Selman, “Satisfiability Solvers”, Handbook of Knowledge Representation, Chapter 2, Elsevier, 2008, 89–134 | DOI | Zbl

[17] J. Geldenhuys, B. van der Merwe, L. van Zijl, “Reducing nondeterministic finite automata with SAT solvers”, Finite-State Methods and Natural Language Processing, Lect. Notes Comput. Sci., 6062, 2009, 81–92 | DOI

[18] T. Jiang, B. Ravikumar, “Minimal NFA problems are hard”, Automata, Languages and Programming, Lect. Notes Comput. Sci., 510, 1991, 629–640 | DOI | MR | Zbl

[19] E. Skvortsov, E. Tipikin, “Experimental study of the shortest reset word of random automata”, Implementation and Application of Automata, Lect. Notes Comput. Sci., 6807, 2011, 290–298 | DOI | MR | Zbl

[20] C. Güniçen, E. Erdem, H. Yenigün, “Generating shortest synchronizing sequences using Answer Set Programming”, Proceedings of Answer Set Programming and Other Computing Paradigms (ASPOCP 2013), 6th International Workshop, 2013, 117–127, arXiv: 1312.6146

[21] J. Olschewski, M. Ummels, “The complexity of finding reset words in finite automata”, Mathematical Foundations of Computer Science, Lect. Notes Comput. Sci., 6281, 2010, 568–579 | DOI | MR | Zbl

[22] N. Eén, N. S{ö}rensson, “An extensible SAT-solver”, Theory and Applications of Satisfiability Testing (SAT 2003), Lect. Notes Comput. Sci., 2919, 2004, 502–518 | DOI | Zbl

[23] N. Eén, N. S{ö}rensson, The MiniSat Page, http://minisat.se

[24] D. Tabakov, M. Y. Vardi, “Experimental evaluation of classical automata constructions”, Logic for Programming, Artificial Intelligence, and Reasoning, Lect. Notes Comput. Sci., 3835, 2005, 396–411 | DOI | Zbl

[25] A. Kisielewicz, J. Kowalski, M. Szykuła, “Computing the shortest reset words of synchronizing automata”, J. Comb. Optim., 29:1 (2015), 88–124 | DOI | MR | Zbl

[26] M. Soos, CryptoMiniSat 2, http://www.msoos.org/cryptominisat2/

[27] A. Biere, “Yet another Local Search Solver and Lingeling and Friends entering the SAT Competition 2014”, Proceedings of SAT Competition 2014: Solver and Benchmark Descriptions, University of Helsinki, 2014, 39–40

[28] M. de Bondt, H. Don, H. Zantema, “DFAs and PFAs with long shortest synchronizing word length”, Developments in Language Theory, Lect. Notes Comput. Sci., 10396, 2017, 122–133 | DOI | MR | Zbl

[29] M. de Bondt, H. Don, H. Zantema, Lower bounds for synchronizing word lengths in partial automata, 2018, arXiv: 1801.10436