Verifying Quantitative Properties Using Bound Functions
=======================================================

Formal methods are successfully used for the verification of
finite-state systems defined with respect to a finite set of atomic
propositions.  We study {\em quanitative verification}, where each
state in the finite-state system is labeled by an integer, or a finite
vector of integers, and the properties are quantitaive, rather than
Boolean.  We describe extensions of formalisms used in standard
verification to the quantitative setting: quantitative automata on
finite and infinite words (standard automata map words to
accept/reject; quantitative automata map words to integers), and a
quantitative calculus (standard $\mu$-calculus formulas correspond to
Boolean predicates; quantitative calculus formulas correspond to
functions from the state space to integers). Both formalisms extend
the standard one by maintaining a set of registers whose values can be
tested and updated.  We study properties of the new formalisms: their
expressive power, and the relation between the linear (automata) and
branching (calculus) formalisms. We define and solve the quantitaive
model-checking and game problems, which correspond to verification of
closed and open systems. While the general setting is undecidable, we
obtain decidability by taking into an account the fact that the
quantitative properties refer to finite-state systems. For example,
our verification algorithms can calculate the maximal distance
(possibly infinity) between a request and a grant, or the maximal
integer that the system may reach no matter how the environment
behaves.