Formal Specification of Performance Metrics for Intelligent Systems

Keywords Formal Specification of Performance Metrics for Intelligent Systems formal specification constraint-based requirements system verification
Standards groups

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

Date published
Document type
technical white paper
Defines standard
Replaced/Superseded by document(s)
Cancelled by
Amended by
File MIME type Size (KB) Language Download
Paper WPMIS00.pdf application/pdf   38.64 KB English DOWNLOAD!
File attachments

There are now so many architectures for intelligent systems:
deliberative planning vs. reactive acting, behavioral subsuming
vs. hierarchical structuring, machine learning vs. logic reasoning,
and symbolic representation vs. procedural knowledge. The
arguments from all schools are all based on how natural systems
(i.e., biologically inspired, from basic forms of life to high level
intelligence) work by taking the parts that support their
architectures. In this paper, we take an engineering point of view,
i.e., by using requirements specification and system verification
as the measurement tool. Since most intelligent systems are real time dynamic systems (all lives are), requirements specification
should be able to represent timed properties. We have developed
timed "-automata that fit to this purpose. We will present this
formal specification, examples for specifying requirements and a
general procedure for verification.

Visit also