Zero-knowledge proof (ZKP) systems have surged attention and held a fundamental role in contemporary cryptography. Zero-knowledge succinct non-interactive argument of knowledge (zk-SNARK) protocols dominate the ZKP usage, implemented through arithmetic circuit programming paradigm. However, underconstrained or overconstrained circuits may lead to bugs. The former refers to circuits that lack the necessary constraints, resulting in unexpected solutions and causing the verifier to accept a bogus witness, and the latter refers to circuits that are constrained excessively, resulting in lacking necessary solutions and causing the verifier to accept no witness. This article introduces a novel approach for pinpointing two distinct types of bugs in ZKP circuits. The method involves encoding the arithmetic circuit constraints to polynomial equation systems and solving them over finite fields by the computer algebra system . The classification of verification results is refined, greatly enhancing the expressive power of the system. A tool, AC 4 , is proposed to represent the implementation of the method. Experiments show that AC 4 demonstrates an increase in the solved rate, showing a 36.7% improvement over Picus and CIVER, and a slight improvement over halo2-analyzer, a checker for halo2 circuits. Within a solvable range, the checking time has also exhibited noticeable improvement, demonstrating a magnitude increase compared to previous efforts.

This paper presents a cooperative control framework for dual-arm robots that integrates vision-language models (VLMs) with online reinforcement learning (RL) to enhance autonomy and adaptability in complex manipulation tasks. The proposed framework adopts a hierarchical architecture: at the top level, the VLM interprets natural language instructions and visual image to generate task plans; at the middle level, an online RL module refines manipulation policies and ensures adaptive decision-making under environmental uncertainty; and at the bottom level, compliant control based on trajectory planning and impedance regulation enables safe and robust execution. In the feedback, YOLOv5 is used to detect the object, GraspNet is used to obtain the optimal grasp pose, and CLIP (Contrastive Language-Image Pre-Training) is used to judge whether task is completed. Simulations and real-world experiments validate the effectiveness of the proposed method. The dual-arm robot successfully performed various cooperative tasks such as grasping, bottle-cap unscrewing, water pouring, and box carrying, achieving an increase in the task success rate from 43% to 100% with online adaptive learning and training. These results demonstrate that the proposed framework effectively bridges high-level reasoning with low-level control, providing a scalable solution for future applications in service robotics, industrial automation, and human-robot collaboration.

Due to the general undecidable results, verification of concurrent programs is a big challenge. Most existing verifiers adopt Petri net and its extensions based on abstraction and approximation as their verification models, which yet suffer from intractable complexity and are thus challenging to be efficient and complete. We choose Basic Parallel Process (BPP) , a subclass of Petri nets, as the backbone verification model for verifying concurrent programs due to its lower complexity. We propose BPPChecker, the first model checker for verifying a subclass of CTL on BPP. A constraint-based algorithm is given in which formulas are handled by SMT solver Z3. Our approach involves introducing a k -step semantics for the EG operator. By doing so, we reduce the problem of deciding the satisfiability of EG -formulas and EF 1 -formulas to the problem of deciding the satisfiability of linear integer arithmetic formulas. Besides, we encode the Actor Communicating System (ACS) , a program model for asynchronously communicating programs, to BPP. Experimental results show that BPPChecker performs more efficiently than the existing tools for a series of branching-time property verification problems of Erlang programs.

An $\mathsf{F}_{d}$ upper bound for the reachability problem in vector addition systems with states (VASS) in fixed dimension is given, where $\mathsf{F}_d$ is the $d$-th level of the Grzegorczyk hierarchy of complexity classes. The new algorithm combines the idea of the linear path scheme characterization of the reachability in the $2$-dimension VASSes with the general decomposition algorithm by Mayr, Kosaraju and Lambert. The result improves the $\mathsf{F}_{d + 4}$ upper bound due to Leroux and Schmitz (LICS 2019).

Knowledge graphs are used extensively in various fields. Labor-intensive and time-consuming error detection for large-scale knowledge graphs significantly increases the need for efficient model checking algorithms in large-scale graphs. Since conventional algorithms are inefficient on such graphs, we propose a new liveness algorithm of knowledge graphs, under a specific given set of labels. By trimming and marking the graphs alternately, a weakly connected components algorithm is then designed to separate graphs into several disjoint sets and a bidirectional forward-backward algorithm computes strongly connected components in each set in parallel. We have implemented our algorithm on a real medical knowledge graph and several open data sets. The evaluation shows that our algorithm achieves up to 11.2x speedup over conventional algorithm with 16 threads.