BEGIN:VCALENDAR
VERSION:2.0
PRODID:icalendar-ruby
CALSCALE:GREGORIAN
METHOD:PUBLISH
BEGIN:VTIMEZONE
TZID:Europe/Vienna
BEGIN:DAYLIGHT
DTSTART:20250330T030000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
RRULE:FREQ=YEARLY;BYDAY=-1SU;BYMONTH=3
TZNAME:CEST
END:DAYLIGHT
BEGIN:STANDARD
DTSTART:20251026T020000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
RRULE:FREQ=YEARLY;BYDAY=-1SU;BYMONTH=10
TZNAME:CET
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
DTSTAMP:20260424T143355Z
UID:1749625200@ist.ac.at
DTSTART:20250611T090000
DTEND:20250611T100000
DESCRIPTION:Speaker: N. Ege Saraç\nhosted by Beatriz Vicoso\nAbstract: Qua
 ntitative 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 r
 equest it receives\, a quantitative one may map each server execution to i
 ts average response time. This quantitative view is relatively well-studie
 d in the context of static verification. However\, although such propertie
 s often appear in practice as performance or robustness measures in a dyna
 mic verification context\, a general theoretical framework for their analy
 sis and classification from a monitoring perspective is still missing.In t
 his thesis\, we aim to develop such a framework that takes resource-precis
 ion tradeoffs of monitors as a central consideration. We present the first
  theory of monitorability for quantitative properties where monitors can b
 e naturally approximate and compared regarding their precision and resourc
 e use. In particular\, we show that additional monitor resources such as r
 egisters or states lead to strictly better approximations for some propert
 ies. To enable such analyses in a machine-model independent way\, we descr
 ibe 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 monitor
 ing with resource-precision considerations. We then extend the boolean saf
 ety-liveness dichotomy and safety-progress hierarchy to the quantitative s
 etting with a monitoring perspective. In particular\, we prove that every 
 property is the pointwise minimum of a safety property and a liveness prop
 erty\, and properties that are both safe and co-safe can be approximately 
 monitored arbitrarily precisely using only finitely many states. We also s
 tudy the classes of quantitative properties definable by finite-state quan
 titative automata and provide algorithms for deciding their safety or live
 ness 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.
LOCATION:Central Bldg / O1 / Mondi 2a (I01.O1.008) and Zoom\, ISTA
ORGANIZER:
SUMMARY:N. Ege Saraç: Thesis Defense: A Monitoring-Oriented Theory and Cla
 ssification of Quantitative Specifications 
URL:https://talks-calendar.ista.ac.at/events/5680
END:VEVENT
END:VCALENDAR