Document Open Access Logo

Minimal DFAs Witnessing Language Inequivalence

Author Jan Martens

PDF

File

Thumbnail PDF
PDF
LIPIcs.CSL.2026.44.pdf
  • Filesize: 0.87 MB
  • 16 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Regular languages
Keywords
  • Deterministic Finite Automata
  • Language Inequivalence
  • DFA decomposition
  • Prime languages

Metrics

Abstract

We study small witnesses for the inequivalence of two regular languages. A natural witness is a distinguishing word, e.g. a word in exactly one of the two languages. We propose using more succinct witnesses in the form of witnessing DFAs. A witnessing DFA recognizes a subset of one of the languages and contains at least one distinguishing word. In this way the DFA expresses behaviour contained in the first language but not the second. We show witnessing DFAs can be used to present more concise witnesses for the inequivalence of two regular languages. We show that the decision problem for the existence of a witnessing DFA of certain size is NP-complete in general, and in P in the special case of unary DFAs. Besides these computational aspects, we study structural properties of witnessing DFAs. Not all languages can be a minimal witness. It turns out that minimal witnesses are exactly the languages that are not decomposable in the union of languages with smaller state-complexity, the so-called prime languages as studied earlier by Kupferman and Mosheiff.

Cite As Get BibTex

Jan Martens. Minimal DFAs Witnessing Language Inequivalence. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 44:1-44:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.CSL.2026.44

Author Details

Jan Martens
  • Leiden Institute of Advanced Computer Science, Leiden University, The Netherlands

References

  1. J. Almeida, M. V. Volkov, and S. V. Goldberg. Complexity of the identity checking problem for finite semigroups. Journal of Mathematical Sciences, 158(5):605-614, 2009. URL: https://doi.org/10.1007/s10958-009-9397-z.
  2. Andrei A. Bulatov, Olga Karpova, Arseny M. Shur, and Konstantin Startsev. Lower bounds on words separation: Are there short identities in transformation semigroups?, August 2017. URL: https://doi.org/10.37236/6450.
  3. Rance Cleaveland. On automatically explaining bisimulation inequivalence. In Edmund M. Clarke and Robert P. Kurshan, editors, Proc. Computer-Aided Verification (CAV 1990), pages 364-372, Berlin, Heidelberg, 1991. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/BFb0023750.
  4. Erik D Demaine, Sarah Eisenstat, Jeffrey Shallit, and David A Wilson. Remarks on separating words. In Markus Holzer, Martin Kutrib, and Giovanni Pighizzini, editors, Proc. of DCFS 2011, volume 6808 of LNCS, pages 147-157. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-22600-7_12.
  5. Mark E. Gold. Complexity of automaton identification from given data. Information and Control, 37(3):302-320, 1978. URL: https://doi.org/10.1016/S0019-9958(78)90562-4.
  6. Hermann Gruber, Markus Holzer, and Christian Rauch. The pumping lemma for regular languages is hard. In International Conference on Implementation and Application of Automata, pages 128-140. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-40247-0_9.
  7. Matthew Hennessy and Robin Milner. On observing nondeterminism and concurrency. In Jaco de Bakker and Jan van Leeuwen, editors, Automata, Languages and Programming (ICALP `1980), pages 299-309, Berlin, Heidelberg, 1980. Springer-Verlag. URL: https://doi.org/10.5555/646234.758793.
  8. John Hopcroft. An n log n algorithm for minimizing states in a finite automaton. In Zvi Kohavi and Azaria Paz, editors, Theory of Machines and Computations, pages 189-196. Academic Press, 1971. URL: https://doi.org/10.1016/B978-0-12-417750-5.50022-1.
  9. Ismaël Jecker, Orna Kupferman, and Nicolas Mazzocchi. Unary Prime Languages. In Javier Esparza and Daniel Král', editors, Proc. of MFCS 2020, volume 170 of Leibniz International Proceedings in Informatics (LIPIcs), pages 51:1-51:12, Dagstuhl, Germany, 2020. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.MFCS.2020.51.
  10. Ondřej Klíma. Identity checking problem for transformation monoids. Semigroup Forum, 84(3):487-498, 2012. URL: https://doi.org/10.1007/s00233-012-9401-7.
  11. Dexter Kozen. Lower bounds for natural proof systems. In Proc. of SFCS 1977, pages 254-266. IEEE, 1977. URL: https://doi.org/10.1109/SFCS.1977.16.
  12. Orna Kupferman and Jonathan Mosheiff. Prime languages. Information and Computation, 240:90-107, 2015. URL: https://doi.org/10.1016/j.ic.2014.09.010.
  13. Jan Martens. Deciding minimal distinguishing DFAs is NP-complete. arXiv preprint arXiv:2306.03533, 2023. URL: https://doi.org/10.48550/arXiv.2306.03533.
  14. Jan Martens and Jan Friso Groote. Computing minimal distinguishing Hennessy-Milner formulas is NP-hard, but variants are tractable. In G.A. Pérez and J.-F. Raskin, editors, Proc. of CONCUR 2023, volume 279 of LIPIcs, pages 32:1-32:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2023.32.
  15. Tyler Moore. Gedanken-experiments on sequential machines. In C. E. Shannon and J. McCarthy, editors, Automata Studies, Annals of Mathematical Studies, no. 34. Citeseer, 1956. Google Scholar
  16. John R. Myhill. Finite automata and the representation of events. WADD Technical Report, 57-624:112-137, 1957. Google Scholar
  17. Anil Nerode. Linear automaton transformations. Proceedings of the American Mathematical Society, 9(4):541-544, 1958. URL: https://doi.org/10.1090/S0002-9939-1958-0135681-9.
  18. Charles P. Pfleeger. State reduction in incompletely specified finite-state machines. IEEE Transactions on Computers, 100(12):1099-1102, 1973. URL: https://doi.org/10.1109/T-C.1973.223655.
  19. Rick Smetsers, Joshua Moerman, and David N Jansen. Minimal separating sequences for all pairs of states. In Adrian-Horia Dediu, Jan Janoušek, Carlos Martín-Vide, and Bianca Truthe, editors, Proc. of (LATA 2016), volume 9618 of LNCS, pages 181-193. Springer, 2016. URL: https://doi.org/10.1007/978-3-319-30000-9_14.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact