---
res:
  bibo_abstract:
  - "Quantitative properties offer a framework for specifying and verifying system
    behaviors beyond the traditional boolean perspective. For example, while a boolean
    property may specify whether a server eventually grants every request it receives,
    a quantitative one may map each server execution to its average response time.
    This quantitative view is relatively well-studied in the context of static verification.
    However, although such properties often appear in practice as performance or robustness
    measures in a dynamic verification context, a general theoretical framework for
    their analysis and classification from a monitoring perspective is still missing.\r\n\r\nIn
    this thesis, we aim to develop such a framework that takes resource-precision
    tradeoffs of monitors as a central consideration. We present the first theory
    of monitorability for quantitative properties where monitors can be naturally
    approximate and compared regarding their precision and resource use. In particular,
    we show that additional monitor resources such as registers or states lead to
    strictly better approximations for some properties. To enable such analyses in
    a machine-model independent way, we describe an abstract notion of monitors that
    can be instantiated with concrete models of monitors. Within this framework, we
    study how abstract monitors behave and identify classes of properties amenable
    to approximate monitoring with resource-precision considerations. We then extend
    the boolean safety-liveness dichotomy and safety-progress hierarchy to the quantitative
    setting with a monitoring perspective. In particular, we prove that every property
    is the pointwise minimum of a safety property and a liveness property, and properties
    that are both safe and co-safe can be approximately monitored arbitrarily precisely
    using only finitely many states. We also study the classes of quantitative properties
    definable by finite-state quantitative automata and provide algorithms for deciding
    their safety or liveness as well as their safety-liveness decompositions. Finally,
    we present the first general-purpose tool for automating the analysis, verification,
    and monitoring of quantitative automata.\r\n\r\n\r\n@eng"
  bibo_authorlist:
  - foaf_Person:
      foaf_givenName: Naci E
      foaf_name: Sarac, Naci E
      foaf_surname: Sarac
      foaf_workInfoHomepage: http://www.librecat.org/personId=8C6B42F8-C8E6-11E9-A03A-F2DCE5697425
  bibo_doi: 10.15479/AT-ISTA-20147
  dct_date: 2025^xs_gYear
  dct_isPartOf:
  - http://id.crossref.org/issn/2663-337X
  dct_language: eng
  dct_publisher: Institute of Science and Technology Austria@
  dct_title: A monitoring-oriented theory and classification of quantitative specifications@
...