Abstract Matrix product states (MPS) are a standard tensor-network representation for ground states of one-dimensional quantum many-body systems, and they underpin widely used simulation tools such as DMRG. However, while quantum model checking has been developed mainly for quantum programs and communication protocols (with properties expressed along a time axis), there is still no comparable framework for systematically verifying spatial and size-dependent properties of physical many-body states, where the key parameter is the system size. This paper takes a step toward bridging the gap. We propose Linear Chain Logic (LCL), a spatial logic designed to specify physically meaningful properties of periodic MPS families as the system size grows, such as nontriviality on rings and large-size asymptotic patterns. Our approach builds on a simple but powerful connection: every periodic MPS naturally induces a completely positive map (a quantum operation) on its virtual space, so many quantitative features of the MPS can be analysed through the repeated application of the operation. Using this perspective, we derive an effective procedure to compute the inner products of an MPS at a given size and to support richer LCL specifications, without relying on brute-force state expansion. We then develop approximate model-checking algorithms that combine sound bounding with asymptotic structural analysis, enabling scalable reasoning about large system sizes. Experiments on representative MPS families illustrate that our method can automatically verify nontriviality and detect asymptotic spatial regimes in a way that complements traditional numerical techniques.

Verifying quantum systems has attracted a lot of interest in the last decades.In this paper, we study the quantitative model-checking of quantum continuous-time Markov chains (quantum CTMCs). The branching-time properties of quantum CTMCs are specified by continuous stochastic logic (CSL), which is well-known for verifying real-time systems, including classical CTMCs. The core of checking the CSL formulas lies in tackling multiphase until formulas. We develop an algebraic method using proper projection, matrix exponentiation, and definite integration to symbolically calculate the probability measures of path formulas. Thus the decidability of CSL is established. To be efficient, numerical methods are incorporated to guarantee that the time complexity is polynomial in the encoding size of the input model and linear in the size of the input formula. A running example of Apollonian networks is further provided to demonstrate our method.

Reachability analysis plays a central role in system design and verification. The reachability problem, denoted ◊jΦ, asks whether the system will meet the property Φ after some time in a given time interval j. Recently, it has been considered on a novel kind of real-time systems — quantum continuous-time Markov chains (QCTMCs), and embedded into the model-checking algorithm. In this paper, we further study the repeated reachability problem in QCTMCs, denoted □Ι◊jΦ, which concerns whether the system starting from each absolute time in Ι meet the property Φ after some coming relative time in j. First of all, we reduce it to the real root isolation of a class of real-valued functions (exponential polynomials), whose solvability is conditional to Schanuel’s conjecture being true. To speed up the procedure, we employ the strategy of sampling. The original problem is shown to be equivalent to the existence of a finite collection of satisfying samples. We then present a sample-driven procedure, which can effectively refine the sample space after each time of sampling, no matter whether the sample itself is satisfying or conflicting. The improvement on efficiency is validated by randomly generated instances. Hence the proposed method would be promising to attack the repeated reachability problems together with checking other ω -regular properties in a wide scope of real-time systems.

Federated learning (FL) is an attractive industrial paradigm to accomplish distributed artificial intelligence (AI) training collaboratively in a data privacy-preserving manner. Most existing designs for FL systems assume that industrial user equipments (UEs) participate voluntarily in FL training. However, since both AI model training and transmission consume considerable energy, UEs are reluctant to participate without economic rewards. Hence, the lack of proper economic reward incentive mechanism results in low UE utility and frustrates UEs' enthusiasm for participating in training. To address the above challenge, in this article, we propose a two-phase energy-aware reward incentive mechanism for the edge-cloud-assisted hierarchical federated learning (HFL) system to optimize the overall UE utility, thereby, incentivizing UEs to participate more actively. Specifically, at the cloud server phase, we design an energy quantity-aware incentive mechanism for reasonably distributing rewards to its sub-edge-assisted FL systems. Subsequently, at the edge server phase, based on the quantitative analysis for the optimal reward allocation solution, we develop an energy-aware water filling-based reward incentive mechanism to adapt to individual needs of UEs and maximize the overall UE utility. Experiments verify that, compared to well-known benchmarks, our incentive mechanism can improve the overall UE utility by up to 55.94% and better incentivize UEs to participate in training.

