5 papers
Quantitative Monitoring of Signal First-Order Logic
Marek Chalupa, Thomas A. Henzinger, N. Ege Saraç +1
Runtime monitoring checks, during execution, whether a partial signal produced by a hybrid system satisfies its specification. Signal First-Order Logic (SFO) offers expressive real…
Flavors of Quantifiers in Hyperlogics
Marek Chalupa, Thomas A. Henzinger, Ana Oliveira da Costa
Hypertrace logic is a sorted first-order logic with separate sorts for time and execution traces. Its formulas specify hyperproperties, which are properties relating multiple trace…
Monitoring Hyperproperties over Observed and Constructed Traces
Marek Chalupa, Thomas A. Henzinger, Ana Oliveira da Costa
We study the problem of monitoring at runtime whether a system fulfills a specification defined by a hyperproperty, such as linearizability or variants of non-interference. For thi…
QuAK: Quantitative Automata Kit
Marek Chalupa, Thomas A. Henzinger, Nicolas Mazzocchi +1
System behaviors are traditionally evaluated through binary classifications of correctness, which do not suffice for properties involving quantitative aspects of systems and execut…
Automating the Analysis of Quantitative Automata with QuAK
Marek Chalupa, Thomas A. Henzinger, Nicolas Mazzocchi +1
Quantitative automata model beyond-boolean aspects of systems: every execution is mapped to a real number by incorporating weighted transitions and value functions that generalize…