MOVES Seminar/Informatik-Kolloquium, 6 April 2006
From Quality to Quantity: Quantative Logics and System relations for
quantitative transition systems
quantitative transition systems
Mariėlle Stoelinga
University Twente, NL
Many system models contain quantitative information, such as time,
probability, resource consumption, and continuous dynamics. Such
quantitative models are usually analyzed in a boolean fashion, answering
verification and refinement questions with a yes/no answer.
This boolean approach has two drawbacks.
* It lacks expressivity, as one cannot quantify to what extend a
property holds.
* It is fragile, since small pertubations in the system model may lead
to opposite truth values for a specification. This is a problem, since
the numbers appearing in the model are often an estimation, obtained by
measurements or learning, of the values in the physical system.
This talk presents a framework for quantative specification, model
checking and refinement. We consider quantitative transition systems
(QTSs), where predicates are assigned a real number in [0,1], rather than
a boolean value. We present system metrics (distance functions) for QTSs,
which are the quantitative analogi of refinement relations: rather than
tellingwhether one system correctly implements another one, metrics
measure how closely one matches the other. We also consider quantative
versions of LTL and CTL, called QLTL and QCTL respectively. In every
state, the value of a formula is a real number in the interval [0,1]. Then
we show that QLTL characterizes is characterized by our linear distance
and the QCTL by our branching distance. This generalizes the well-known
fact that trace equivalence is characterized by LTL and bisimulation by
CTL.
probability, resource consumption, and continuous dynamics. Such
quantitative models are usually analyzed in a boolean fashion, answering
verification and refinement questions with a yes/no answer.
This boolean approach has two drawbacks.
* It lacks expressivity, as one cannot quantify to what extend a
property holds.
* It is fragile, since small pertubations in the system model may lead
to opposite truth values for a specification. This is a problem, since
the numbers appearing in the model are often an estimation, obtained by
measurements or learning, of the values in the physical system.
This talk presents a framework for quantative specification, model
checking and refinement. We consider quantitative transition systems
(QTSs), where predicates are assigned a real number in [0,1], rather than
a boolean value. We present system metrics (distance functions) for QTSs,
which are the quantitative analogi of refinement relations: rather than
tellingwhether one system correctly implements another one, metrics
measure how closely one matches the other. We also consider quantative
versions of LTL and CTL, called QLTL and QCTL respectively. In every
state, the value of a formula is a real number in the interval [0,1]. Then
we show that QLTL characterizes is characterized by our linear distance
and the QCTL by our branching distance. This generalizes the well-known
fact that trace equivalence is characterized by LTL and bisimulation by
CTL.
