arXiv subjects

Wei Dong

Publications and source records attributed to Wei Dong.

168 records · Page 10Linked to original sources

arXiv2015

3D Wireless: Modeling Wireless Performance by Combining Spatial and Temporal Behaviors

Performance characterization is a fundamental issue in wireless networks for real time routing, wireless network simulation, and etc. There are four basic wireless operations that are required to be modeled, i.e., unicast, anycast, broadcast, and multicast. As observed in many recent works, the temporal and spatial distribution of packet receptions can have significant impact on wireless performance involving multiple links (anycast/broadcast/multicast). However, existing performance models and simulations overlook these two wireless behaviors, leading to biased performance estimation and simulation results. In this paper, we first explicitly identify the necessary "3-Dimension" information for wireless performance modeling, i.e., packet reception rate (PRR), PRR spatial distribution, and temporal distribution. We then propose a comprehensive modeling approach considering 3-Dimension Wireless information (called 3DW model). Further, we demonstrate the generality and wide applications of 3DW model by two case studies: 3DWbased network simulation and 3DW-based real time routing protocol. Extensive simulation and testbed experiments have been conducted. The results show that 3DW model achieves much more accurate performance estimation for both anycast and broadcast/multicast. 3DW-based simulation can effectively reserve the end-to-end performance metric of the input empirical traces. 3DW-based routing can select more efficient senders, achieving better transmission efficiency.

cs.NI↗

arXiv2014

MPISE: Symbolic Execution of MPI Programs

Message Passing Interfaces (MPI) plays an important role in parallel computing. Many parallel applications are implemented as MPI programs. The existing methods of bug detection for MPI programs have the shortage of providing both input and non-determinism coverage, leading to missed bugs. In this paper, we employ symbolic execution to ensure the input coverage, and propose an on-the-fly schedule algorithm to reduce the interleaving explorations for non-determinism coverage, while ensuring the soundness and completeness. We have implemented our approach as a tool, called MPISE, which can automatically detect the deadlock and runtime bugs in MPI programs. The results of the experiments on benchmark programs and real world MPI programs indicate that MPISE finds bugs effectively and efficiently. In addition, our tool also provides diagnostic information and replay mechanism to help understanding bugs.

cs.DC↗

arXiv2014

Diffusion Rates for Hydrogen on Pd(111) from Molecular Quantum Dynamics Calculations

Diffusion rates are calculated on the basis of van Hove's formula for the dynamical structure factor (DSF) related to particle scattering at mobile adsorbates. The formula is evaluated quantum mechanically using eigenfunctions obtained from three dimensional realistic models for H/Pd(111) derived from first principle calculations. Results are compatible with experimental data for H/Ru(0001) and H/Pt(111), if one assumes that the total rate obtained from the DSF is the sum of a diffusion and a friction rate. A simple kinetic model to support this assumption is presented.

physics.chem-ph↗

arXiv2013

A Subspace Technique for The Identification of Switched Affine Models

The problem of estimating parameters of switched affine systems with noisy input-output observations is considered. The switched affine models is transformed into a switched linear one by removing its intersection subspace, which is estimated from observations. A subspace technique is proposed to exploit the observations' permutation structure, which transforms the problem of associating observations with subsystems into one of de-permutating a block diagonal matrix, referred as adjacency matrix. Then a normalized spectral clustering algorithm is presented to recover the block structure of adjacency matrix, from which each observation is related to a particular subsystem. With the labelled observations, parameters of the submodel are estimated via the total least squares (TLS) estimator. The proposed technique is applicable to switched affine systems with arbitrarily shaped domain partitions, and it offers significantly improved performance and lowered computation complexity than existing techniques.

stat.ME↗

arXiv2013

Spectral Clustering on Subspace for Parameter Estimation of Jump Linear Models

The problem of estimating parameters of a deterministic jump or piecewise linear model is considered. A subspace technique referred to as spectral clustering on subspace (SCS) algorithm is proposed to estimate a set of linear model parameters, the model input, and the set of switching epochs. The SCS algorithm exploits a block diagonal structure of the system input subspace, which partitions the observation space into separate subspaces, each corresponding to one and only one linear submodel. A spectral clustering technique is used to label the noisy observations for each submodel, which generates estimates of switching time epoches. A total least squares technique is used to estimate model parameters and the model input. It is shown that, in the absence of observation noise, the SCS algorithm provides exact parameter identification. At high signal to noise ratios, SCS attains a clairvoyant Cramér-Rao bound computed by assuming the labeling of observation samples is perfect.

stat.ME↗

arXiv2013

Counterexample-Preserving Reduction for Symbolic Model Checking

The cost of LTL model checking is highly sensitive to the length of the formula under verification. We observe that, under some specific conditions, the input LTL formula can be reduced to an easier-to-handle one before model checking. In our reduction, these two formulae need not to be logically equivalent, but they share the same counterexample set w.r.t the model. In the case that the model is symbolically represented, the condition enabling such reduction can be detected with a lightweight effort (e.g., with SAT-solving). In this paper, we tentatively name such technique "Counterexample-Preserving Reduction" (CePRe for short), and finally the proposed technquie is experimentally evaluated by adapting NuSMV.

cs.LO↗