SearcharxivSearch

arXiv subjects

Huan Long

Publications and source records attributed to Huan Long.

14 recordsLinked to original sources

3-VASS Reachability is in EXPSPACE

A VASS can be viewed as a finite-state automaton manipulating a fixed number (called its dimension) of counters holding non-negative values. The reachability problem, asking whether there is a run from one configuration, defined by a state and values of the counters, to another configuration, has been a long-standing algorithmic challenge in theoretical computer science. When the dimension is part of the input, the problem has been shown to be ACKERMANN-complete in 2021. For fixed dimension greater than 2, and in particular for dimension 3, the exact complexity of the reachability problem remains unclear. For a long time the known algorithms for the 3-dimensional VASS reachability problem had been non-elementary, while the best known lower bound is merely PSPACE hardness inherited from dimension 2. A recent breakthrough in (Czerwi\'nski, Jecker, Lasota, Orlikowski, ICALP 2025) gave the first elementary upper bound for the problem, namely 2-EXPSPACE. In this paper it is shown that the reachability problem in 3-VASS belongs to EXPSPACE. The proof is based on a hierarchical pumpability analysis, yielding a doubly-exponential length bound on the shortest runs between two configurations.

cs.FL

A Unifying Approach to Probabilistic Testing Equivalences

Probabilistic concurrent systems are foundational models for modern mobile computing. In this paper, a unifying approach to probabilistic testing equivalences is proposed. With the help of a new distribution-based semantics for probabilistic models and a probabilistic testing framework with respect to process predicates, the internal characterization and the external characterization for testing equivalences are studied. The latter characterization can be viewed as the generalization of the classical fair/should equivalence and may equivalence. These equivalences are shown to be congruences. A thorough comparison between these equivalences and probabilistic bisimilarities is carried out. The techniques introduced in this paper can be easily extended to other probabilistic concurrent models. To showcase this flexibility, a case study is carried out on the pCSP model.

cs.LO

A Programming Language for Feasible Solutions

Runtime efficiency and termination are crucial properties in the studies of program verification. Instead of dealing with these issues in an ad hoc manner, it would be useful to develop a robust framework in which such properties are guaranteed by design. This paper introduces a new imperative programming language whose design is grounded in a static type system that ensures the following equivalence property: All definable programs are guaranteed to run in polynomial time; Conversely, all problems solvable in polynomial time can be solved by some programs of the language. The contribution of this work is twofold. On the theoretical side, the foundational equivalence property is established, and the proof of the equivalence theorem is non-trivial. On the practical side, a programming approach is proposed that can streamline program analysis and verification for feasible computations. An interpreter for the language has been implemented, demonstrating the feasibility of the approach in practice.

cs.PL

Analyzing Divergence for Nondeterministic Probabilistic Models

Branching and weak probabilistic bisimilarities are two well-known notions capturing behavioral equivalence between nondeterministic probabilistic systems. For probabilistic systems, divergence is of major concern. Recently several divergence-sensitive refinements of branching and weak probabilistic bisimilarities have been proposed in the literature. Both the definitions of these equivalences and the techniques to investigate them differ significantly. This paper presents a comprehensive comparative study on divergence-sensitive behavioral equivalence relations that refine the branching and weak probabilistic bisimilarities. Additionally, these equivalence relations are shown to have efficient checking algorithms. The techniques of this paper might be of independent interest in a more general setting.

cs.LO

Image-Based Abnormal Data Detection and Cleaning Algorithm via Wind Power Curve

This paper proposes an image-based algorithm for detecting and cleaning the wind turbine abnormal data based on wind power curve (WPC) images. The abnormal data are categorized into three types, negative points, scattered points, and stacked points. The proposed algorithm includes three steps, data pre-cleaning, normal data extraction, and data marking. The negative abnormal points, whose wind speed is greater than cut-in speed and power is below zero, are first filtered in the data pre-cleaning step. The scatter figure of the rest wind power data forms the WPC image and corresponding binary image. In the normal data extraction step, the principle part of the WPC binary image, representing the normal data, is extracted by the mathematical morphology operation (MMO). The optimal parameter setting of MMO is determined by minimizing the dissimilarity between the extracted principle part and the reference WPC image based on Hu moments. In the data mark step, the pixel points of scattered and stacked abnormal data are successively identified. The mapping relationship between the wind power points and image pixel points is built to mark the wind turbine normal and abnormal data. The proposed image-based algorithm is compared with k-means, local outlier factor, combined algorithm based on change point grouping algorithm and quartile algorithm (CA). Numerous experiments based on 33 wind turbines from two wind farms are conducted to validate the effectiveness, efficiency, and universality of the proposed method.

eess.SY

Computationally Enhanced Approach for Chance-Constrained OPF Considering Voltage Stability

The effective management of stochastic characteristics of renewable power generations is vital for ensuring the stable and secure operation of power systems. This paper addresses the task of optimizing the chance-constrained voltage-stability-constrained optimal power flow (CC-VSC-OPF) problem, which is hindered by the implicit voltage stability index and intractable chance constraints Leveraging a neural network (NN)-based surrogate model, the stability constraint is explicitly formulated and directly integrated into the model. To perform uncertainty propagation without relying on presumptions or complicated transformations, an advanced data-driven method known as adaptive polynomial chaos expansion (APCE) is developed. To extend the scalability of the proposed algorithm, a partial least squares (PLS)-NN framework is designed, which enables the establishment of a parsimonious surrogate model and efficient computation of large-scale Hessian matrices. In addition, a dimensionally decomposed APCE (DD-APCE) is proposed to alleviate the "curse of dimensionality" by restricting the interaction order among random variables. Finally, the above techniques are merged into an iterative scheme to update the operation point. Simulation results reveal the cost-effective performances of the proposed method in several test systems.

eess.SY

Safety-aware Semi-end-to-end Coordinated Decision Model for Voltage Regulation in Active Distribution Network

Prediction plays a vital role in the active distribution network voltage regulation under the high penetration of photovoltaics. Current prediction models aim at minimizing individual prediction errors but overlook their collective impacts on downstream decision-making. Hence, this paper proposes a safety-aware semi-end-to-end coordinated decision model to bridge the gap from the downstream voltage regulation to the upstream multiple prediction models in a coordinated differential way. The semi-end-to-end model maps the input features to the optimal var decisions via prediction, decision-making, and decision-evaluating layers. It leverages the neural network and the second-order cone program (SOCP) to formulate the stochastic PV/load predictions and the var decision-making/evaluating separately. Then the var decision quality is evaluated via the weighted sum of the power loss for economy and the voltage violation penalty for safety, denoted by regulation loss. Based on the regulation loss and prediction errors, this paper proposes the hybrid loss and hybrid stochastic gradient descent algorithm to back-propagate the gradients of the hybrid loss with respect to multiple predictions for enhancing decision quality. Case studies verify the effectiveness of the proposed model with lower power loss for economy and lower voltage violation rate for safety awareness.

eess.SY

Electricity Price Prediction for Energy Storage System Arbitrage: A Decision-focused Approach

Electricity price prediction plays a vital role in energy storage system (ESS) management. Current prediction models focus on reducing prediction errors but overlook their impact on downstream decision-making. So this paper proposes a decision-focused electricity price prediction approach for ESS arbitrage to bridge the gap from the downstream optimization model to the prediction model. The decision-focused approach aims at utilizing the downstream arbitrage model for training prediction models. It measures the difference between actual decisions under the predicted price and oracle decisions under the true price, i.e., decision error, by regret, transforms it into the tractable surrogate regret, and then derives the gradients to predicted price for training prediction models. Based on the prediction and decision errors, this paper proposes the hybrid loss and corresponding stochastic gradient descent learning method to learn prediction models for prediction and decision accuracy. The case study verifies that the proposed approach can efficiently bring more economic benefits and reduce decision errors by flattening the time distribution of prediction errors, compared to prediction models for only minimizing prediction errors.

cs.LG

Conservative Sparse Neural Network Embedded Frequency-Constrained Unit Commitment With Distributed Energy Resources

The increasing penetration of distributed energy resources (DERs) will decrease the rotational inertia of the power system and further degrade the system frequency stability. To address the above issues, this paper leverages the advanced neural network (NN) to learn the frequency dynamics and incorporates NN to facilitate system reliable operation. This paper proposes the conservative sparse neural network (CSNN) embedded frequency-constrained unit commitment (FCUC) with converter-based DERs, including the learning and optimization stages. In the learning stage, it samples the inertia parameters, calculates the corresponding frequency, and characterizes the stability region of the sampled parameters using the convex hulls to ensure stability and avoid extrapolation. For conservativeness, the positive prediction error penalty is added to the loss function to prevent possible frequency requirement violation. For the sparsity, the NN topology pruning is employed to eliminate unnecessary connections for solving acceleration. In the optimization stage, the trained CSNN is transformed into mixed-integer linear constraints using the big-M method and then incorporated to establish the data-enhanced model. The case study verifies 1) the effectiveness of the proposed model in terms of high accuracy, fewer parameters, and significant solving acceleration; 2) the stable system operation against frequency violation under contingency.

