2 Search Results for "Ferrère, Thomas"

Document
DOI: 10.4230/LIPIcs.FSTTCS.2025.20
Flavors of Quantifiers in Hyperlogics

Authors: Marek Chalupa, Thomas A. Henzinger, and Ana Oliveira da Costa

Published in: LIPIcs, Volume 360, 45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025)

Abstract
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 traces. In this work, we extend hypertrace logic by introducing trace quantifiers that range over the set of all possible traces. In this extended logic, formulas can quantify over two kinds of trace variables: constrained trace variables, which range over a fixed set of traces defined by the model, and unconstrained trace variables, which can be assigned to any trace. In comparison, hyperlogics such as HyperLTL have only constrained trace quantifiers. We use hypertrace logic to study how different quantifier patterns affect the decidability of the satisfiability problem. We prove that hypertrace logic without constrained trace quantifiers is equivalent to monadic second-order logic of one successor (S1S), and therefore satisfiable, and that the trace-prefixed fragment (all trace quantifiers precede all time quantifiers) is equivalent to HyperQPTL. Moreover, we show that all hypertrace formulas where the only alternation between constrained trace quantifiers is from an existential to a universal quantifier are equisatisfiable to formulas without constraints on their trace variables and, therefore, decidable as well. Our framework allows us to study also time-prefixed hyperlogics, for which we provide new decidability and undecidability results.
Cite as

Marek Chalupa, Thomas A. Henzinger, and Ana Oliveira da Costa. Flavors of Quantifiers in Hyperlogics. In 45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 360, pp. 20:1-20:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{chalupa_et_al:LIPIcs.FSTTCS.2025.20,
  author =	{Chalupa, Marek and Henzinger, Thomas A. and Oliveira da Costa, Ana},
  title =	{{Flavors of Quantifiers in Hyperlogics}},
  booktitle =	{45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025)},
  pages =	{20:1--20:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-406-2},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{360},
  editor =	{Aiswarya, C. and Mehta, Ruta and Roy, Subhajit},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2025.20},
  URN =		{urn:nbn:de:0030-drops-251016},
  doi =		{10.4230/LIPIcs.FSTTCS.2025.20},
  annote =	{Keywords: Hyperproperties, Satisfiability, First-order Logic, S1S}
}
Document
DOI: 10.4230/LIPIcs.CSL.2020.20
Monitoring Event Frequencies

Authors: Thomas Ferrère, Thomas A. Henzinger, and Bernhard Kragl

Published in: LIPIcs, Volume 152, 28th EACSL Annual Conference on Computer Science Logic (CSL 2020)

Abstract
The monitoring of event frequencies can be used to recognize behavioral anomalies, to identify trends, and to deduce or discard hypotheses about the underlying system. For example, the performance of a web server may be monitored based on the ratio of the total count of requests from the least and most active clients. Exact frequency monitoring, however, can be prohibitively expensive; in the above example it would require as many counters as there are clients. In this paper, we propose the efficient probabilistic monitoring of common frequency properties, including the mode (i.e., the most common event) and the median of an event sequence. We define a logic to express composite frequency properties as a combination of atomic frequency properties. Our main contribution is an algorithm that, under suitable probabilistic assumptions, can be used to monitor these important frequency properties with four counters, independent of the number of different events. Our algorithm samples longer and longer subwords of an infinite event sequence. We prove the almost-sure convergence of our algorithm by generalizing ergodic theory from increasing-length prefixes to increasing-length subwords of an infinite sequence. A similar algorithm could be used to learn a connected Markov chain of a given structure from observing its outputs, to arbitrary precision, for a given confidence.
Cite as

Thomas Ferrère, Thomas A. Henzinger, and Bernhard Kragl. Monitoring Event Frequencies. In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 20:1-20:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{ferrere_et_al:LIPIcs.CSL.2020.20,
  author =	{Ferr\`{e}re, Thomas and Henzinger, Thomas A. and Kragl, Bernhard},
  title =	{{Monitoring Event Frequencies}},
  booktitle =	{28th EACSL Annual Conference on Computer Science Logic (CSL 2020)},
  pages =	{20:1--20:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-132-0},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{152},
  editor =	{Fern\'{a}ndez, Maribel and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2020.20},
  URN =		{urn:nbn:de:0030-drops-116633},
  doi =		{10.4230/LIPIcs.CSL.2020.20},
  annote =	{Keywords: monitoring, frequency property, Markov chain}
}
  • Refine by Type
  • 2 Document/PDF
  • 1 Document/HTML

  • Refine by Publication Year
  • 1 2025
  • 1 2020

  • Refine by Author
  • 2 Henzinger, Thomas A.
  • 1 Chalupa, Marek
  • 1 Ferrère, Thomas
  • 1 Kragl, Bernhard
  • 1 Oliveira da Costa, Ana

  • Refine by Series/Journal
  • 2 LIPIcs

  • Refine by Classification
  • 1 Software and its engineering → Software organization and properties
  • 1 Theory of computation → Logic and verification
  • 1 Theory of computation → Randomness, geometry and discrete structures

  • Refine by Keyword
  • 1 First-order Logic
  • 1 Hyperproperties
  • 1 Markov chain
  • 1 S1S
  • 1 Satisfiability
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact