Minimizing Deterministic Lattice Automata

  • Shulamit Halamish
  • Orna Kupferman
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 6604)

Abstract

Traditional automata accept or reject their input, and are therefore Boolean. In contrast, weighted automata map each word to a value from a semiring over a large domain. The special case of lattice automata, in which the semiring is a finite lattice, has interesting theoretical properties as well as applications in formal methods. A minimal deterministic automaton captures the combinatoric nature and complexity of a formal language. Deterministic automata are used in run-time monitoring, pattern recognition, and modeling systems. Thus, the minimization problem for deterministic automata is of great interest, both theoretically and in practice.

For traditional automata on finite words, a minimization algorithm, based on the Myhill-Nerode right congruence on the set of words, generates in polynomial time a canonical minimal deterministic automaton. A polynomial algorithm is known also for weighted automata over the tropical semiring. For general deterministic weighted automata, the problem of minimization is open. In this paper we study minimization of lattice automata. We show that it is impossible to define a right congruence in the context of lattices, and that no canonical minimal automaton exists. Consequently, the minimization problem is much more complicated, and we prove that it is NP-complete. As good news, we show that while right congruence fails already for finite lattices that are fully ordered, for this setting we are able to combine a finite number of right congruences and generate a minimal deterministic automaton in polynomial time.

References

  1. 1.
    Alur, R., Kanade, A., Weiss, G.: Ranking automata and games for prioritized requirements. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 240–253. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  2. 2.
    ESF Network programme. Automata: from mathematics to applications (AutoMathA) (2010), http://www.esf.org/index.php?id=1789
  3. 3.
    Bruns, G., Godefroid, P.: Model checking partial state spaces with 3-valued temporal logics. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 274–287. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  4. 4.
    Bruns, G., Godefroid, P.: Temporal logic query checking. In: Proc. 16th LICS, pp. 409–420. IEEE Computer Society, Los Alamitos (2001)Google Scholar
  5. 5.
    Chan, W.: Temporal-logic queries. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 450–463. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  6. 6.
    Chechik, M., Devereux, B., Gurfinkel, A.: Model-checking infinite state-space systems with fine-grained abstractions using SPIN. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol. 2057, pp. 16–36. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  7. 7.
    Droste, M., Kuich, W., Vogler, H. (eds.): Handbook of Weighted Automata. Springer, Heidelberg (2009)MATHGoogle Scholar
  8. 8.
    Easterbrook, S., Chechik, M.: A framework for multi-valued reasoning over inconsistent viewpoints. In: Proc. 23rd Int. Conf. on Software Engineering, pp. 411–420. IEEE Computer Society Press, Los Alamitos (2001)Google Scholar
  9. 9.
    Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72–83. Springer, Heidelberg (1997)CrossRefGoogle Scholar
  10. 10.
    Henzinger, T.A.: From boolean to quantitative notions of correctness. In: Proc. 37th POPL, pp. 157–158 (2010)Google Scholar
  11. 11.
    Hussain, A., Huth, M.: On model checking multiple hybrid views. Technical Report TR-2004-6, University of Cyprus (2004)Google Scholar
  12. 12.
    Karp, R.M.: Reducibility among combinatorial problems. In: Complexity of Computer Computations, pp. 85–103 (1972)CrossRefGoogle Scholar
  13. 13.
    Kupferman, O., Lustig, Y.: Lattice automata. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol. 4349, pp. 199–213. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  14. 14.
    Kupferman, O., Lustig, Y.: Latticed simulation relations and games. International Journal on the Foundations of Computer Science 21(2), 167–189 (2010)MathSciNetCrossRefGoogle Scholar
  15. 15.
    Kirsten, D., Mäurer, I.: On the determinization of weighted automata. Journal of Automata, Languages and Combinatorics 10(2/3), 287–312 (2005)MathSciNetMATHGoogle Scholar
  16. 16.
    Krob, D.: The equality problem for rational series with multiplicities in the tropical emiring is undecidable. Journal of Algebra and Computation 4, 405–425 (1994)CrossRefGoogle Scholar
  17. 17.
    Li, Y., Pedrycz, W.: Minimization of lattice finite automata and its application to the decomposition of lattice languages. Fuzzy Sets and Systems 158(13), 1423–1436 (2007)MathSciNetCrossRefGoogle Scholar
  18. 18.
    Mohri, M.: Finite-state transducers in language and speech processing. Computational Linguistics 23(2), 269–311 (1997)MathSciNetGoogle Scholar
  19. 19.
    Malik, D.S., Mordeson, J.N., Sen, M.K.: Minimization of fuzzy finite automata. Information Sciences 113, 323–330 (1999)MathSciNetCrossRefGoogle Scholar
  20. 20.
    Myhill, J.: Finite automata and the representation of events. Technical Report WADD TR-57-624, pp. 112–137, Wright Patterson AFB, Ohio (1957)Google Scholar
  21. 21.
    Nerode, A.: Linear automaton transformations. Proceedings of the American Mathematical Society 9(4), 541–544 (1958)MathSciNetCrossRefGoogle Scholar
  22. 22.
    Zekai, L., Lan, S.: Minimization of lattice automata. In: Proc. 2nd ICFIE, pp. 194–205 (2007)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2011

Authors and Affiliations

  • Shulamit Halamish
    • 1
  • Orna Kupferman
    • 1
  1. 1.School of Engineering and Computer ScienceHebrew UniversityJerusalemIsrael

Personalised recommendations