BZPEERPapers, people, evidence and research paths
Menu

Discover

SearchFind papers, people, topics, institutions and opportunities from one place.GraphSee how papers, authors, topics and evidence connect.

Research tools

HomeContinue from the papers, people and topics that matter now.CollectionsTurn saved papers into reading lists, evidence maps and shareable context.ResearchReconstruct the path that led you from search to paper to question.CollaborationMove from a paper, topic or expert request into a focused thread.PublishCreate full-text research articles with metadata, formulas and versions.

Network

ExpertsFind specialists whose work and reviews explain why they can help.CommunitiesJoin research groups organized around papers, topics and shared evidence.

Opportunities

ListingsBrowse roles, calls and collaborations connected to real research context.

Account

Log inReturn to your saved papers, graph views and active threads.Create accountStart saving papers, building a research trail and joining teams.
Log inCreate account

Source author record

Kuize Zhang

Kuize Zhang appears in the imported research catalog. Authorship, coauthor and topic links are available while profile ownership is still unclaimed.

ResearcherUnclaimed source record
math.OCFormal Languages and Automata TheoryCryptography and Securityeess.SYmath.RAProgramming LanguagesSystems and Control

Catalog footprint

What is connected

10works
7topics
4close collaborators

Actions

Connect this record

Log in to claim
Open graphBrowse works

Research graph

See the researcher in context

Open full explorer

Inspect adjacent papers, topics, institutions and collaborators without losing the researcher page.

Building this map preview

BZPEER is loading the nearby papers, people, topics and institutions for this page.

Published work

10 published item(s)

preprint2025arXiv

[Draft] High-order estimation-based properties and high-order observers for labeled finite-state automata

In this paper, we consider labeled finite-state automata (LFSAs), extend some state estimation-based properties from a single agent to a finite ordered set of agents. We also extend the notion of observer to \emph{high-order observer} using our \emph{concurrent composition}. As a result, a general framework for characterizing high-order estimation-based properties is built, in which each agent infers its preceding agent's estimation via all agents in front. The high-order observer plays the role of a basic tool to verify such properties. In more detail, in our general framework, the system's structure is publicly known to all agents $A_1,\dots,A_n$; each agent $A_i$ has its own observable event set $E_i$, and additionally knows all its preceding agents' observable events but can only observe its own observable events. The intuitive meaning of our high-order observer is to characterize what agent $A_n$ knows about what $A_{n-1}$ knows about \dots what $A_2$ knows about $A_1$'s state estimate of the system. This general framework can be regarded as an automata representation of dynamic epistemic logic. Compared with the classical representation of dynamic epistemic logic based on fragments of logic, our representation has advantages in property verification and flexibly changing agents to enforce properties. As case studies, this general framework applies to basic properties such as current-state opacity, strong current-state opacity, regular-language-based opacity, critical observability, high-order opacity, etc. Special cases for which verification can be done more efficiently are also discussed.

0 citations0 reviewsNo code linkedOpen access
preprint2022arXiv

Detectability of labeled weighted automata over monoids

In this paper, we for the first time obtain characterization of four fundamental notions of detectability for general labeled weighted automata over monoids (denoted by $\mathcal{A}^{\mathfrak{M}}$ for short), where the four notions are strong (periodic) detectability (SD and SPD) and weak (periodic) detectability (WD and WPD). Firstly, we formulate the notions of concurrent composition, observer, and detector for $\mathcal{A}^{\mathfrak{M}}$. Secondly, we use the concurrent composition to give an equivalent condition for SD, use the detector to give an equivalent condition for SPD, and use the observer to give equivalent conditions for WD and WPD, all for general $\mathcal{A}^{\mathfrak{M}}$ without any assumption. Thirdly, we prove that for a labeled weighted automaton over monoid $(\mathbb{Q}^k,+)$ (denoted by $\mathcal{A}^{\mathbb{Q}^k}$), its concurrent composition, observer, and detector can be computed in NP, $2$-EXPTIME, and $2$-EXPTIME, respectively, by developing novel connections between $\mathcal{A}^{\mathbb{Q}^k}$ and the NP-complete exact path length problem (proved by [Nykänen and Ukkonen, 2002]) and a subclass of Presburger arithmetic. As a result, we prove that for $\mathcal{A}^{\mathbb{Q}^k}$, SD can be verified in coNP, while SPD, WD, and WPD can be verified in $2$-EXPTIME. Finally, we prove that the problems of verifying SD and SPD of deterministic, deadlock-free, and divergence-free $\mathcal{A}^{\mathbb{N}}$ over monoid $(\mathbb{N},+)$ are both coNP-hard. The developed original methods will provide foundations for characterizing other fundamental properties (e.g., diagnosability, opacity) for $\mathcal{A}^{\mathfrak{M}}$. We also initially explore detectability in labeled timed automata, and prove that the SD verification problem is PSPACE-complete, while WD and WPD are undecidable.