eess.SY

On Geometric Structure of Activation Spaces in Neural Networks

In this paper, we investigate the geometric structure of activation spaces of fully connected layers in neural networks and then show applications of this study. We propose an efficient approximation algorithm to characterize the convex hull of massive points in high dimensional space. Based on this new algorithm, four common geometric properties shared by the activation spaces are concluded, which gives a rather clear description of the activation spaces. We then propose an alternative classification method grounding on the geometric structure description, which works better than neural networks alone. Surprisingly, this data classification method can be an indicator of overfitting in neural networks. We believe our work reveals several critical intrinsic properties of modern neural networks and further gives a new metric for evaluating them.

cs.LG

Knowledge-based Fully Convolutional Network and Its Application in Segmentation of Lung CT Images

A variety of deep neural networks have been applied in medical image segmentation and achieve good performance. Unlike natural images, medical images of the same imaging modality are characterized by the same pattern, which indicates that same normal organs or tissues locate at similar positions in the images. Thus, in this paper we try to incorporate the prior knowledge of medical images into the structure of neural networks such that the prior knowledge can be utilized for accurate segmentation. Based on this idea, we propose a novel deep network called knowledge-based fully convolutional network (KFCN) for medical image segmentation. The segmentation function and corresponding error is analyzed. We show the existence of an asymptotically stable region for KFCN which traditional FCN doesn't possess. Experiments validate our knowledge assumption about the incorporation of prior knowledge into the convolution kernels of KFCN and show that KFCN can achieve a reasonable segmentation and a satisfactory accuracy.

