Search Results

Documents authored by Bernardi, Giovanni


Document
A Theory of (Linear-Time) Timed Monitors

Authors: Mouloud Amara, Giovanni Bernardi, Mohammed Aristide Foughali, and Adrian Francalanza

Published in: LIPIcs, Volume 333, 39th European Conference on Object-Oriented Programming (ECOOP 2025)


Abstract
Runtime Verification (RV) is gaining popularity due to its scalability and ability to analyse block-box systems. Monitoring is at the heart of RV; a logical formula ϕ, formalising some property of interest, is typically translated into a monitor that checks whether the system under scrutiny satisfies ϕ during its execution. A logical formula ϕ is violation (resp. satisfaction) monitorable iff there exists a monitor for ϕ that is both sound and complete w.r.t. its violation (resp. satisfaction). The monitorability problem is thus concerned with determining the largest subset of a logic L that is monitorable. Although this problem has been solved for expressive untimed logics, it remains open for timed logics, where formulae can express both the order of events and the quantity of time separating them. This paper solves the monitorability problem for T^lin, a new expressive (linear-time) timed μ-calculus that we propose. First, we show that T^lin is strictly more expressive than MTL, the de facto timed extension of LTL. Second, we identify MT^lin, the largest monitorable fragment of T^lin: we characterise its largest subsets of formulae that are violation monitorable, satisfaction monitorable, and complete monitorable (both satisfaction and violation monitorable). To wit, this is the first work that answers the monitorability question for such an expressive timed logic.

Cite as

Mouloud Amara, Giovanni Bernardi, Mohammed Aristide Foughali, and Adrian Francalanza. A Theory of (Linear-Time) Timed Monitors. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 1:1-1:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)


Copy BibTex To Clipboard

@InProceedings{amara_et_al:LIPIcs.ECOOP.2025.1,
  author =	{Amara, Mouloud and Bernardi, Giovanni and Foughali, Mohammed Aristide and Francalanza, Adrian},
  title =	{{A Theory of (Linear-Time) Timed Monitors}},
  booktitle =	{39th European Conference on Object-Oriented Programming (ECOOP 2025)},
  pages =	{1:1--1:30},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-373-7},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{333},
  editor =	{Aldrich, Jonathan and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2025.1},
  URN =		{urn:nbn:de:0030-drops-232930},
  doi =		{10.4230/LIPIcs.ECOOP.2025.1},
  annote =	{Keywords: Timed logics, Runtime Verification, Monitorability}
}
Document
Artifact
A Theory of (Linear-Time) Timed Monitors (Artifact)

Authors: Mouloud Amara, Giovanni Bernardi, Mohammed Aristide Foughali, and Adrian Francalanza

Published in: DARTS, Volume 11, Issue 2, Special Issue of the 39th European Conference on Object-Oriented Programming (ECOOP 2025)


Abstract
We provide an OCaml implementation of the logics MTL and T^lin, as well as monitors. Our artefact includes a compiler that translates T^lin formulae into monitors. The generation of a monitor M from some formula ϕ is decorated with a warning whenever ϕ is not in the syntax of the maximally-expressive monitorable fragment. The resulting monitors being reactive and deterministic, we also implement their semantics, and provide further a pseudo-monitoring prototype where the monitor incrementally consumes an infinite timed word and reaches a verdict whenever possible. For convenience, for users that prefer to use MTL (bearing in mind the loss of expressivity), we also provide a compiler from MTL to T^lin.

Cite as

Mouloud Amara, Giovanni Bernardi, Mohammed Aristide Foughali, and Adrian Francalanza. A Theory of (Linear-Time) Timed Monitors (Artifact). In Special Issue of the 39th European Conference on Object-Oriented Programming (ECOOP 2025). Dagstuhl Artifacts Series (DARTS), Volume 11, Issue 2, pp. 8:1-8:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)


Copy BibTex To Clipboard