Verifying quantum programs has attracted a lot of interest in recent years. In this article, we consider the following two categories of termination problems of quantum programs with nondeterminism, namely: (1) (termination) Is an input of a program terminating with probability one under all schedulers? If not, how can a scheduler be synthesized to evidence the nontermination? (2) (universal termination) Are all inputs terminating with probability one under their respective schedulers? If yes, a further question asks whether there is a scheduler that forces all inputs to be terminating with probability one together with how to synthesize it; otherwise, how can an input be provided to refute the universal termination? For the effective verification of the first category, we over-approximate the reachable set of quantum program states by the reachable subspace, whose algebraic structure is a linear space. On the other hand, we study the set of divergent states from which the program terminates with probability zero under some scheduler. The divergent set also has an explicit algebraic structure. Exploiting these explicit algebraic structures, we address the decision problem by a necessary and sufficient condition, i.e., the disjointness of the reachable subspace and the divergent set. Furthermore, the scheduler synthesis is completed in exponential time, whose bottleneck lies in computing the divergent set reported for the first time. For the second category, we reduce the decision problem to the existence of an invariant subspace, from which the program terminates with probability zero under all schedulers. The invariant subspace is characterized by linear equations and thus can be efficiently computed. The states on that invariant subspace are evidence of the nontermination. Furthermore, the scheduler synthesis is completed by seeking a pattern of finite schedulers that forces all inputs to be terminating with positive probability. The repetition of that pattern yields the desired universal scheduler that forces all inputs to be terminating with probability one. All the problems in the second category are shown, also for the first time, to be solved in polynomial time. Finally, we demonstrate the aforementioned methods via a running example—the quantum Bernoulli factory protocol.

Magnetic resonance imaging (MRI) tasks often involve multiple contrasts. Recently, numerous deep learning-based multi-contrast MRI super-resolution (SR) and reconstruction methods have been proposed to explore the complementary information from the multi-contrast images. However, these methods either construct parameter-sharing networks or manually design fusion rules, failing to accurately model the correlations between multi-contrast images and lacking certain interpretations. In this paper, we propose a multi-contrast convolutional dictionary (MC-CDic) model under the guidance of the optimization algorithm with a well-designed data fidelity term. Specifically, we bulid an observation model for the multi-contrast MR images to explicitly model the multi-contrast images as common features and unique features. In this way, only the useful information in the reference image can be transferred to the target image, while the inconsistent information will be ignored. We employ the proximal gradient algorithm to optimize the model and unroll the iterative steps into a deep CDic model. Especially, the proximal operators are replaced by learnable ResNet. In addition, multi-scale dictionaries are introduced to further improve the model performance. We test our MC-CDic model on multi-contrast MRI SR and reconstruction tasks. Experimental results demonstrate the superior performance of the proposed MC-CDic model against existing SOTA methods. Code is available at https://github.com/lpcccc-cv/MC-CDic.

Pansharpening aims to sharpen low resolution (LR) multispectral (MS) images with the help of corresponding high resolution (HR) panchromatic (PAN) images to obtain HRMS images. Model-based pansharpening methods manually design objective functions via observation model and hand-crafted priors. However, inevitable performance degradation may occur in the case that the prior is invalid. Although many deep learning based end-to-end pansharpening methods have been proposed recently, they still need to be improved due to the insufficient study on HRMS related domain knowledge. Besides, existing pansharpening methods rarely consider the misalignments between MS and PAN images, leading to poor performance. To tackle these issues, this paper proposes to unrolling the observation model with registration embedding for pansharpening. Inspired by the optical flow estimation, we embed the registration operation into the observation model to reconstruct the pansharpening function with the help of a deep prior of HRMS images, and then unroll the iterative solution into a novel deep convolutional network.. Apart from the single HRMS supervision, we also introduce a consistency loss to supervise the two degradation processes. The use of consistency loss enables the degradation sub-networks to learn more realistic degradation. Experimental results at reduced-resolution and full-resolution are reported to demonstrate the superiority of the proposed method to other state-of-the-art pansharpening methods. In GaoFen-2 dataset evaluation, our method achieves 1.2dB higher PSNR than SOTA techniques.

