11 Search Results for "Zălinescu, Eugen"

Document
DOI: 10.4230/LIPIcs.CONCUR.2025.4
Monitorability for the Modal Mu-Calculus over Systems with Data: From Practice to Theory

Authors: Luca Aceto, Antonis Achilleos, Duncan Paul Attard, Léo Exibard, Adrian Francalanza, Anna Ingólfsdóttir, and Karoliina Lehtinen

Published in: LIPIcs, Volume 348, 36th International Conference on Concurrency Theory (CONCUR 2025)

Abstract
Runtime verification consists in checking whether a system satisfies a given specification by observing the execution trace it produces. In the regular setting, the modal μ-calculus provides a versatile formalism for expressing specifications of the control flow of the system. This paper focuses on the data flow and studies an extension of that logic that allows it to express data-dependent properties, identifying fragments that can be verified at runtime and with what correctness guarantees. The logic studied here is closely related with register automata with guessing. That correspondence yields a monitor synthesis algorithm, and a strict hierarchy among the various fragments of the logic, in contrast to the regular setting. We then exhibit a fragment of the logic that can express all monitorable formulae in the logic without greatest fixed-points but not in the full logic, and show this is the best we can get.
Cite as

Luca Aceto, Antonis Achilleos, Duncan Paul Attard, Léo Exibard, Adrian Francalanza, Anna Ingólfsdóttir, and Karoliina Lehtinen. Monitorability for the Modal Mu-Calculus over Systems with Data: From Practice to Theory. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 4:1-4:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{aceto_et_al:LIPIcs.CONCUR.2025.4,
  author =	{Aceto, Luca and Achilleos, Antonis and Attard, Duncan Paul and Exibard, L\'{e}o and Francalanza, Adrian and Ing\'{o}lfsd\'{o}ttir, Anna and Lehtinen, Karoliina},
  title =	{{Monitorability for the Modal Mu-Calculus over Systems with Data: From Practice to Theory}},
  booktitle =	{36th International Conference on Concurrency Theory (CONCUR 2025)},
  pages =	{4:1--4:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-389-8},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{348},
  editor =	{Bouyer, Patricia and van de Pol, Jaco},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.4},
  URN =		{urn:nbn:de:0030-drops-239546},
  doi =		{10.4230/LIPIcs.CONCUR.2025.4},
  annote =	{Keywords: Runtime verification, monitorability, \muHML with data, register automata}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2025.19
Time for Timed Monitorability

Authors: Thomas M. Grosen, Sean Kauffman, Kim G. Larsen, and Martin Zimmermann

Published in: LIPIcs, Volume 348, 36th International Conference on Concurrency Theory (CONCUR 2025)

Abstract
Monitoring is an important part of the verification toolbox, in particular in situations where exhaustive verification using, e.g., model-checking is infeasible. The goal of online monitoring is to determine the satisfaction or violation of a specification during runtime, i.e., based on finite execution prefixes. However, not every specification is amenable to monitoring, e.g., properties for which no finite execution can witness satisfaction or violation. Monitorability is the question of whether a given specification is amenable to monitoring, and has been extensively studied in discrete time. Here, we study the monitorability problem for real-time properties expressed as Timed Automata. For specifications given by deterministic Timed Muller Automata, we prove decidability while we show that the problem is undecidable for specifications given by nondeterministic Timed Büchi automata. Furthermore, we refine monitorability to also determine bounds on the number of events as well as the time that must pass before monitoring the property may yield an informative verdict. We prove that for deterministic Timed Muller automata, such bounds can be effectively computed. In contrast we show that for nondeterministic Timed Büchi automata such bounds are not computable.
Cite as

Thomas M. Grosen, Sean Kauffman, Kim G. Larsen, and Martin Zimmermann. Time for Timed Monitorability. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 19:1-19:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{grosen_et_al:LIPIcs.CONCUR.2025.19,
  author =	{Grosen, Thomas M. and Kauffman, Sean and Larsen, Kim G. and Zimmermann, Martin},
  title =	{{Time for Timed Monitorability}},
  booktitle =	{36th International Conference on Concurrency Theory (CONCUR 2025)},
  pages =	{19:1--19:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-389-8},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{348},
  editor =	{Bouyer, Patricia and van de Pol, Jaco},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.19},
  URN =		{urn:nbn:de:0030-drops-239690},
  doi =		{10.4230/LIPIcs.CONCUR.2025.19},
  annote =	{Keywords: Monitorability, Monitoring, Timed Automata, MITL}
}
Document
Pearl/Brave New Idea
DOI: 10.4230/LIPIcs.ECOOP.2025.42
Contract Systems Need Domain-Specific Notations (Pearl/Brave New Idea)

