Formal Specification of Performance Metrics for Intelligent Systems

SYSTEM VERIFICATION
For most dynamic systems, stability or convergence is the
most important property that needs to be verified. For
example, we can verify that equation dx/dt = 0 satisfies the
property of "-automaton in Figure 1(a) with G as |x|£e for
any positive number e. The most commonly used method
for the verification of such properties is the use of
Liaponov functions. We developed a formal method based
on model-checking, that generalizes Liaponov functions
[13,17]. This method is automatic if the domain of interest
is finite discrete and time is discrete [13].

The details of the model-checking method are out of
the scope of this paper. The basic principle is to first find a
set of invariants, each associated with an automaton-state
in the timed "-automaton. Then, find a set of Liaponov
functions, which are non-increasing in stable states and
decreasing in bad states. Finally, find a set of local and
global timing functions, where local timing functions are
decreasing in timed states and global timing functions, like
Liaponov functions, are non-increasing in stable states and
decreasing in bad states, in addition to be bounded in
values.