We introduce the lattice-valued Kripke structures, for the purpose of allowing imprecise or incomplete specifications to be expressed, by extending the traditional notion of Kripke structures in the context of complete residuated lattice. Moreover, we show how the traditional trace inclusion and equivalence, can be lifted to a setting of quantitative where their interpretations are given as elements of complete residuated lattices. We also present logical characterizations of our notions, given by a lattice-valued extension of LTL.