Authors: Cameron Moy, Ryan Jung, and Matthias Felleisen

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

Abstract
Contract systems enable programmers to state specifications and have them enforced at run time. First-order contracts are expressed using ordinary code, while higher-order contracts are expressed using the notation familiar from type systems. Most interface descriptions, though, come with properties that involve not just assertions about single method calls, but entire call chains. Typical contract systems cannot express these specifications concisely. Such specifications demand domain-specific notations. In response, this paper proposes that contract systems abstract over the notation used for stating specifications. It presents an architecture for such a system, some illustrative examples, and an evaluation in terms of common notations from the literature.
Cite as

Cameron Moy, Ryan Jung, and Matthias Felleisen. Contract Systems Need Domain-Specific Notations (Pearl/Brave New Idea). In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 42:1-42:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{moy_et_al:LIPIcs.ECOOP.2025.42,
  author =	{Moy, Cameron and Jung, Ryan and Felleisen, Matthias},
  title =	{{Contract Systems Need Domain-Specific Notations}},
  booktitle =	{39th European Conference on Object-Oriented Programming (ECOOP 2025)},
  pages =	{42:1--42:24},
  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.42},
  URN =		{urn:nbn:de:0030-drops-233348},
  doi =		{10.4230/LIPIcs.ECOOP.2025.42},
  annote =	{Keywords: software contracts, domain-specific languages}
}
Document
DOI: 10.4230/LIPIcs.OPODIS.2024.7
Incentive Compatibility of Ethereum’s PoS Consensus Protocol

Authors: Ulysse Pavloff, Yackolley Amoussou-Guenou, and Sara Tucci-Piergiovanni

Published in: LIPIcs, Volume 324, 28th International Conference on Principles of Distributed Systems (OPODIS 2024)

Abstract
This paper investigates whether following the fork-choice rule in the Ethereum PoS consensus protocol constitutes a Nash equilibrium - i.e., whether the protocol that maintains the canonical chain in Ethereum is incentive-compatible. Specifically, we explore whether selfish participants may attempt to manipulate the fork-choice rule by forking out previous blocks and capturing the rewards associated with those blocks. Our analysis considers two strategies for participants: the obedient strategy, which adheres to the prescribed protocol, and the cunning strategy, which attempts to manipulate the fork-choice rule to gain more rewards. We evaluate the conditions under which selfish participants might deviate from the obedient strategy. We found that, in a synchronous system, following the prescribed fork-choice rule is incentive-compatible. However, in an eventually synchronous system, the protocol is eventually incentive-compatible - that is, only a limited number of proposers will find it profitable to fork the chain during the synchronous period. After this sequence of cunning proposers, subsequent proposers will find it more profitable to follow the protocol.
Cite as

