  A large number of different model checking approaches has been proposed
during the last decade. The different approaches are applicable to different
model types including untimed, timed, probabilistic and stochastic models. This
paper presents a new framework for model checking techniques which includes
some of the known approaches, but enlarges the class of models for which model
checking can be applied to the general class of weighted automata. The approach
allows an easy adaption of model checking to models which have not been
considered yet for this purpose. Examples for those new model types for which
model checking can be applied are max/plus or min/plus automata which are well
established models to describe different forms of dynamic systems and
optimization problems. In this context, model checking can be used to verify
temporal or quantitative properties of a system. The paper first presents
briefly our class of weighted automata, as a very general model type. Then
Valued Computational Tree Logic (CTL$) is introduced as a natural extension of
the well known branching time logic CTL. Afterwards, algorithms to check a
weighted automaton according to a CTL$ formula are presented. As a last result,
a bisimulation is presented for weighted automata and for CTL$.
