arXiv subjects

Ru Yang

Publications and source records attributed to Ru Yang.

5 recordsLinked to original sources

arXiv2023

On-the-fly Unfolding with Optimal Exploration for Linear Temporal Logic Model Checking of Concurrent Software and Systems

Context: Linear temporal logic (LTL) model checking faces a significant challenge known as the state-explosion problem. The on-the-fly method is a solution that constructs and checks the state space simultaneously, avoiding generating all states in advance. But it is not effective for concurrent interleaving. Unfolding based on Petri nets is a succinct structure covering all states that can mitigate this problem caused by concurrency. Many state-of-the-art methods optimally explore a complete unfolding structure using a tree-like structure. However, it is difficult to apply such a tree-like structure directly to the traditional on-the-fly method of LTL. At the same time, constructing a complete unfolding structure in advance and then checking LTL is also wasteful. Thus, the existing optimal exploration methods are not applicable to the on-the-fly unfolding. Objective: To solve these challenges, we propose an LTL model-checking method called on-the-fly unfolding with optimal exploration. This method is based on program dependence net (PDNet) proposed in the previous work. Method: Firstly, we define conflict transitions of PDNet and an exploration tree with a novel notion of delayed transitions, which differs from the existing tree-like structure. The tree improves the on-the-fly unfolding by exploring each partial-order run only once and avoiding enumerating all possible combinations. Then, we propose an on-the-fly unfolding algorithm that simultaneously constructs the exploration tree and generates the unfolding structure while checking LTL. Results: We implement a tool for concurrent programs. It also improves traditional unfolding generations and performs better than SPIN and DiVine on the used benchmarks.

cs.LO↗

arXiv2021

Deep DIC: Deep Learning-Based Digital Image Correlation for End-to-End Displacement and Strain Measurement

Digital image correlation (DIC) has become an industry standard to retrieve accurate displacement and strain measurement in tensile testing and other material characterization. Though traditional DIC offers a high precision estimation of deformation for general tensile testing cases, the prediction becomes unstable at large deformation or when the speckle patterns start to tear. In addition, traditional DIC requires a long computation time and often produces a low spatial resolution output affected by filtering and speckle pattern quality. To address these challenges, we propose a new deep learning-based DIC approach--Deep DIC, in which two convolutional neural networks, DisplacementNet and StrainNet, are designed to work together for end-to-end prediction of displacements and strains. DisplacementNet predicts the displacement field and adaptively tracks a region of interest. StrainNet predicts the strain field directly from the image input without relying on the displacement prediction, which significantly improves the strain prediction accuracy. A new dataset generation method is developed to synthesize a realistic and comprehensive dataset, including the generation of speckle patterns and the deformation of the speckle image with synthetic displacement fields. Though trained on synthetic datasets only, Deep DIC gives highly consistent and comparable predictions of displacement and strain with those obtained from commercial DIC software for real experiments, while it outperforms commercial software with very robust strain prediction even at large and localized deformation and varied pattern qualities. In addition, Deep DIC is capable of real-time prediction of deformation with a calculation time down to milliseconds.

eess.IV↗

arXiv2021

Using GAN-based models to sentimental analysis on imbalanced datasets in education domain

While the whole world is still struggling with the COVID-19 pandemic, online learning and home office become more common. Many schools transfer their courses teaching to the online classroom. Therefore, it is significant to mine the students' feedback and opinions from their reviews towards studies so that both schools and teachers can know where they need to improve. This paper trains machine learning and deep learning models using both balanced and imbalanced datasets for sentiment classification. Two SOTA category-aware text generation GAN models: CatGAN and SentiGAN, are utilized to synthesize text used to balance the highly imbalanced dataset. Results on three datasets with different imbalance degree from distinct domains show that when using generated text to balance the dataset, the F1-score of machine learning and deep learning model on sentiment classification increases 2.79% ~ 9.28%. Also, the results indicate that the average growth degree for CR100k is higher than CR23k, the average growth degree for deep learning is more increased than machine learning algorithms, and the average growth degree for more complex deep learning models is more increased than simpler deep learning models in experiments.

cs.CL↗

arXiv2021

Modeling and Analysis of Three Properties of Mobile Interactive Systems Based on Variable Petri Nets

Due to the mobility and frequent disconnections, the correctness of mobile interaction systems, such as mobile robot systems and mobile payment systems, are often difficult to analyze. This paper introduces three critical properties of systems, called system connectivity, interaction soundness and data validity, and presents a related modeling and analysis method, based on a kind of Petri nets called VPN. For a given system, a model including component nets and interaction structure nets is constructed by using VPNs. The component net describes the internal process of each component, while the interaction structure net reflects the dynamic interaction between components. Based on this model, three properties are defined and analyzed. The case study of a practical mobile payment system shows the effectiveness of the proposed method.

eess.SY↗

arXiv2021

Variable Petri Nets for Mobility

Mobile computing systems, service-based systems and some other systems with mobile interacting components have recently received much attention. However, because of their characteristics such as mobility and disconnection, it is difficult to model and analyze them by using a structure-fixed model. This work proposes a new Petri net model called Variable Petri Net (VPN) for modeling and analyzing these systems. The definition, firing rule, and related analysis technology of VPN are introduced in detail. In a VPN, the possible interaction interfaces are abstracted as a new kind of places called virtual places, and the occurrences of (dis)connections are described by new functions, which makes it appropriate to describe the component collaboration in systems and realize the scalability and pluggability of systems. Moreover, to overcome the shortcoming that markings cannot reflect link capability of a system, VPNs add a constraint function along with a marking to represent a complete system configuration. Several examples are used to demonstrate the newly proposed model and method.

cs.SE↗