@Article{amara_et_al:DARTS.11.2.8,
  author =	{Amara, Mouloud and Bernardi, Giovanni and Foughali, Mohammed Aristide and Francalanza, Adrian},
  title =	{{A Theory of (Linear-Time) Timed Monitors (Artifact)}},
  pages =	{8:1--8:3},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2025},
  volume =	{11},
  number =	{2},
  editor =	{Amara, Mouloud and Bernardi, Giovanni and Foughali, Mohammed Aristide and Francalanza, Adrian},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.11.2.8},
  URN =		{urn:nbn:de:0030-drops-233517},
  doi =		{10.4230/DARTS.11.2.8},
  annote =	{Keywords: Timed logics, Runtime verification, Monitorability}
}
Document
Robustness against Consistency Models with Atomic Visibility

Authors: Giovanni Bernardi and Alexey Gotsman

Published in: LIPIcs, Volume 59, 27th International Conference on Concurrency Theory (CONCUR 2016)


Abstract
To achieve scalability, modern Internet services often rely on distributed databases with consistency models for transactions weaker than serializability. At present, application programmers often lack techniques to ensure that the weakness of these consistency models does not violate application correctness. We present criteria to check whether applications that rely on a database providing only weak consistency are robust, i.e., behave as if they used a database providing serializability. When this is the case, the application programmer can reap the scalability benefits of weak consistency while being able to easily check the desired correctness properties. Our results handle systematically and uniformly several recently proposed weak consistency models, as well as a mechanism for strengthening consistency in parts of an application.

Cite as

Giovanni Bernardi and Alexey Gotsman. Robustness against Consistency Models with Atomic Visibility. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 7:1-7:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@InProceedings{bernardi_et_al:LIPIcs.CONCUR.2016.7,
  author =	{Bernardi, Giovanni and Gotsman, Alexey},
  title =	{{Robustness against Consistency Models with Atomic Visibility}},
  booktitle =	{27th International Conference on Concurrency Theory (CONCUR 2016)},
  pages =	{7:1--7:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-017-0},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{59},
  editor =	{Desharnais, Jos\'{e}e and Jagadeesan, Radha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2016.7},
  URN =		{urn:nbn:de:0030-drops-61652},
  doi =		{10.4230/LIPIcs.CONCUR.2016.7},
  annote =	{Keywords: Robustness, Replication, Consistency models, Transactions}
}
Document
A Framework for Transactional Consistency Models with Atomic Visibility

Authors: Andrea Cerone, Giovanni Bernardi, and Alexey Gotsman

Published in: LIPIcs, Volume 42, 26th International Conference on Concurrency Theory (CONCUR 2015)


Abstract
Modern distributed systems often rely on databases that achieve scalability by providing only weak guarantees about the consistency of distributed transaction processing. The semantics of programs interacting with such a database depends on its consistency model, defining these guarantees. Unfortunately, consistency models are usually stated informally or using disparate formalisms, often tied to the database internals. To deal with this problem, we propose a framework for specifying a variety of consistency models for transactions uniformly and declaratively. Our specifications are given in the style of weak memory models, using structures of events and relations on them. The specifications are particularly concise because they exploit the property of atomic visibility guaranteed by many consistency models: either all or none of the updates by a transaction can be visible to another one. This allows the specifications to abstract from individual events inside transactions. We illustrate the use of our framework by specifying several existing consistency models. To validate our specifications, we prove that they are equivalent to alternative operational ones, given as algorithms closer to actual implementations. Our work provides a rigorous foundation for developing the metatheory of the novel form of concurrency arising in weakly consistent large-scale databases.

Cite as

Andrea Cerone, Giovanni Bernardi, and Alexey Gotsman. A Framework for Transactional Consistency Models with Atomic Visibility. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 58-71, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)


Copy BibTex To Clipboard

@InProceedings{cerone_et_al:LIPIcs.CONCUR.2015.58,
  author =	{Cerone, Andrea and Bernardi, Giovanni and Gotsman, Alexey},
  title =	{{A Framework for Transactional Consistency Models with Atomic Visibility}},
  booktitle =	{26th International Conference on Concurrency Theory (CONCUR 2015)},
  pages =	{58--71},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-91-0},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{42},
  editor =	{Aceto, Luca and de Frutos Escrig, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2015.58},
  URN =		{urn:nbn:de:0030-drops-53756},
  doi =		{10.4230/LIPIcs.CONCUR.2015.58},
  annote =	{Keywords: Replication, Consistency models, Transactions}
}
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