Searcharxiv⌕ Search

arXiv subjects

Kuize Zhang

Publications and source records attributed to Kuize Zhang.

25 records · Page 2Linked to original sources

Opacity of nondeterministic transition systems: A (bi)simulation relation approach

In this paper, we propose several opacity-preserving (bi)simulation relations for general nondeterministic transition systems (NTS) in terms of initial-state opacity, current-state opacity, K-step opacity, and infinite-step opacity. We also show how one can leverage quotient construction to compute such relations. In addition, we use a two-way observer method to verify opacity of nondeterministic finite transition systems (NFTSs). As a result, although the verification of opacity for infinite NTSs is generally undecidable, if one can find such an opacity-preserving relation from an infinite NTS to an NFTS, the (lack of) opacity of the NTS can be easily verified over the NFTS which is decidable.

cs.LO↗

Observability and reconstructibility of large-scale Boolean control networks via network aggregations

It is known that determining the observability and reconstructibility of Boolean control networks (BCNs) are both NP-hard in the number of nodes of BCNs. In this paper, we use the aggregation method to overcome the challenging complexity problem in verifying the observability and reconstructibility of large-scale BCNs with special structures in some sense. First, we define a special class of aggregations that are compatible with observability and reconstructibility (i.e, observability and reconstructibility are meaningful for each part of the aggregation), and show that even for this special class of aggregations, the whole BCN being observable/reconstructible does not imply the resulting sub-BCNs being observable/reconstructible, and vice versa. Second, for acyclic aggregations in this special class, we prove that all resulting sub-BCNs being observable/reconstructible implies the whole BCN being observable/reconstructible. Third, we show that finding such acyclic special aggregations with sufficiently small parts can tremendously reduce computational complexity. Finally, we use the BCN T-cell receptor kinetics model to illustrate the efficiency of these results. In addition, the special aggregation method characterized in this paper can also be used to deal with the observability/reconstructibility of large-scale linear (special classes of nonlinear) control systems with special network structures.

math.OC↗

A weighted pair graph representation for reconstructibility of Boolean control networks

A new concept of weighted pair graphs (WPGs) is proposed to represent a new reconstructibility definition for Boolean control networks (BCNs), which is a generalization of the reconstructibility definition given in [Fornasini & Valcher, TAC2013, Def. 4]. Based on the WPG representation, an effective algorithm for determining the new reconstructibility notion for BCNs is designed with the help of the theories of finite automata and formal languages. We prove that a BCN is not reconstructible iff its WPG has a complete subgraph. Besides, we prove that a BCN is reconstructible in the sense of [Fornasini & Valcher, TAC2013, Def. 4] iff its WPG has no cycles, which is simpler to be checked than the condition in [Fornasini & Valcher, TAC2013, Thm. 4].

math.OC↗

Basis for the linear space of matrices under equivalence

The semi-tensor product (STP) of matrices which was proposed by Daizhan Cheng in 2001 [2], is a natural generalization of the standard matrix product and well defined at every two finite-dimensional matrices. In 2016, Cheng proposed a new concept of semi-tensor addition (STA) which is a natural generalization of the standard matrix addition and well defined at every two finite-dimensional matrices with the same ratio between the numbers of rows and columns [1]. In addition, an identify equivalence relation between matrices was defined in [1], STP and STA were proved valid for the corresponding identify equivalence classes, and the corresponding quotient space was endowed with an algebraic structure and a manifold structure. In this follow-up paper, we give a new concise basis for the quotient space, which also shows that the Lie algebra corresponding to the quotient space is of countably infinite dimension.

math.OC↗

Polynomial representation for orthogonal projections onto subspaces of finite games

The space of finite games can be decomposed into three orthogonal subspaces [5], which are the subspaces of pure potential games, nonstrategic games and pure harmonic games. The orthogonal projections onto these subspaces are represented as the Moore-Penrose inverses of the corresponding linear operators (i.e., matrices) [5]. Although the representation is compact and nice, no analytic method is given to calculate Moore- Penrose inverses of these linear operators. Hence using their results, one cannot verify whether a finite game belongs to one of these subspaces. In this paper, jumping over calculating Moore-Penrose inverses of these linear operators directly, via using group inverses, in the framework of the semitensor product of matrices, we give explicit polynomial representation for these orthogonal projections and for potential functions of potential games. Using our results, one not only can determine whether a finite game belongs to one of these subspaces, but also can find an arbitrary finite game belonging to one of them. Besides, we give formal definitions for these types of games by using their payoff functions. Based on these results, more properties of finite games are revealed.

math.OC↗

Observability of Boolean control networks: A unified approach based on the theories of finite automata

The problem on how to determine the observability of Boolean control networks (BCNs) has been open for five years already. In this paper, we propose a unified approach to determine all the four types of observability of BCNs in the literature. We define the concept of weighted pair graphs for BCNs. In the sense of each observability, we use the so-called weighted pair graph to transform a BCN to a finite automaton, and then we use the automaton to determine observability. In particular, the two types of observability that rely on initial states and inputs in the literature are determined. Finally, we show that no pairs of the four types of observability are equivalent, which reveals the essence of nonlinearity of BCNs.

math.OC↗

High-order S-Lemma with application to stability of a class of switched nonlinear systems

This paper extends some results on the S-Lemma proposed by Yakubovich and uses the improved results to investigate the asymptotic stability of a class of switched nonlinear systems. Firstly, the strict S-Lemma is extended from quadratic forms to homogeneous functions with respect to any dilation, where the improved S-Lemma is named the strict homogeneous S-Lemma (the SHS-Lemma for short). In detail, this paper indicates that the strict S-Lemma does not necessarily hold for homogeneous functions that are not quadratic forms, and proposes a necessary and sufficient condition under which the SHS-Lemma holds. It is well known that a switched linear system with two sub-systems admits a Lyapunov function with homogeneous derivative (LFHD for short), if and only if it has a convex combination of the vector fields of its two sub-systems that admits a LFHD. In this paper, it is shown that this conclusion does not necessarily hold for a general switched nonlinear system with two sub-systems, and gives a necessary and sufficient condition under which the conclusion holds for a general switched nonlinear system with two sub-systems. It is also shown that for a switched nonlinear system with three or more sub-systems, the "if" part holds, but the "only if" part may not. At last, the S-Lemma is extended from quadratic polynomials to polynomials of degree more than $2$ under some mild conditions, and the improved results are called the homogeneous S-Lemma (the HS-Lemma for short) and the non-homogeneous S-Lemma (the NHS-Lemma for short), respectively. Besides, some examples and counterexamples are given to illustrate the main results.

math.OC↗