SearcharxivSearch

arXiv subjects

Zekun Ji

Publications and source records attributed to Zekun Ji.

6 recordsLinked to original sources

De Rham-Betti Groups of Type IV Abelian Fourfolds

We determine the de Rham--Betti (dRB) groups of several classes of abelian varieties over $\overline{\mathbb{Q}}$. We prove that $G_{\mathrm{dRB}}(A)=\mathrm{MT}(A)$ for every simple abelian fourfold of type IV. At present, much of what is known about the dRB structures of abelian varieties derives from W\"ustholz's Analytic Subgroup Theorem, whose applications primarily control linear relations among periods of $\mathrm{H}^{1}(A)$ and divisor-class information. In comparison with the theory of Hodge structures, our understanding of dRB structures remains limited. We therefore adopt an approach different from the method of Moonen-Zarhin for determining the Mumford-Tate groups of these abelian varieties. Depending on the endomorphism type of the abelian fourfold, we use Galois-theoretic analysis, van Geemen's half-twist construction, and positivity constraints arising from polarizations, as appropriate, to exclude proper reductive subgroups of the corresponding Mumford-Tate groups as candidates for the dRB groups. We also use results on periods due to Gross and Chudnovsky. This article is an expansion of the second part of the author's PhD thesis https://pure.uva.nl/ws/files/311471255/Thesis.pdf; see also https://arxiv.org/abs/2511.01072 by the author.

math.AG

Weight of the De Rham-Betti Structures of Abelian Varieties

In this note, we prove that for any abelian variety defined over $\overline{\mathbb{Q}}$, its de Rham-Betti (dRB) group necessarily contains $\mathbb{G}_{m}$ as the group of homotheties. Consequently, this rules out the existence of non-zero dRB classes in odd-degree cohomology groups of abelian varieties over $\overline{\mathbb{Q}}$. This generalises results of the first part of arXiv:2511.01072.

math.AG

De Rham-Betti Groups of Type IV Abelian Varieties

We study the de Rham-Betti structure of a simple abelian variety of type IV. We will take a Tannakian point of view inspired by André. The main results are that the de Rham-Betti groups of simple CM abelian fourfolds and simple abelian fourfolds over $\overline{\mathbb{Q}}$ whose endomorphism algebra is a degree 4 CM-field coincide with their Mumford-Tate groups. The method of proof involves a thorough investigation of the reductive subgroups of the Mumford-Tate groups of these abelian varieties, inspired by Kreutz-Shen-Vial. The condition that the underlying abelian variety is simple and the condition that the de Rham-Betti group is an algebraic group defined over $\mathbb{Q}$ are also used in a crucial way. The proof is different from the method of computing Mumford-Tate groups of these abelian varieties by Moonen-Zarhin. We will also study a family of de Rham-Betti structures, in the formalism proposed by Saito-Terasoma. For such families with geometric origin, we will characterize properties of fixed tensors of the de Rham-Betti group associated with such a family.

math.AG

Mars 2.0: A Toolchain for Modeling, Analysis, Verification and Code Generation of Cyber-Physical Systems

We introduce Mars 2.0 for modeling, analysis, verification and code generation of Cyber-Physical Systems. Mars 2.0 integrates Mars 1.0 with several important extensions and improvements, allowing the design of cyber-physical systems using the combination of AADL and Simulink/Stateflow, which provide a unified graphical framework for modeling the functionality, physicality and architecture of the system to be developed. For a safety-critical system, formal analysis and verification of its combined AADL and Simulink/Stateflow model can be conducted via the following steps. First, the toolchain automatically translates AADL and Simulink/Stateflow models into Hybrid CSP (HCSP), an extension of CSP for formally modeling hybrid systems. Second, the HCSP processes can be simulated using the HCSP simulator, and to complement incomplete simulation, they can be verified using the Hybrid Hoare Logic prover in Isabelle/HOL, as well as the more automated HHLPy prover. Finally, implementations in SystemC or C can be automatically generated from the verified HCSP processes. The transformation from AADL and Simulink/Stateflow to HCSP, and the one from HCSP to SystemC or C, are both guaranteed to be correct with formal proofs. This approach allows model-driven design of safety-critical cyber-physical systems based on graphical and formal models and proven-correct translation procedures. We demonstrate the use of the toolchain on several benchmarks of varying complexity, including several industrial-sized examples.

cs.PL

Formally Verified C Code Generation from Hybrid Communicating Sequential Processes

Hybrid Communicating Sequential Processes (HCSP) is a formal model for hybrid systems, including primitives for evolution along an ordinary differential equation (ODE), communication, and parallel composition. Code generation is needed to convert HCSP models into code that can be executed in practice, and the correctness of this conversion is essential to ensure that the generated code accurately reflects the formal model. In this paper, we propose a code generation algorithm from HCSP to C with POSIX library for concurrency. The main difficulties include how to bridge the gap between the synchronized communication model in HCSP and the use of mutexes for synchronization in C, and how to discretize evolution along ODEs and support interrupt of ODE evolution by communication. To prove the correctness of code generation, we define a formal semantics for POSIX C, and build transition system models for both HCSP and C programs. We then define an approximate bisimulation relation between traces of transition systems, and show that under certain robustness conditions for HCSP, the generated C program is approximately bisimilar to the original model. Finally, we evaluate the code generation algorithm on a detailed model for automatic cruise control, showing its utility on real-world examples.

cs.PL

Session Types With Multiple Senders Single Receiver (report version)

Message passing is a fundamental element in software development, ranging from concurrent and mobile computing to distributed services, but it suffers from communication errors such as deadlocks. Session types are a typing discipline for enforcing safe structured interactions between multiple participants. However, each typed interaction is restricted to having one fixed sender and one fixed receiver. In this paper, we extend session types with existential branching types, to handle a common interaction pattern with multiple senders and a single receiver in a synchronized setting, i.e. a receiver is available to receive messages from multiple senders, and which sender actually participates in the interaction cannot be determined till execution. We build the type system with existential branching types, which retain the important properties induced by standard session types: type safety, progress (i.e. deadlock-freedom), and fidelity. We further provide a novel communication type system to guarantee progress of dynamically interleaved multiparty sessions, by abandoning the strong restrictions of existing type systems. Finally, we encode Rust multi-thread primitives in the extended session types to show its expressivity, which can be considered as an attempt to check the deadlock-freedom of Rust multi-thread programs.

cs.PL