講座名稱：Detectability of discrete-event systems

講座人：張奎澤

講座時間：12月4日14:30-16:00

地點：網絡與安全創(chuàng)新研究大樓 A1236室

講座人介紹：

張奎澤，分別于2009年和2014年在哈爾濱工程大學取得數(shù)學學士學位和控制科學與工程博士學位?，F(xiàn)在中國科學院數(shù)學與系統(tǒng)科學研究院作訪問學者。2015年至2024年期間工作經歷先后包括：哈爾濱工程大學副教授，中國科學院數(shù)學與系統(tǒng)科學研究院博士后，德國慕尼黑工業(yè)大學博士后，瑞典皇家理工學院博士后，德國柏林工業(yè)大學洪堡學者，英國薩里大學講師，意大利卡利亞里大學訪問教授。

研究興趣主要為理論計算機科學和控制論。主要研究題目為多種動態(tài)系統(tǒng)中基本性質的形式化驗證和綜合。所研究的系統(tǒng)包括布爾控制網絡、有限自動機、Petri網、定時自動機，幺半群上的加權有限自動機。提出布爾控制網絡的能觀性圖，離散事件系統(tǒng)的新框架，幺半群上的加權有限自動機。以第一作者出版Springer Nature專著一部，以獨立作者出版Foundations and Trends in Systems and Control專著一部。發(fā)表40篇期刊論文（多篇論文發(fā)表在控制論頂級期刊和理論計算機科學頂級期刊中）和30多篇會議論文。

講座內容：

Detectability of partially-observed dynamical systems is a basic property which means that one can use observed output sequences to determine the current and subsequent states. The state detection problem dates back to E.F. Moore’s Gedanken-experiments in 1956 on sequential machines which were called Moore machines later. The basic definitions of strong detectability and weak detectability in discrete-event systems modeled by labeled finite-state automata were given by Shu and Lin in 2007. In this talk, we will firstly review the classical polynomial-time verification algorithm for strong detectability of labeled finite-state automata given by S. Shu and F. Lin in 2011 based on two fundamental assumptions of (1) deadlock-freeness (an automaton will always run) and (2) having no reachable unobservable cycle (the running of an automaton will eventually be observed). Shu and Lin’s algorithm was derived based on their detector method. Secondly, we will introduce our new polynomial-time verification algorithm (collaborated with A. Giua) by developing a concurrent-composition method without any assumption, thus rewriting the fundamental results on detectability.

主辦單位：數(shù)學與交叉科學研究院