Probabilistic model checking is a powerful method for analyzing quantitative properties of probabilistic systems. Its core is to calculate reachability probabilities. One prevalent method of computing these probabilities is value iteration, which performs one-way fixed point iteration to obtain an approximation to the true value but sometimes returns unreliable results. Three recently proposed sound methods – interval iteration, sound value iteration and optimistic value iteration – extended from value iteration ensure the accuracy of the returned results, and each method has its own merits and demerits. In this paper, we propose a new sound method called bisection value iteration. Our method accelerates bounds convergence through bisection together with upper/lower bound verification and can be applied to calculating reachability and expected rewards for Markov decision processes. The experiments show that our method performs well on a wide range of instances.

Modern vehicles are generally equipped with dozens of (or even hundreds of) electronic and intelligent devices and bloom into more involved information hub in enabling V2X networking. Protecting this increasingly complex vehicle ecosystem can be an arduous task, especially as the proliferation of data across distinct connected devices makes them more vulnerable than ever before. Intrusion detection systems (IDSs) have been found extremely rewarding in monitoring in-vehicle network traffic and detecting potential intrusions. The paper presents WLOF-InV, a novel unsupervised method based on local density for IDS on in-vehicle network. Given historical in-vehicle data of message identifiers, WLOF-InV first segments the traffic into a slice of (e.g., m) sliding windows. For each sliding window, WLOF-InV exerts information gain to select features for dimensionality reduction and squeezes out n features which are then bundled together to form a row vector and eventually gets an m*n matrix. WLOF-InV then adaptively determines the hyper parameters for local outlier factor (LOF) model (optimizing the scores for ranking the training data and the cutoff position for anomalies). In online detection, WLOF-InV determines the features by the information gain and invokes abnormal score weighting mode (which weights the LOF value of each dimension data by entropy method) to obtain the complete LOF score (of the overall traffic), and thereby grabs the anomaly traffic by resorting to the adjusted model. WLOF-InV is validated on the real data of three attack types (DoS, fuzzy, and impersonation). Experimental results demonstrate that WLOF-InV contrives next to optimal performance.

The notion of program sensitivity (aka Lipschitz continuity) specifies that changes in the program input result in proportional changes to the program output. For probabilistic programs the notion is naturally extended to expected sensitivity. A previous approach develops a relational program logic framework for proving expected sensitivity of probabilistic while loops, where the number of iterations is fixed and bounded. In this work, we consider probabilistic while loops where the number of iterations is not fixed, but randomized and depends on the initial input values. We present a sound approach for proving expected sensitivity of such programs. Our sound approach is martingale-based and can be automated through existing martingale-synthesis algorithms. Furthermore, our approach is compositional for sequential composition of while loops under a mild side condition. We demonstrate the effectiveness of our approach on several classical examples from Gambler's Ruin, stochastic hybrid systems and stochastic gradient descent. We also present experimental results showing that our automated approach can handle various probabilistic programs in the literature.

We consider a class of univariate real functions---poly-powers---that extend integer exponents to real algebraic exponents for polynomials. Our purpose is to isolate positive roots of such a function into disjoint intervals, which can be further easily computed up to any desired precision. To this end, we first classify poly-powers into simple and non-simple ones, depending on the number of linearly independent exponents. For the former, we present a complete isolation method based on Gelfond--Schneider theorem. For the latter, the completeness depends on Schanuel's conjecture. Finally experiential results demonstrate the effectivity of the proposed method.