---
res:
  bibo_abstract:
  - 'Traditional formal methods are based on a Boolean satisfaction notion: a reactive
    system satisfies, or not, a given specification. We generalize formal methods
    to also address the quality of systems. As an adequate specification formalism
    we introduce the linear temporal logic LTL[F]. The satisfaction value of an LTL[F]
    formula is a number between 0 and 1, describing the quality of the satisfaction.
    The logic generalizes traditional LTL by augmenting it with a (parameterized)
    set F of arbitrary functions over the interval [0,1]. For example, F may contain
    the maximum or minimum between the satisfaction values of subformulas, their product,
    and their average. The classical decision problems in formal methods, such as
    satisfiability, model checking, and synthesis, are generalized to search and optimization
    problems in the quantitative setting. For example, model checking asks for the
    quality in which a specification is satisfied, and synthesis returns a system
    satisfying the specification with the highest quality. Reasoning about quality
    gives rise to other natural questions, like the distance between specifications.
    We formalize these basic questions and study them for LTL[F]. By extending the
    automata-theoretic approach for LTL to a setting that takes quality into an account,
    we are able to solve the above problems and show that reasoning about LTL[F] has
    roughly the same complexity as reasoning about traditional LTL.@eng'
  bibo_authorlist:
  - foaf_Person:
      foaf_givenName: Shaull
      foaf_name: Almagor, Shaull
      foaf_surname: Almagor
  - foaf_Person:
      foaf_givenName: Udi
      foaf_name: Boker, Udi
      foaf_surname: Boker
      foaf_workInfoHomepage: http://www.librecat.org/personId=31E297B6-F248-11E8-B48F-1D18A9856A87
  - foaf_Person:
      foaf_givenName: Orna
      foaf_name: Kupferman, Orna
      foaf_surname: Kupferman
  bibo_doi: 10.1007/978-3-642-39212-2_3
  bibo_issue: Part 2
  bibo_volume: 7966
  dct_date: 2013^xs_gYear
  dct_language: eng
  dct_publisher: Springer@
  dct_title: Formalizing and reasoning about quality@
...