Searcharxiv⌕ Search

arXiv subjects

Jun Pang

Publications and source records attributed to Jun Pang.

64 records · Page 4Linked to original sources
arXiv2015

Parallel Approximate Steady-state Analysis of Large Probabilistic Boolean Networks (Technical Report)

Probabilistic Boolean networks (PBNs) is a widely used computational framework for modelling biological systems. The steady-state dynamics of PBNs is of special interest in the analysis of biological systems. However, obtaining the steady-state distributions for such systems poses a significant challenge due to the state space explosion problem which often arises in the case of large PBNs. The only viable way is to use statistical methods. We have considered the two-state Markov chain approach and the Skart method for the analysis of large PBNs in our previous work. However, the sample size required in both methods is often huge in the case of large PBNs and generating them is expensive in terms of computation time. Parallelising the sample generation is an ideal way to solve this issue. In this paper, we consider combining the German & Rubin method with either the two-state Markov chain approach or the Skart method for parallelisation. The first method can be used to run multiple independent Markov chains in parallel and to control their convergence to the steady-state while the other two methods can be used to determine the sample size required for computing the steady-state probability of states of interest. Experimental results show that our proposed combinations can reduce time cost of computing stead-state probabilities of large PBNs significantly.

cs.DC↗
arXiv2014

Proceedings Third International Workshop on Engineering Safety and Security Systems

The International Workshop on Engineering Safety and Security Systems (ESSS) aims at contributing to the challenge of constructing reliable and secure systems. The workshop covers areas such as formal specification, type checking, model checking, program analysis/transformation, model-based testing and model-driven software construction. The workshop will bring together researchers and industry R&D expertise together to exchange their knowledge, discuss their research findings, and explore potential collaborations. The main theme of the workshop is methods and techniques for constructing large reliable and secure systems. The goal of the workshop is to establish a platform for the exchange of ideas, discussion, cross-fertilization, inspiration, co-operation, and dissemination.

cs.SE↗
arXiv2014

Stateful Security Protocol Verification

A long-standing research problem in security protocol design is how to efficiently verify security protocols with tamper-resistant global states. In this paper, we address this problem by first proposing a protocol specification framework, which explicitly represents protocol execution states and state transformations. Secondly, we develop an algorithm for verifying security properties by utilizing the key ingredients of the first-order reasoning for reachability analysis, while tracking state transformation and checking the validity of newly generated states. Our verification algorithm is proven to be (partially) correct, if it terminates. We have implemented the proposed framework and verification algorithms in a tool named SSPA, and evaluate it using a number of stateful security protocols. The experimental results show that our approach is not only feasible but also practically efficient. In particular, we have found a security flaw on the digital envelope protocol, which could not be detected by existing security protocol verifiers.

cs.CR↗
arXiv2012

An Algorithm for Probabilistic Alternating Simulation

In probabilistic game structures, probabilistic alternating simulation (PA-simulation) relations preserve formulas defined in probabilistic alternating-time temporal logic with respect to the behaviour of a subset of players. We propose a partition based algorithm for computing the largest PA-simulation, which is to our knowledge the first such algorithm that works in polynomial time, by extending the generalised coarsest partition problem (GCPP) in a game-based setting with mixed strategies. The algorithm has higher complexities than those in the literature for non-probabilistic simulation and probabilistic simulation without mixed actions, but slightly improves the existing result for computing probabilistic simulation with respect to mixed actions.

cs.GT↗
arXiv2011

A Study of the PDGF Signaling Pathway with PRISM

In this paper, we apply the probabilistic model checker PRISM to the analysis of a biological system -- the Platelet-Derived Growth Factor (PDGF) signaling pathway, demonstrating in detail how this pathway can be analyzed in PRISM. We show that quantitative verification can yield a better understanding of the PDGF signaling pathway.

cs.CE↗
arXiv2011

A Group Signature Based Electronic Toll Pricing System

With the prevalence and development of GNSS technologies, location-based vehicle services (LBVS) have experienced a rapid growth in recent years. However, location is a sensitive and private piece of information, so the design and development of such services just take the clients' privacy concerns into account. In this paper, we propose a new electronic toll pricing system based on group signatures, which provides a strong guarantee for the clients' anonymity within groups. Our system achieves a balance between privacy and the communication overhead imposed upon the users.

cs.CR↗
arXiv2011

Asynchronous Bounded Expected Delay Networks

The commonly used asynchronous bounded delay (ABD) network models assume a fixed bound on message delay. We propose a probabilistic network model, called asynchronous bounded expected delay (ABE) model. Instead of a strict bound, the ABE model requires only a bound on the expected message delay. While the conditions of ABD networks restrict the set of possible executions, in ABE networks all asynchronous executions are possible, but executions with extremely long delays are less probable. In contrast to ABD networks, ABE networks cannot be synchronised efficiently. At the example of an election algorithm, we show that the minimal assumptions of ABE networks are sufficient for the development of efficient algorithms. For anonymous, unidirectional ABE rings of known size N we devise a probabilistic leader election algorithm having average message and time complexity O(N).

cs.DC↗
arXiv2010

On Probabilistic Alternating Simulations

This paper presents simulation-based relations for probabilistic game structures. The first relation is called probabilistic alternating simulation, and the second called probabilistic alternating forward simulation, following the naming convention of Segala and Lynch. We study these relations with respect to the preservation of properties specified in probabilistic alternating-time temporal logic.

cs.LO↗
arXiv2009

How to Work with Honest but Curious Judges? (Preliminary Report)

The three-judges protocol, recently advocated by Mclver and Morgan as an example of stepwise refinement of security protocols, studies how to securely compute the majority function to reach a final verdict without revealing each individual judge's decision. We extend their protocol in two different ways for an arbitrary number of 2n+1 judges. The first generalisation is inherently centralised, in the sense that it requires a judge as a leader who collects information from others, computes the majority function, and announces the final result. A different approach can be obtained by slightly modifying the well-known dining cryptographers protocol, however it reveals the number of votes rather than the final verdict. We define a notion of conditional anonymity in order to analyse these two solutions. Both of them have been checked in the model checker MCMAS.

cs.CR↗