Sciweavers

VMCAI
2007
Springer

Lattice Automata

14 years 4 months ago
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 ...
Orna Kupferman, Yoad Lustig
Added 09 Jun 2010
Updated 09 Jun 2010
Type Conference
Year 2007
Where VMCAI
Authors Orna Kupferman, Yoad Lustig
Comments (0)