Showing 1–3 of 3 results for author: Chambart, P

Tenderbake -- A Solution to Dynamic Repeated Consensus for Blockchains

Authors: Lăcrămioara Aştefanoaei, Pierre Chambart, Antonella Del Pozzo, Thibault Rieutord, Sara Tucci, Eugen Zălinescu

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 prot… ▽ More 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 instances. 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. △ Less

Submitted 25 February, 2021; v1 submitted 31 January, 2020; originally announced January 2020.

Comments: This new version mainly brings the following improvements: (1) endorsement messages do not need to contain a aQC, therefore the message size of proposals and the size of message buffers decreases by a factor of `n`; and (2) the implementation of 'betterChain' (now called 'betterHead') has changed

Forward Analysis and Model Checking for Trace Bounded WSTS

Authors: Pierre Chambart, Alain Finkel, Sylvain Schmitz

Abstract: We investigate a subclass of well-structured transition systems (WSTS), the bounded---in the sense of Ginsburg and Spanier (Trans. AMS 1964)---complete deterministic ones, which we claim provide an adequate basis for the study of forward analyses as developed by Finkel and Goubault-Larrecq (Logic. Meth. Comput. Sci. 2012). Indeed, we prove that, unlike other conditions considered previously for th… ▽ More We investigate a subclass of well-structured transition systems (WSTS), the bounded---in the sense of Ginsburg and Spanier (Trans. AMS 1964)---complete deterministic ones, which we claim provide an adequate basis for the study of forward analyses as developed by Finkel and Goubault-Larrecq (Logic. Meth. Comput. Sci. 2012). Indeed, we prove that, unlike other conditions considered previously for the termination of forward analysis, boundedness is decidable. Boundedness turns out to be a valuable restriction for WSTS verification, as we show that it further allows to decide all $ω$-regular properties on the set of infinite traces of the system. △ Less

Submitted 4 March, 2016; v1 submitted 16 April, 2010; originally announced April 2010.

Report number: RR-LSV-10-08 ACM Class: D.2.4; F.4.1; F.4.3

Journal ref: 32nd International Conference on Application and Theory of Petri Nets, volume 6709 of Lecture Notes in Computer Science, pages 49--68. Springer Heidelberg

Toward a Compositional Theory of Leftist Grammars and Transformations

Authors: Pierre Chambart, Philippe Schnoebelen

Abstract: Leftist grammars [Motwani et al., STOC 2000] are special semi-Thue systems where symbols can only insert or erase to their left. We develop a theory of leftist grammars seen as word transformers as a tool toward rigorous analyses of their computational power. Our main contributions in this first paper are (1) constructions proving that leftist transformations are closed under compositions and tr… ▽ More Leftist grammars [Motwani et al., STOC 2000] are special semi-Thue systems where symbols can only insert or erase to their left. We develop a theory of leftist grammars seen as word transformers as a tool toward rigorous analyses of their computational power. Our main contributions in this first paper are (1) constructions proving that leftist transformations are closed under compositions and transitive closures, and (2) a proof that bounded reachability is NP-complete even for leftist grammars with acyclic rules. △ Less

Submitted 27 January, 2010; originally announced January 2010.

Comments: Full version of the FOSSACS 2010 paper

Journal ref: Proc. FoSSaCS'10, LNCS 6014, pages 237-251. Springer, 2010