cs.CV

Curvature-based Comparison of Two Neural Networks

In this paper we show the similarities and differences of two deep neural networks by comparing the manifolds composed of activation vectors in each fully connected layer of them. The main contribution of this paper includes 1) a new data generating algorithm which is crucial for determining the dimension of manifolds; 2) a systematic strategy to compare manifolds. Especially, we take Riemann curvature and sectional curvature as part of criterion, which can reflect the intrinsic geometric properties of manifolds. Some interesting results and phenomenon are given, which help in specifying the similarities and differences between the features extracted by two networks and demystifying the intrinsic mechanism of deep neural networks.

cs.LG

The Local Dimension of Deep Manifold

Based on our observation that there exists a dramatic drop for the singular values of the fully connected layers or a single feature map of the convolutional layer, and that the dimension of the concatenated feature vector almost equals the summation of the dimension on each feature map, we propose a singular value decomposition (SVD) based approach to estimate the dimension of the deep manifolds for a typical convolutional neural network VGG19. We choose three categories from the ImageNet, namely Persian Cat, Container Ship and Volcano, and determine the local dimension of the deep manifolds of the deep layers through the tangent space of a target image. Through several augmentation methods, we found that the Gaussian noise method is closer to the intrinsic dimension, as by adding random noise to an image we are moving in an arbitrary dimension, and when the rank of the feature matrix of the augmented images does not increase we are very close to the local dimension of the manifold. We also estimate the dimension of the deep manifold based on the tangent space for each of the maxpooling layers. Our results show that the dimensions of different categories are close to each other and decline quickly along the convolutional layers and fully connected layers. Furthermore, we show that the dimensions decline quickly inside the Conv5 layer. Our work provides new insights for the intrinsic structure of deep neural networks and helps unveiling the inner organization of the black box of deep neural networks.

cs.CV

On the Computation Power of Name Parameterization in Higher-order Processes

Parameterization extends higher-order processes with the capability of abstraction (akin to that in lambda-calculus), and is known to be able to enhance the expressiveness. This paper focuses on the parameterization of names, i.e. a construct that maps a name to a process, in the higher-order setting. We provide two results concerning its computation capacity. First, name parameterization brings up a complete model, in the sense that it can express an elementary interactive model with built-in recursive functions. Second, we compare name parameterization with the well-known pi-calculus, and provide two encodings between them.

cs.LO