-
Fully Automated Selfish Mining Analysis in Efficient Proof Systems Blockchains
Authors:
Krishnendu Chatterjee,
Amirali Ebrahimzadeh,
Mehrdad Karrabi,
Krzysztof Pietrzak,
Michelle Yeo,
Đorđe Žikelić
Abstract:
We study selfish mining attacks in longest-chain blockchains like Bitcoin, but where the proof of work is replaced with efficient proof systems -- like proofs of stake or proofs of space -- and consider the problem of computing an optimal selfish mining attack which maximizes expected relative revenue of the adversary, thus minimizing the chain quality. To this end, we propose a novel selfish mini…
▽ More
We study selfish mining attacks in longest-chain blockchains like Bitcoin, but where the proof of work is replaced with efficient proof systems -- like proofs of stake or proofs of space -- and consider the problem of computing an optimal selfish mining attack which maximizes expected relative revenue of the adversary, thus minimizing the chain quality. To this end, we propose a novel selfish mining attack that aims to maximize this objective and formally model the attack as a Markov decision process (MDP). We then present a formal analysis procedure which computes an $ε$-tight lower bound on the optimal expected relative revenue in the MDP and a strategy that achieves this $ε$-tight lower bound, where $ε>0$ may be any specified precision. Our analysis is fully automated and provides formal guarantees on the correctness. We evaluate our selfish mining attack and observe that it achieves superior expected relative revenue compared to two considered baselines.
In concurrent work [Sarenche FC'24] does an automated analysis on selfish mining in predictable longest-chain blockchains based on efficient proof systems. Predictable means the randomness for the challenges is fixed for many blocks (as used e.g., in Ouroboros), while we consider unpredictable (Bitcoin-like) chains where the challenge is derived from the previous block.
△ Less
Submitted 7 May, 2024;
originally announced May 2024.
-
Sound and Complete Witnesses for Template-based Verification of LTL Properties on Polynomial Programs
Authors:
Krishnendu Chatterjee,
Amir Kafshdar Goharshady,
Ehsan Kafshdar Goharshady,
Mehrdad Karrabi,
Đorđe Žikelić
Abstract:
We study the classical problem of verifying programs with respect to formal specifications given in the linear temporal logic (LTL). We first present novel sound and complete witnesses for LTL verification over imperative programs. Our witnesses are applicable to both verification (proving) and refutation (finding bugs) settings. We then consider LTL formulas in which atomic propositions can be po…
▽ More
We study the classical problem of verifying programs with respect to formal specifications given in the linear temporal logic (LTL). We first present novel sound and complete witnesses for LTL verification over imperative programs. Our witnesses are applicable to both verification (proving) and refutation (finding bugs) settings. We then consider LTL formulas in which atomic propositions can be polynomial constraints and turn our focus to polynomial arithmetic programs, i.e. programs in which every assignment and guard consists only of polynomial expressions. For this setting, we provide an efficient algorithm to automatically synthesize such LTL witnesses. Our synthesis procedure is both sound and semi-complete. Finally, we present experimental results demonstrating the effectiveness of our approach and that it can handle programs which were beyond the reach of previous state-of-the-art tools.
△ Less
Submitted 1 July, 2024; v1 submitted 8 March, 2024;
originally announced March 2024.
-
Solving Long-run Average Reward Robust MDPs via Stochastic Games
Authors:
Krishnendu Chatterjee,
Ehsan Kafshdar Goharshady,
Mehrdad Karrabi,
Petr Novotný,
Đorđe Žikelić
Abstract:
Markov decision processes (MDPs) provide a standard framework for sequential decision making under uncertainty. However, MDPs do not take uncertainty in transition probabilities into account. Robust Markov decision processes (RMDPs) address this shortcoming of MDPs by assigning to each transition an uncertainty set rather than a single probability value. In this work, we consider polytopic RMDPs i…
▽ More
Markov decision processes (MDPs) provide a standard framework for sequential decision making under uncertainty. However, MDPs do not take uncertainty in transition probabilities into account. Robust Markov decision processes (RMDPs) address this shortcoming of MDPs by assigning to each transition an uncertainty set rather than a single probability value. In this work, we consider polytopic RMDPs in which all uncertainty sets are polytopes and study the problem of solving long-run average reward polytopic RMDPs. We present a novel perspective on this problem and show that it can be reduced to solving long-run average reward turn-based stochastic games with finite state and action spaces. This reduction allows us to derive several important consequences that were hitherto not known to hold for polytopic RMDPs. First, we derive new computational complexity bounds for solving long-run average reward polytopic RMDPs, showing for the first time that the threshold decision problem for them is in $NP \cap coNP$ and that they admit a randomized algorithm with sub-exponential expected runtime. Second, we present Robust Polytopic Policy Iteration (RPPI), a novel policy iteration algorithm for solving long-run average reward polytopic RMDPs. Our experimental evaluation shows that RPPI is much more efficient in solving long-run average reward polytopic RMDPs compared to state-of-the-art methods based on value iteration.
△ Less
Submitted 30 April, 2024; v1 submitted 21 December, 2023;
originally announced December 2023.
-
Game Dynamics and Equilibrium Computation in the Population Protocol Model
Authors:
Dan Alistarh,
Krishnendu Chatterjee,
Mehrdad Karrabi,
John Lazarsfeld
Abstract:
We initiate the study of game dynamics in the population protocol model: $n$ agents each maintain a current local strategy and interact in pairs uniformly at random. Upon each interaction, the agents play a two-person game and receive a payoff from an underlying utility function, and they can subsequently update their strategies according to a fixed local algorithm. In this setting, we ask how the…
▽ More
We initiate the study of game dynamics in the population protocol model: $n$ agents each maintain a current local strategy and interact in pairs uniformly at random. Upon each interaction, the agents play a two-person game and receive a payoff from an underlying utility function, and they can subsequently update their strategies according to a fixed local algorithm. In this setting, we ask how the distribution over agent strategies evolves over a sequence of interactions, and we introduce a new distributional equilibrium concept to quantify the quality of such distributions. As an initial example, we study a class of repeated prisoner's dilemma games, and we consider a family of simple local update algorithms that yield non-trivial dynamics over the distribution of agent strategies. We show that these dynamics are related to a new class of high-dimensional Ehrenfest random walks, and we derive exact characterizations of their stationary distributions, bounds on their mixing times, and prove their convergence to approximate distributional equilibria. Our results highlight trade-offs between the local state space of each agent, and the convergence rate and approximation factor of the underlying dynamics. Our approach opens the door towards the further characterization of equilibrium computation for other classes of games and dynamics in the population setting.
△ Less
Submitted 19 May, 2024; v1 submitted 14 July, 2023;
originally announced July 2023.
-
Shadfa 0.1: The Iranian Movie Knowledge Graph and Graph-Embedding-Based Recommender System
Authors:
Rayhane Pouyan,
Hadi Kalamati,
Hannane Ebrahimian,
Mohammad Karrabi,
Mohammad-R. Akbarzadeh-T
Abstract:
Movies are a great source of entertainment. However, the problem arises when one is trying to find the desired content within this vast amount of data which is significantly increasing every year. Recommender systems can provide appropriate algorithms to solve this problem. The content_based technique has found popularity due to the lack of available user data in most cases. Content_based recommen…
▽ More
Movies are a great source of entertainment. However, the problem arises when one is trying to find the desired content within this vast amount of data which is significantly increasing every year. Recommender systems can provide appropriate algorithms to solve this problem. The content_based technique has found popularity due to the lack of available user data in most cases. Content_based recommender systems are based on the similarity of items' demographic information; Term Frequency _ Inverse Document Frequency (TF_IDF) and Knowledge Graph Embedding (KGE) are two approaches used to vectorize data to calculate these similarities. In this paper, we propose a weighted content_based movie RS by combining TF_IDF which is an appropriate approach for embedding textual data such as plot/description, and KGE which is used to embed named entities such as the director's name. The weights between features are determined using a Genetic algorithm. Additionally, the Iranian movies dataset is created by scra** data from movie_related websites. This dataset and the structure of the FarsBase KG are used to create the MovieFarsBase KG which is a component in the implementation process of the proposed content_based RS. Using precision, recall, and F1 score metrics, this study shows that the proposed approach outperforms the conventional approach that uses TF_IDF for embedding all attributes.
△ Less
Submitted 14 October, 2022;
originally announced October 2022.
