Logic Seminar

The Logic Seminar is a joint LOS/IMAR/ILDS seminar, featuring talks on mathematical logic, philosophical logic and logical aspects of computer science.

All seminars, except where otherwise indicated, will be on Thursdays between 14:00 and 16:00, Bucharest time. The seminars are held locally at Hall 214 (“Google”) of the Faculty of Mathematics and Computer Science, University of Bucharest, but can also be occasionally held remotely.

To receive announcements about the seminar, please send an email to logic-seminar@ilds.ro.

Organizers: Laurențiu Leuștean, Andrei Sipoș

Past Talks in 2022-2023

Thursday, March 30, 2023

Denisa Diaconescu (University of Bucharest & Runtime Verification)

VLSM: A General Framework for Reasoning About Faulty Distributed Systems

Abstract:

Formally modeling and reasoning about distributed systems with faults is a challenging task [1]. Depending on the system model, an execution of a distributed protocol may be subject to many kinds of faults, from simple recoverable component crashes to Byzantine adversarial actions [4]. Each kind of failure may then require specific actions for evasion or recovery by the affected components.

To address this problem, we recently proposed the theory of Validating Labeled State transition and Message production systems (VLSMs) as a general approach to modeling and verifying distributed protocols executing in the presence of faults [5]. In particular, VLSM executions can be subject to equivocation behavior. Equivocation refers to claiming different beliefs about the state of the protocol to different parts of the system in order to steer the protocol-following components into making inconsistent decisions; messages received from equivocating components seem to be valid messages [3]. For example, if a system tries to come to a consensus about the value of a bit, an equivocating component may claim the bit is 0 to one part of the system, and 1 to the other. Equivocation behavior cannot be produced by a single protocol execution, but only by multiple protocol executions, i.e., an equivocating component behaves as if running multiple copies of the protocol.

Our VLSM-based modeling and verification methodology for distributed protocols follows the correct-by-construction approach for design and development [2]: we define an abstract class of protocols (satisfying some generic abstract properties), prove general results about protocols belonging to the class, and then obtain correct-by-construction protocols by concretely instantiating the abstract components, or, alternatively, prove that concrete protocols satisfy those requirements.

References:

[1] Pedro Fonseca, Kaiyuan Zhang, Xi Wang & Arvind Krishnamurthy (2017): An Empirical Study on the Correctness of Formally Verified Distributed Systems. In: European Conference on Computer Systems, pp. 328–343, doi:10.1145/3064176.3064183.

[2] David Gries (1981): The Science of Programming. Springer, doi:10.1007/978-1-4612-5983-1.

[3] Alexander Jaffe, Thomas Moscibroda & Siddhartha Sen (2012): On the price of equivocation in Byzantine agreement. In: Symposium on Principles of Distributed Computing, pp. 309–318, doi:10.1145/2332432.2332491.

[4] Leslie Lamport, Robert Shostak & Marshall Pease (1982): The Byzantine Generals Problem. ACM Transactions on Programming Languages and Systems 4(3), pp. 382–401, doi:10.1145/357172.357176.

[5] V. Zamfir, M. Calancea, D. Diaconescu, W. Kołowski, B. Moore, K. Palmskog, T. F. Șerbănuță, M. Stay, D. Trufaș, & J. Tušil (2022): Validating Labelled State Transition and Message Production Systems: A Theory for Modelling Faulty Distributed Systems. arXiv:2202.12662 [cs.DC].

Past Seminars