Automatic Generation of Quality Specifications
==============================================

The logic LTL[\U] extends LTL by quality operators. The satisfaction
value of an LTL[\U] formula in a computation refines the 0/1 value of
LTL formulas to a real value in [0,1].  The higher the value is, the
better is the quality of the computation. The quality operator
$\factor_\lambda$, for a quality constant $\lambda \in [0,1]$, enables
the designer to prioritize different satisfaction
possibilities. Formally, the satisfaction value of a sub-formula
$\factor_\lambda \varphi$ is $\lambda$ times the satisfaction value of
$\varphi$. For example, the LTL[\U] formula $G({\it req} \rightarrow
(X {\it grant} \vee \factor_{\frac{1}{2}} F{\it grant}))$ has value
$1$ in computations in which every request is immediately followed by
a grant, value $\frac{1}{2}$ if grants to some requests involve a
delay, and value $0$ if some request is not followed by a grant.

The design of an LTL[\U] formula typically starts with an LTL formula
on top of which the designer adds the parameterized $\factor$
operators.  In the Boolean setting, the problem of automatic
generation of specifications from binary-tagged computations is of
great importance and is a very challenging one.  Here we consider the
quantitative counterpart: an LTL[\U] query is an LTL[\U] formula in
which some of the quality constants are replaced by variables. Given
an LTL[\U] query and a set of computations tagged by satisfaction
values, the goal is to find an assignment to the variables in the
query so that the obtained LTL[\U] formula has the given satisfaction
values, or, if this is impossible, best approximates them. The
motivation to solving LTL[\U] queries is that in practice it is easier
for a designer to provide desired satisfaction values in
representative computations than to come up with quality constants
that capture his intuition of good and bad quality.

We study the problem of solving LTL[\U] queries and show that while
the problem is NP-hard, interesting fragments can be solved in
polynomial time. One such fragment is the case of a single tagged
computation, which we use for introducing a heuristic for the general
case. The polynomial solution is based on an analysis of the search
space, showing that reasoning about the infinitely many possible
assignments can proceed by reasoning about their partition into
finitely many classes. Our experimental results show the effectiveness
and favorable outcome of the heuristic.