-
A Formally Verified Lightning Network
Authors:
Grzegorz Fabiański,
Rafał Stefański,
Orfeas Stefanos Thyfronitis Litos
Abstract:
In this work we use formal verification to prove that the Lightning Network (LN), the most prominent scaling technique for Bitcoin, always safeguards the funds of honest users. We provide a custom implementation of (a simplification of) LN, express the desired security goals and, for the first time, we provide a machine checkable proof that they are upheld under every scenario, all in an integrate…
▽ More
In this work we use formal verification to prove that the Lightning Network (LN), the most prominent scaling technique for Bitcoin, always safeguards the funds of honest users. We provide a custom implementation of (a simplification of) LN, express the desired security goals and, for the first time, we provide a machine checkable proof that they are upheld under every scenario, all in an integrated fashion. We build our system using the Why3 platform.
△ Less
Submitted 10 March, 2025;
originally announced March 2025.
-
Properties of nowhere dense graph classes related to independent set problem
Authors:
Grzegorz Fabiański
Abstract:
A set is called r-independent, if every two vertices of it are in distance greater then r. In the r-independent set problem with parameter k, we ask whether in a given graph G there exists an r-independent set of size k. In this work we present an algorithm for this problem, which applied to a graph from any fixed nowhere dense class, works in time bounded by f(k, r)*G, for some function f. We als…
▽ More
A set is called r-independent, if every two vertices of it are in distance greater then r. In the r-independent set problem with parameter k, we ask whether in a given graph G there exists an r-independent set of size k. In this work we present an algorithm for this problem, which applied to a graph from any fixed nowhere dense class, works in time bounded by f(k, r)*G, for some function f. We also present alternative algorithm, with running time bounded by g(k, r)*G, working on slightly more general classes of graphs.
△ Less
Submitted 27 November, 2019;
originally announced December 2019.
-
Progressive Algorithms for Domination and Independence
Authors:
Grzegorz Fabiański,
Michał Pilipczuk,
Sebastian Siebertz,
Szymon Toruńczyk
Abstract:
We consider a generic algorithmic paradigm that we call progressive exploration, which can be used to develop simple and efficient parameterized graph algorithms. We identify two model-theoretic properties that lead to efficient progressive algorithms, namely variants of the Helly property and stability. We demonstrate our approach by giving linear-time fixed-parameter algorithms for the distance-…
▽ More
We consider a generic algorithmic paradigm that we call progressive exploration, which can be used to develop simple and efficient parameterized graph algorithms. We identify two model-theoretic properties that lead to efficient progressive algorithms, namely variants of the Helly property and stability. We demonstrate our approach by giving linear-time fixed-parameter algorithms for the distance-r dominating set problem (parameterized by the solution size) in a wide variety of restricted graph classes, such as powers of nowhere dense classes, map graphs, and (for $r=1$) biclique-free graphs. Similarly, for the distance-r independent set problem the technique can be used to give a linear-time fixed-parameter algorithm on any nowhere dense class. Despite the simplicity of the method, in several cases our results extend known boundaries of tractability for the considered problems and improve the best known running times.
△ Less
Submitted 16 November, 2018;
originally announced November 2018.
