arXiv subjects

Zining Cao

Publications and source records attributed to Zining Cao.

8 recordsLinked to original sources

arXiv2026

On Generalized Performance Evaluation and Generalized Controller Synthesis

In this paper, we propose the frameworks of generalized performance evaluation and generalized controller synthesis. To this end, we give a true concurrent process calculus as the model of systems, and present a lattice-valued performance evaluation language as the performance specification of systems. We give a framework of generalized performance evaluation based on the process calculus and the performance evaluation language. We show that the several problems in computer science are special cases of generalized performance evaluation. A generalized performance evaluation algorithm is presented. Furthermore, we present a framework of generalized controller synthesis, which is the inverse problem of generalized performance evaluation. We show several special cases of generalized controller synthesis in computer science, and give an outline of generalized controller synthesis algorithm.

cs.LO↗

arXiv2025

Controller synthesis method for multi-agent system based on temporal logic specification

Controller synthesis is a theoretical approach to the systematic design of discrete event systems. It constructs a controller to provide feedback and control to the system, ensuring it meets specified control specifications. Traditional controller synthesis methods often use formal languages to describe control specifications and are mainly oriented towards single-agent and non-probabilistic systems. With the increasing complexity of systems, the control requirements that need to be satisfied also become more complex. Based on this, this paper proposes a controller synthesis method for semi-cooperative semi-competitive multi-agent probabilistic discrete event systems to solve the controller synthesis problem based on temporal logic specifications. The controller can ensure the satisfaction of specifications to a certain extent. The specification is given in the form of a linear temporal logic formula. This paper designs a controller synthesis algorithm that combines probabilistic model checking. Finally, the effectiveness of this method is verified through a case study.

cs.MA↗

arXiv2025

On Higher Order Busy Beaver Function

In this paper, we extend Busy Beaver function to a class of higher order Busy Beaver functions based on Turing oracle machine. We prove some results about the relation between decidability of number theoretical formula and higher order Busy Beaver functions, and the relation between computability of max-min partial recursive functions and higher order Busy Beaver functions. We also present some conjectures on higher order Busy Beaver functions.

cs.CC↗

arXiv2025

A Complete Mental Temporal Logic for Intelligent Agent

In this paper, we present a complete mental temporal logic, called BPICTL, which generalizes CTL by introducing mental modalities. A sound and complete inference system of BPICTL is given. We prove the finite model property of BPICTL. Furthermore, we present a model checking algorithm for BPICTL.

cs.LO↗

arXiv2025

Model Checking for Multi-Agent Systems Modeled By Epistemic Process Calculus

This paper presents a comprehensive framework for modeling and verifying multi-agent systems. The paper introduce an Epistemic Process Calculus for multi-agent systems, which formalizes the syntax and semantics to capture the essential features of agent behavior interactions and epistemic states. Building upon this calculus, we propose ATLE, an extension of Alternating-time Temporal Logic incorporating epistemic operators to express complex properties related to agent epistemic state. To verify ATLE specifications, this paper presents a model checking algorithm that systematically explores the state space of a multi-agent system and evaluates the satisfaction of the specified properties. Finally, a case study is given to demonstrate the method.

cs.FL↗

arXiv2020

Formal modeling and performance evaluation for hybrid systems:a probabilistic hybrid process algebra-based approach

Probabilistic behavior is omnipresent in computer controlled systems, in particular, so-called safety-critical hybrid systems, because of various reasons, like uncertain environments, or fundamental properties of nature. In this paper, we extend existing hybrid process algebra $ACP_{hs}^{srt}$ with probability without replacing nondeterministic choice operator. In view of some shortcomings in existing approximate probabilistic bisimulation, we relax the constrains and propose a novel approximate probabilistic bisimulation relation. After that, we present a performance evaluation language, CTRML, to reason over probabilistic systems, which extend the results to real number. Along with the specification language, we present a set of algorithms for the evaluation of the language. Additionally, we transfer the hybrid process algebra to probabilistic transition system and show experimental results.

cs.FL↗

arXiv2014

Refinement Checking for Multirate Hybrid ZIA

A hybrid system is a dynamical system with both discrete and continuous components. In order to study the modeling and verification aspects of hybrid system, in this paper we first introduce a specification approach combining interface automata, initialized multirate hybrid automata and Z language, which is named MZIA. Meanwhile we propose a refinement relation on MZIAs. Then we give an algorithm for checking refinement relation between MZIAs with finite domain and demonstrate the correctness of the algorithm.

cs.LO↗

arXiv2012

Reducing Higher Order Pi-Calculus to Spatial Logics

In this paper, we show that theory of processes can be reduced to the theory of spatial logic. Firstly, we propose a spatial logic SL for higher order pi-calculus, and give an inference system of SL. The soundness and incompleteness of SL are proved. Furthermore, we show that the structure congruence relation and one-step transition relation can be described as the logical relation of SL formulae. We also extend bisimulations for processes to that for SL formulae. Then we extend all definitions and results of SL to a weak semantics version of SL, called WL. At last, we add mu-operator to SL. This new logic is named muSL. We show that WL is a sublogic of muSL and replication operator can be expressed in muSL.

cs.LO↗