Skip to content
Institute for Logic and Data Science
Menu
  • Home
  • Research
    • Research Projects
    • Scientific Seminars
  • Events
  • People
  • Partners
  • About
    • About Us
    • Support us
    • Executive Board
    • Contact
Menu

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

  • LOS/IMAR/ILDS Logic Seminar in 2021-2022
  • LOS/IMAR Logic Seminar in 2020-2021
  • FMI/IMAR Logic Seminar in 2019-2020
  • FMI/IMAR Logic Seminar in 2018-2019
  • FMI/IMAR Logic Seminar in 2017-2018
  • FMI/IMAR Logic Seminar in 2016-2017
  • FMI/IMAR Logic Seminar in 2015-2016
  • FMI/IMAR Logic Seminar in 2014-2015
  • IMAR Logic Seminar in 2013-2014
  • IMAR Logic Seminar in 2012-2013
  • FMI Logic in Computer Science Seminar in 2014
  • FMI Logic in Computer Science Seminar in 2013

Follow us

Subscribe to our RSS feed.

Subscribe

Support us

Looking for ways to support our research? Check out all the different opportunities!

Contact us

Interested in logic and/or data science research? Send an email to contact@ilds.ro

Institute for Logic and Data Science
Str. Popa Tatu nr. 18
010805 Bucharest, Romania
contact@ilds.ro

© 2023 Institute for Logic and Data Science | Powered by Minimalist Blog WordPress Theme