In permissioned blockchains, a set of identifiable miners validates transactions and creates new blocks. In scholarship, the proposed solution for the consensus protocol is usually inspired by the Byzantine fault tolerance (BFT) based on voting rather than the proof-of-work (PoW). The advantage of PoW with respect to BFT is that it allows the final user to evaluate the cost required to change a confirmed transaction without the need to trust the consortium of miners. In this paper, we analyse the problems that arise from the application of PoW in permissioned blockchains. In standard PoW, it may be easy for colluded miners to temporarily reach 50% of the total hash power (HP). Moreover, since mining rewards are not usually expected in permissioned contexts, the problem of balancing the computational efforts among the miners becomes crucial. We propose a solution based on a sliding window algorithm to address these problems and analyse its effectiveness in terms of fairness and security. Furthermore, we present a quantitative, analytical model in order to assess its capacity to balance the hash power provided by heterogeneous miners. Our study considers the trade-off between the need to trust the entire consortium of miners guaranteed by the global HP invested by the mining process and the need to prevent collusion among malicious miners aimed at reaching 50% of the total HP. As a result, the model can be used to find the optimal parameters for the sliding window protocol.

In this paper, we deal with the lumpability approach to cope with the state space explosion problem inherent to the computation of the stationary performance indices of large stochastic models. The lumpability method is based on a state aggregation technique and applies to Markov chains exhibiting some structural regularity. Moreover, it allows one to efficiently compute the exact values of the stationary performance indices when the model is actually lumpable. The notion of quasi-lumpability is based on the idea that a Markov chain can be altered by relatively small perturbations of the transition rates in such a way that the new resulting Markov chain is lumpable. In this case, only upper and lower bounds on the performance indices can be derived. Here, we introduce a novel notion of quasi-lumpability, named proportional lumpability, which extends the original definition of lumpability but, differently from the general definition of quasi-lumpability, it allows one to derive exact stationary performance indices for the original process. We then introduce the notion of proportional bisimilarity for the terms of the performance process algebra PEPA. Proportional bisimilarity induces a proportional lumpability on the underlying continuous-time Markov chains. Finally, we prove some compositionality results and show the applicability of our theory through examples.

Quantitative analysis of computer systems is often based\ud on Markovian models. Among the formalisms that are used\ud in practice, Markovian process algebras have found many\ud applications, also thanks to their compositional nature that\ud allows one to specify systems as interacting individual au-\ud tomata that carry out actions. Nevertheless, as with all\ud state-based modelling techniques, Markovian process alge-\ud bras suer from the well-known state space explosion prob-\ud lem. State aggregation, specically lumping, is one of the\ud possible methods for tackling this problem. In this paper we\ud revisit the notion ofMarkovian bisimulation which has previ-\ud ously been shown to induce a lumpable relation in the under-\ud lying Markov process. Here we consider the coarser relation\ud of contextual lumpability, and taking the specic example of\ud strong equivalence in PEPA, we propose a slightly relaxed\ud denition of Markovian bisimulation, named lumpable bisim-\ud ilarity, and prove that this is a characterisation of the notion\ud of contextual lumpability for PEPA components. Moreover,\ud we show that lumpable bisimilarity induces the largest con-\ud textual lumping over the Markov process underlying any\ud PEPA component. We provide an algorithm for lumpable\ud bisimilarity and study both its time and space complexity

The systematic development of complex systems usually relies on a stepwise refinement procedure from an abstract specification to a more concrete one that can finally be implemented. The use of refinement operators preserving system properties is clearly essential since it avoids properties to be re-investigated at each development step. In this paper, we formalize the notion of refinement for processes described as terms of the security process algebra (SPA). We consider several information flow security properties and provide sufficient conditions under which our refinement operators preserve such security properties. Finally, we study how refinements can be composed still preserving the security of the system.