---
OA_place: publisher
_id: '20147'
abstract:
- lang: eng
  text: "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"
acknowledgement: "This work was supported in part by the Austrian Science Fund (FWF)\r\nunder
  grant Z211-N23 (Wittgenstein Award) and the ERC-2020-AdG 101020093.\r\n"
alternative_title:
- ISTA Thesis
article_processing_charge: No
author:
- first_name: Naci E
  full_name: Sarac, Naci E
  id: 8C6B42F8-C8E6-11E9-A03A-F2DCE5697425
  last_name: Sarac
citation:
  ama: Sarac NE. A monitoring-oriented theory and classification of quantitative specifications.
    2025. doi:<a href="https://doi.org/10.15479/AT-ISTA-20147">10.15479/AT-ISTA-20147</a>
  apa: Sarac, N. E. (2025). <i>A monitoring-oriented theory and classification of
    quantitative specifications</i>. Institute of Science and Technology Austria.
    <a href="https://doi.org/10.15479/AT-ISTA-20147">https://doi.org/10.15479/AT-ISTA-20147</a>
  chicago: Sarac, Naci E. “A Monitoring-Oriented Theory and Classification of Quantitative
    Specifications.” Institute of Science and Technology Austria, 2025. <a href="https://doi.org/10.15479/AT-ISTA-20147">https://doi.org/10.15479/AT-ISTA-20147</a>.
  ieee: N. E. Sarac, “A monitoring-oriented theory and classification of quantitative
    specifications,” Institute of Science and Technology Austria, 2025.
  ista: Sarac NE. 2025. A monitoring-oriented theory and classification of quantitative
    specifications. Institute of Science and Technology Austria.
  mla: Sarac, Naci E. <i>A Monitoring-Oriented Theory and Classification of Quantitative
    Specifications</i>. Institute of Science and Technology Austria, 2025, doi:<a
    href="https://doi.org/10.15479/AT-ISTA-20147">10.15479/AT-ISTA-20147</a>.
  short: N.E. Sarac, A Monitoring-Oriented Theory and Classification of Quantitative
    Specifications, Institute of Science and Technology Austria, 2025.
corr_author: '1'
date_created: 2025-08-07T15:57:57Z
date_published: 2025-08-07T00:00:00Z
date_updated: 2026-08-12T08:46:04Z
day: '07'
ddc:
- '000'
degree_awarded: PhD
department:
- _id: GradSch
- _id: ToHe
doi: 10.15479/AT-ISTA-20147
doi_confirm: '1'
ec_funded: 1
file:
- access_level: closed
  checksum: 0f3015f1db36576a23d8d669afb60b41
  content_type: application/x-zip-compressed
  creator: esarac
  date_created: 2025-08-21T09:40:28Z
  date_updated: 2025-09-10T08:19:51Z
  file_id: '20200'
  file_name: 2025_Sarac_NaciEge_Thesis.zip
  file_size: 8884801
  relation: source_file
- access_level: open_access
  checksum: 332ed2fe61f580641664ec3f05d30f14
  content_type: application/pdf
  creator: esarac
  date_created: 2025-08-21T09:40:34Z
  date_updated: 2025-08-21T09:40:34Z
  file_id: '20201'
  file_name: 2025_Sarac_NaciEge_Thesis.pdf
  file_size: 2955584
  relation: main_file
  success: 1
file_date_updated: 2025-09-10T08:19:51Z
has_accepted_license: '1'
language:
- iso: eng
month: '08'
oa: 1
oa_version: Published Version
page: '149'
project:
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: Z211
  name: Formal methods for the design and analysis of complex systems
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
  call_identifier: H2020
  grant_number: '101020093'
  name: Vigilant Algorithmic Monitoring of Software
publication_identifier:
  issn:
  - 2663-337X
publication_status: published
publisher: Institute of Science and Technology Austria
publisher_comment: "In reference to IEEE copyrighted material which is used with permission
  in this thesis, the IEEE does not\r\nendorse any of ISTA's products or services.
  Internal or personal use of this\r\nmaterial is permitted. If interested in reprinting/republishing
  IEEE copyrighted material for advertising or promotional\r\npurposes or for creating
  new collective works for resale or redistribution, please go to\r\nhttp://www.ieee.org/publications_standards/publications/rights/rights_link.html
  to learn how to obtain a License from\r\nRightsLink.  If applicable, University
  Microfilms and/or ProQuest Library, or the Archives of Canada may supply single
  copies of the dissertation."
related_material:
  record:
  - id: '11775'
    relation: part_of_dissertation
    status: public
  - id: '13140'
    relation: part_of_dissertation
    status: deleted
  - id: '19741'
    relation: part_of_dissertation
    status: public
  - id: '19643'
    relation: part_of_dissertation
    status: deleted
  - id: '17634'
    relation: part_of_dissertation
    status: public
  - id: '13221'
    relation: part_of_dissertation
    status: public
  - id: '9356'
    relation: part_of_dissertation
    status: public
  - id: '20342'
    relation: part_of_dissertation
    status: public
status: public
supervisor:
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000-0002-2985-7724
title: A monitoring-oriented theory and classification of quantitative specifications
tmp:
  image: /images/cc_by.png
  legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
  name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
  short: CC BY (4.0)
type: dissertation
user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9
year: '2025'
...