Ulysse Pavloff, Yackolley Amoussou-Guenou, and Sara Tucci-Piergiovanni. Incentive Compatibility of Ethereum’s PoS Consensus Protocol. In 28th International Conference on Principles of Distributed Systems (OPODIS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 324, pp. 7:1-7:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{pavloff_et_al:LIPIcs.OPODIS.2024.7,
  author =	{Pavloff, Ulysse and Amoussou-Guenou, Yackolley and Tucci-Piergiovanni, Sara},
  title =	{{Incentive Compatibility of Ethereum’s PoS Consensus Protocol}},
  booktitle =	{28th International Conference on Principles of Distributed Systems (OPODIS 2024)},
  pages =	{7:1--7:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-360-7},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{324},
  editor =	{Bonomi, Silvia and Galletta, Letterio and Rivi\`{e}re, Etienne and Schiavoni, Valerio},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.OPODIS.2024.7},
  URN =		{urn:nbn:de:0030-drops-225431},
  doi =		{10.4230/LIPIcs.OPODIS.2024.7},
  annote =	{Keywords: Ethereum PoS, Game Theory, Block Reward}
}
Document
DOI: 10.4230/LIPIcs.OPODIS.2024.8
Optimal Multilevel Slashing for Blockchains

Authors: Kenan Wood, Hammurabi Mendes, and Jonad Pulaj

Published in: LIPIcs, Volume 324, 28th International Conference on Principles of Distributed Systems (OPODIS 2024)

Abstract
We present the notion of multilevel slashing, where proof-of-stake blockchain validators can obtain gradual levels of assurance that a certain block is bound to be finalized in a global consensus procedure, unless an increasing and optimally large number of Byzantine processes have their staked assets slashed - that is, deducted - due to provably incorrect behavior. Our construction is a highly parameterized generalization of combinatorial intersection systems based on finite projective spaces, with asymptotic high availability and optimal slashing properties. Even under weak conditions, we show that our construction has asymptotically optimal slashing properties with respect to message complexity and validator load; this result also illustrates a fundamental trade off between message complexity, load, and slashing. In addition, we show that any intersection system whose ground elements are disjoint subsets of nodes (e.g. "committees" in committee-based consensus protocols) has asymptotic high availability under similarly weak conditions. Finally, our multilevel construction gives the flexibility to blockchain validators to decide how many "levels" of finalization assurance they wish to obtain. This functionality can be seen either as (i) a form of an early, slashing-based block finalization; or (ii) a service to support reorg tolerance.
Cite as

Kenan Wood, Hammurabi Mendes, and Jonad Pulaj. Optimal Multilevel Slashing for Blockchains. In 28th International Conference on Principles of Distributed Systems (OPODIS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 324, pp. 8:1-8:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{wood_et_al:LIPIcs.OPODIS.2024.8,
  author =	{Wood, Kenan and Mendes, Hammurabi and Pulaj, Jonad},
  title =	{{Optimal Multilevel Slashing for Blockchains}},
  booktitle =	{28th International Conference on Principles of Distributed Systems (OPODIS 2024)},
  pages =	{8:1--8:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-360-7},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{324},
  editor =	{Bonomi, Silvia and Galletta, Letterio and Rivi\`{e}re, Etienne and Schiavoni, Valerio},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.OPODIS.2024.8},
  URN =		{urn:nbn:de:0030-drops-225445},
  doi =		{10.4230/LIPIcs.OPODIS.2024.8},
  annote =	{Keywords: Blockchains, Finality, Slashablility, Committees, Availability}
}
Document
DOI: 10.4230/LIPIcs.DISC.2022.12
Liveness and Latency of Byzantine State-Machine Replication

Authors: Manuel Bravo, Gregory Chockler, and Alexey Gotsman

Published in: LIPIcs, Volume 246, 36th International Symposium on Distributed Computing (DISC 2022)

Abstract
Byzantine state-machine replication (SMR) ensures the consistency of replicated state in the presence of malicious replicas and lies at the heart of the modern blockchain technology. Byzantine SMR protocols often guarantee safety under all circumstances and liveness only under synchrony. However, guaranteeing liveness even under this assumption is nontrivial. So far we have lacked systematic ways of incorporating liveness mechanisms into Byzantine SMR protocols, which often led to subtle bugs. To close this gap, we introduce a modular framework to facilitate the design of provably live and efficient Byzantine SMR protocols. Our framework relies on a view abstraction generated by a special SMR synchronizer primitive to drive the agreement on command ordering. We present a simple formal specification of an SMR synchronizer and its bounded-space implementation under partial synchrony. We also apply our specification to prove liveness and analyze the latency of three Byzantine SMR protocols via a uniform methodology. In particular, one of these results yields what we believe is the first rigorous liveness proof for the algorithmic core of the seminal PBFT protocol.
Cite as

Manuel Bravo, Gregory Chockler, and Alexey Gotsman. Liveness and Latency of Byzantine State-Machine Replication. In 36th International Symposium on Distributed Computing (DISC 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 246, pp. 12:1-12:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{bravo_et_al:LIPIcs.DISC.2022.12,
  author =	{Bravo, Manuel and Chockler, Gregory and Gotsman, Alexey},
  title =	{{Liveness and Latency of Byzantine State-Machine Replication}},
  booktitle =	{36th International Symposium on Distributed Computing (DISC 2022)},
  pages =	{12:1--12:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-255-6},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{246},
  editor =	{Scheideler, Christian},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.DISC.2022.12},
  URN =		{urn:nbn:de:0030-drops-172037},
  doi =		{10.4230/LIPIcs.DISC.2022.12},
  annote =	{Keywords: Replication, blockchain, partial synchrony, liveness}
}
Document
DOI: 10.4230/OASIcs.FAB.2022.5
Fork Accountability in Tenderbake

Authors: Antonella Del Pozzo and Thibault Rieutord

Published in: OASIcs, Volume 101, 5th International Symposium on Foundations and Applications of Blockchain 2022 (FAB 2022)

Abstract
This work investigates the Fork Accountability problem in the BFT-Consensus-based Blockchain context. When there are more attackers than the tolerated ones, BFT-Consensus may fail in delivering safety. When this occurs, Fork Accountability aims to account for the responsible processes for that safety violation. As a case study, we consider Tenderbake when the assumption on the maximum number of Byzantine validators - participants involved in creating the next block - does not hold anymore. When a fork occurs, there are more than one-third of Byzantine validators, and we aim to account for the responsible validators to remove them from the system. In this work, we compare three different approaches to implementing accountability in the case of a fork. In particular, we show that in the case of a fork, if we do not modify Tenderbake or we enrich it with a reliable broadcast communication abstraction, then we can account Byzantine processes only in particular scenarios. Contrarily, if we change Tenderbake such that the exchanged messages also carry extra information (which size is proportional to the duration of the current consensus computation), then we can account for Byzantine processes in all kinds of scenarios; however, at the cost of unbounded message size and unbounded local memory.
Cite as

Antonella Del Pozzo and Thibault Rieutord. Fork Accountability in Tenderbake. In 5th International Symposium on Foundations and Applications of Blockchain 2022 (FAB 2022). Open Access Series in Informatics (OASIcs), Volume 101, pp. 5:1-5:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{delpozzo_et_al:OASIcs.FAB.2022.5,
  author =	{Del Pozzo, Antonella and Rieutord, Thibault},
  title =	{{Fork Accountability in Tenderbake}},
  booktitle =	{5th International Symposium on Foundations and Applications of Blockchain 2022 (FAB 2022)},
  pages =	{5:1--5:22},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-248-8},
  ISSN =	{2190-6807},
  year =	{2022},
  volume =	{101},
  editor =	{Tucci-Piergiovanni, Sara and Crooks, Natacha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.FAB.2022.5},
  URN =		{urn:nbn:de:0030-drops-162723},
  doi =		{10.4230/OASIcs.FAB.2022.5},
  annote =	{Keywords: Blockchain, BFT-Consensus, Fork Accountability}
}
Document
DOI: 10.4230/OASIcs.FAB.2021.1
Tenderbake - A Solution to Dynamic Repeated Consensus for Blockchains

Authors: Lăcrămioara Aştefănoaei, Pierre Chambart, Antonella Del Pozzo, Thibault Rieutord, Sara Tucci-Piergiovanni, and Eugen Zălinescu

Published in: OASIcs, Volume 92, 4th International Symposium on Foundations and Applications of Blockchain 2021 (FAB 2021)

Abstract
First-generation blockchains provide probabilistic finality: a block can be revoked, albeit the probability decreases as the block "sinks" deeper into the chain. Recent proposals revisited committee-based BFT consensus to provide deterministic finality: as soon as a block is validated, it is never revoked. A distinguishing characteristic of these second-generation blockchains over classical BFT protocols is that committees change over time as the participation and the blockchain state evolve. In this paper, we push forward in this direction by proposing a formalization of the Dynamic Repeated Consensus problem and by providing generic procedures to solve it in the context of blockchains. Our approach is modular in that one can plug in different synchronizers and single-shot consensus. To offer a complete solution, we provide a concrete instantiation, called {{Tenderbake}}, and present a blockchain synchronizer and a single-shot consensus algorithm, working in a Byzantine and partially synchronous system model with eventually synchronous clocks. In contrast to recent proposals, our methodology is driven by the need to bound the message buffers. This is essential in preventing spamming and run-time memory errors. Moreover, {{Tenderbake}} processes can synchronize with each other without exchanging messages, leveraging instead the information stored in the blockchain.
Cite as

Lăcrămioara Aştefănoaei, Pierre Chambart, Antonella Del Pozzo, Thibault Rieutord, Sara Tucci-Piergiovanni, and Eugen Zălinescu. Tenderbake - A Solution to Dynamic Repeated Consensus for Blockchains. In 4th International Symposium on Foundations and Applications of Blockchain 2021 (FAB 2021). Open Access Series in Informatics (OASIcs), Volume 92, pp. 1:1-1:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{astefanoaei_et_al:OASIcs.FAB.2021.1,
  author =	{A\c{s}tef\u{a}noaei, L\u{a}cr\u{a}mioara and Chambart, Pierre and Del Pozzo, Antonella and Rieutord, Thibault and Tucci-Piergiovanni, Sara and Z\u{a}linescu, Eugen},
  title =	{{Tenderbake - A Solution to Dynamic Repeated Consensus for Blockchains}},
  booktitle =	{4th International Symposium on Foundations and Applications of Blockchain 2021 (FAB 2021)},
  pages =	{1:1--1:23},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-196-2},
  ISSN =	{2190-6807},
  year =	{2021},
  volume =	{92},
  editor =	{Gramoli, Vincent and Sadoghi, Mohammad},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.FAB.2021.1},
  URN =		{urn:nbn:de:0030-drops-139877},
  doi =		{10.4230/OASIcs.FAB.2021.1},
  annote =	{Keywords: Blockchain, BFT-Consensus, Dynamic Repeated Consensus}
}
Document
DOI: 10.4230/LIPIcs.DISC.2020.23
Making Byzantine Consensus Live

Authors: Manuel Bravo, Gregory Chockler, and Alexey Gotsman

Published in: LIPIcs, Volume 179, 34th International Symposium on Distributed Computing (DISC 2020)

Abstract
Partially synchronous Byzantine consensus protocols typically structure their execution into a sequence of views, each with a designated leader process. The key to guaranteeing liveness in these protocols is to ensure that all correct processes eventually overlap in a view with a correct leader for long enough to reach a decision. We propose a simple view synchronizer abstraction that encapsulates the corresponding functionality for Byzantine consensus protocols, thus simplifying their design. We present a formal specification of a view synchronizer and its implementation under partial synchrony, which runs in bounded space despite tolerating message loss during asynchronous periods. We show that our synchronizer specification is strong enough to guarantee liveness for single-shot versions of several well-known Byzantine consensus protocols, including HotStuff, Tendermint, PBFT and SBFT. We furthermore give precise latency bounds for these protocols when using our synchronizer. By factoring out the functionality of view synchronization we are able to specify and analyze the protocols in a uniform framework, which allows comparing them and highlights trade-offs.
Cite as

Manuel Bravo, Gregory Chockler, and Alexey Gotsman. Making Byzantine Consensus Live. In 34th International Symposium on Distributed Computing (DISC 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 179, pp. 23:1-23:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{bravo_et_al:LIPIcs.DISC.2020.23,
  author =	{Bravo, Manuel and Chockler, Gregory and Gotsman, Alexey},
  title =	{{Making Byzantine Consensus Live}},
  booktitle =	{34th International Symposium on Distributed Computing (DISC 2020)},
  pages =	{23:1--23:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-168-9},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{179},
  editor =	{Attiya, Hagit},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.DISC.2020.23},
  URN =		{urn:nbn:de:0030-drops-131013},
  doi =		{10.4230/LIPIcs.DISC.2020.23},
  annote =	{Keywords: Byzantine consensus, blockchain, partial synchrony, liveness}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2015.590
Failure-aware Runtime Verification of Distributed Systems

Authors: David Basin, Felix Klaedtke, and Eugen Zalinescu

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

Abstract
Prior runtime-verification approaches for distributed systems are limited as they do not account for network failures and they assume that system messages are received in the order they are sent. To overcome these limitations, we present an online algorithm for verifying observed system behavior at runtime with respect to specifications written in the real-time logic MTL that efficiently handles out-of-order message deliveries and operates in the presence of failures. Our algorithm uses a three-valued semantics for MTL, where the third truth value models knowledge gaps, and it resolves knowledge gaps as it propagates Boolean values through the formula structure. We establish the algorithm's soundness and provide completeness guarantees. We also show that it supports distributed system monitoring, where multiple monitors cooperate and exchange their observations and conclusions.
Cite as

David Basin, Felix Klaedtke, and Eugen Zalinescu. Failure-aware Runtime Verification of Distributed Systems. In 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 45, pp. 590-603, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{basin_et_al:LIPIcs.FSTTCS.2015.590,
  author =	{Basin, David and Klaedtke, Felix and Zalinescu, Eugen},
  title =	{{Failure-aware Runtime Verification of Distributed Systems}},
  booktitle =	{35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)},
  pages =	{590--603},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-97-2},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{45},
  editor =	{Harsha, Prahladh and Ramalingam, G.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2015.590},
  URN =		{urn:nbn:de:0030-drops-56194},
  doi =		{10.4230/LIPIcs.FSTTCS.2015.590},
  annote =	{Keywords: Runtime verification, monitoring algorithm, real-time logics, multi-valued semantics, distributed systems, asynchronous communication}
}
Document
DOI: 10.4230/OASIcs.TrustworthySW.2006.691
Relating two standard notions of secrecy

Authors: Eugen Zalinescu, Véronique Cortier, and Michaël Rusinowitch

Published in: OASIcs, Volume 3, Workshop on Trustworthy Software (2006)

Abstract
Two styles of definitions are usually considered to express that a security protocol preserves the confidentiality of a data { t s}. Reach-ability-based secrecy means that { t s} should never be disclosed while equi-valence-based secrecy states that two executions of a protocol with distinct instances for { t s} should be indistinguishable to an attacker. Although the second formulation ensures a higher level of security and is closer to cryptographic notions of secrecy, decidability results and automatic tools have mainly focused on the first definition so far. This paper initiates a systematic investigation of situations where syntactic secrecy entails strong secrecy. We show that in the passive case, reachability-based secrecy actually implies equivalence-based secrecy for signatures, symmetric and asymmetric encryption provided that the primitives are probabilistic. For active adversaries in the case of symmetric encryption, we provide sufficient (and rather tight) conditions on the protocol for this implication to hold.
Cite as

Eugen Zalinescu, Véronique Cortier, and Michaël Rusinowitch. Relating two standard notions of secrecy. In Workshop on Trustworthy Software. Open Access Series in Informatics (OASIcs), Volume 3, pp. 1-29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)

Copy BibTex To Clipboard

@InProceedings{zalinescu_et_al:OASIcs.TrustworthySW.2006.691,
  author =	{Zalinescu, Eugen and Cortier, V\'{e}ronique and Rusinowitch, Micha\"{e}l},
  title =	{{Relating two standard notions of secrecy}},
  booktitle =	{Workshop on Trustworthy Software},
  pages =	{1--29},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-02-6},
  ISSN =	{2190-6807},
  year =	{2006},
  volume =	{3},
  editor =	{Autexier, Serge and Merz, Stephan and van der Torre, Leon and Wilhelm, Reinhard and Wolper, Pierre},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.TrustworthySW.2006.691},
  URN =		{urn:nbn:de:0030-drops-6911},
  doi =		{10.4230/OASIcs.TrustworthySW.2006.691},
  annote =	{Keywords: Verification, security protocols, secrecy, applied-pi calculus}
}
  • Refine by Type
  • 11 Document/PDF
  • 5 Document/HTML

  • Refine by Publication Year
  • 5 2025
  • 2 2022
  • 1 2021
  • 1 2020
  • 1 2015
  • Show More...

  • Refine by Author
  • 2 Bravo, Manuel
  • 2 Chockler, Gregory
  • 2 Del Pozzo, Antonella
  • 2 Gotsman, Alexey
  • 2 Rieutord, Thibault
  • Show More...

  • Refine by Series/Journal
  • 8 LIPIcs
  • 3 OASIcs

  • Refine by Classification
  • 4 Theory of computation → Distributed algorithms
  • 2 Theory of computation → Distributed computing models
  • 2 Theory of computation → Logic and verification
  • 2 Theory of computation → Modal and temporal logics
  • 1 Computer systems organization → Dependable and fault-tolerant systems and networks
  • Show More...

  • Refine by Keyword
  • 2 BFT-Consensus
  • 2 Blockchain
  • 2 Runtime verification
  • 2 blockchain
  • 2 liveness
  • 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