Lattice Automata

  • Orna Kupferman
  • Yoad Lustig
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4349)


Several verification methods involve reasoning about multi-valued systems, in which an atomic proposition is interpreted at a state as a lattice element, rather than a Boolean value. The automata-theoretic approach for reasoning about Boolean-valued systems has proven to be very useful and powerful. We develop an automata-theoretic framework for reasoning about multi-valued objects, and describe its application. The basis to our framework are lattice automata on finite and infinite words, which assign to each input word a lattice element. We study the expressive power of lattice automata, their closure properties, the blow-up involved in related constructions, and decision problems for them. Our framework and results are different and stronger then those known for semi-ring and weighted automata. Lattice automata exhibit interesting features from a theoretical point of view. In particular, we study the complexity of constructions and decision problems for lattice automata in terms of the size of both the automaton and the underlying lattice. For example, we show that while determinization of lattice automata involves a blow up that depends on the size of the lattice, such a blow up can be avoided when we complement lattice automata. Thus, complementation is easier than determinization. In addition to studying the theoretical aspects of lattice automata, we describe how they can be used for an efficient reasoning about a multi-valued extension of LTL.


Model Check Closure Property Atomic Proposition Lattice Element Kripke Structure 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. CAV 1999.
    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
  2. Bruns, G., Godefroid, P.: Temporal logic query checking. In: Proc. 16th LICS, pp. 409–420 (2001)Google Scholar
  3. ICALP 2004.
    Bruns, G., Godefroid, P.: Model checking with 3-valued temporal logics. In: Díaz, J., et al. (eds.) ICALP 2004. LNCS, vol. 3142, pp. 281–293. Springer, Heidelberg (2004)Google Scholar
  4. Chechik, M., Devereux, B., Gurfinkel, A.: Model-checking infinite state-space systems with fine-grained abstractions using SPIN. In: Dwyer, M.B. (ed.) Model Checking Software. LNCS, vol. 2057, pp. 16–36. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  5. CAV 2000.
    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. Choueka, Y.: Theories of automata on ω-tapes: A simplified approach. Journal of Computer and System Sciences 8, 117–141 (1974)zbMATHMathSciNetGoogle Scholar
  7. Easterbrook, S., Chechik, M.: A framework for multi-valued reasoning over inconsistent viewpoints. In: Proc. 23rd ICSE, pp. 411–420 (2001)Google Scholar
  8. CAV 1997.
    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)Google Scholar
  9. Hussain, A., Huth, M.: On model checking multiple hybrid views. Technical Report TR-2004-6, University of Cyprus (2004)Google Scholar
  10. IEEE standard multivalue logic system for VHDL model interoperability (std_logic_1164) (1993)Google Scholar
  11. Immerman, N.: Nondeterministic space is closed under complement. SIAM Journal on Computing 17, 935–938 (1988)zbMATHCrossRefMathSciNetGoogle Scholar
  12. Kuich, W., Salomaa, A.: Semirings, Automata, Languages. In: EATCS Monographs on Theoretical Computer Science, Springer, Heidelberg (1986)Google Scholar
  13. Kurshan, R.P.: Computer Aided Verification of Coordinating Processes. Princeton University Press, Princeton (1994)Google Scholar
  14. Kupferman, O., Vardi, M.Y.: Weak alternating automata are not that weak. ACM TOCL 2(2), 408–429 (2001)CrossRefMathSciNetzbMATHGoogle Scholar
  15. Kupferman, O., Vardi, M.Y., Wolper, P.: An automata-theoretic approach to branching-time model checking. Journal of the ACM 47(2), 312–360 (2000)CrossRefMathSciNetzbMATHGoogle Scholar
  16. Miyano, S., Hayashi, T.: Alternating finite automata on ω-words. Theoretical Computer Science 32, 321–330 (1984)zbMATHCrossRefMathSciNetGoogle Scholar
  17. Mohri, M.: Finite-state transducers in language and speech processing. Computational Linguistics 23(2), 269–311 (1997)MathSciNetGoogle Scholar
  18. Rabin, M.O., Scott, D.: Finite automata and their decision problems. IBM Journal of Research and Development 3, 115–125 (1959)MathSciNetCrossRefGoogle Scholar
  19. Safra, S.: On the complexity of ω-automata. In: Proc. 29th FOCS, pages 319–327 (1988)Google Scholar
  20. Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. Information and Computation 115(1), 1–37 (1994)zbMATHCrossRefMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2007

Authors and Affiliations

  • Orna Kupferman
    • 1
  • Yoad Lustig
    • 1
  1. 1.Hebrew University, School of Engineering and Computer Science, Jerusalem 91904Israel

Personalised recommendations