Lattice Automata

Abstract. 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 ...

• Type: Conference
• Year: 2007
• Where: VMCAI
• Authors: Orna Kupferman, Yoad Lustig
• Keywords: Lattice Automata, Lattice Automata Exhibit, Lattice Element, Software Engineering, VMCAI 2007