0 citations0 reviewsNo code linkedOpen access
preprint2022arXiv

Synthesis for observability of logical control networks

Finite-state systems have applications in systems biology, formal verification and synthesis of infinite-state (hybrid) systems, etc. As deterministic finite-state systems, logical control networks (LCNs) consist of a finite number of nodes which can be in a finite number of states and update their states. In this paper, we investigate the synthesis problem for observability of LCNs based on state feedback with exogenous input by using the semitensor product proposed by Daizhan Cheng and the notion of observability graph (previously called weighted pair graph) proposed by us. We show that state feedback with exogenous input can either enforce or weaken observability of an LCN. We prove that for an LCN $Σ$ and another closed-loop LCN $Σ_{\mathcal{C}}$ obtained by feeding a state-feedback controller $\mathcal{C}$ with exogenous input into $Σ$, (1) if $Σ$ is observable, then $Σ_{\mathcal{C}}$ can be either observable or not; (2) if $Σ$ is not observable, $Σ_{\mathcal{C}}$ can also be observable or not. We also prove that if an unobservable LCN can be made observable by state feedback with exogenous input, then it can also be made observable by state feedback (without exogenous input, equivalent to state feedback with constant input). Furthermore, we give an upper bound on the number of state-feedback controllers that are needed to be tested in order to verify whether an unobservable LCN can be made observable by state feedback, and based on the procedure of obtaining the upper bound, we design an observability synthesis algorithm, by additionally combining the ideas of a greedy algorithm and dynamic programming. These results open the study of observability synthesis in LCNs.

0 citations0 reviewsNo code linkedOpen access
preprint2022arXiv

Verification of Strong K-Step Opacity for Discrete-Event Systems

In this paper, we revisit the verification of strong K-step opacity (K-SSO) for partially-observed discrete-event systems modeled as nondeterministic finite-state automata. As a stronger version of the standard K-step opacity, K-SSO requires that an intruder cannot make sure whether or not a secret state has been visited within the last K observable steps. To efficiently verify K-SSO, we propose a new concurrent-composition structure, which is a variant of our previously- proposed one. Based on this new structure, we design an algorithm for deciding K-SSO and prove that the proposed algorithm not only reduces the time complexity of the existing algorithms, but also does not depend on the value of K. Furthermore, a new upper bound on the value of K in K-SSO is derived, which also reduces the existing upper bound on K in the literature. Finally, we illustrate the proposed algorithm by a simple example.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

A unified method to decentralized state inference and fault diagnosis/prediction of discrete-event systems

The state inference problem and fault diagnosis/prediction problem are fundamental topics in many areas. In this paper, we consider discrete-event systems (DESs) modeled by finite-state automata (FSAs). There exist results for decentralized versions of the latter problem but there is almost no result for a decentralized version of the former problem. We propose a decentralized version of strong detectability called co-detectability which implies that once a system satisfies this property, for each generated infinite-length event sequence, at least one local observer can determine the current and subsequent states after a common observation time delay. We prove that the problem of verifying co-detectability of FSAs is coNP-hard. Moreover, we use a unified concurrent-composition method to give PSPACE verification algorithms for co-detectability, co-diagnosability, and co-predictability of FSAs, without any assumption or modifying the FSAs under consideration, where co-diagnosability is firstly studied by [Debouk & Lafortune & Teneketzis 2000], while co-predictability is firstly studied by [Kumar \& Takai 2010]. By our proposed unified method, one can see that in order to verify co-detectability, more technical difficulties will be met compared to verifying the other two properties, because in co-detectability, generated outputs are counted, but in the latter two properties, only occurrences of events are counted. For example, when one output was generated, any number of unobservable events could have occurred. The PSPACE-hardness of verifying co-diagnosability is already known in the literature. In this paper, we prove the PSPACE-hardness of verifying co-predictability.

0 citations0 reviewsNo code linkedOpen access
preprint2016arXiv

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].

0 citations0 reviewsNo code linkedOpen access
preprint2016arXiv

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.

0 citations0 reviewsNo code linkedOpen access
preprint2015arXiv

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.

0 citations0 reviewsNo code linkedOpen access
preprint2015arXiv

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.

0 citations0 reviewsNo code linkedOpen access
preprint2014arXiv

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.

0 citations0 reviewsNo code linkedOpen access