Verification analysis of self-verifying automata via semi-tensor product of matrices

作     者：YAN Yong-yi CHEN Zeng-qiang LIU Zhong-xin 

作者机构：College of Computer and Control Engineering Nankai University College of Science Civil Aviation University of China 

出 版 物：《The Journal of China Universities of Posts and Telecommunications》 (中国邮电高校学报（英文版）)

年 卷 期：2014年第21卷第4期

页      面：96-104页

核心收录：

学科分类：07[理学] 08[工学] 070104[理学-应用数学] 0701[理学-数学] 081202[工学-计算机软件与理论] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

基　　金：supported by the National Natural Science Foundation of China (61174094) the Tianjin Natural Science Foundation of China (14JCYBJC18700, 13JCYBJC17400) 

主　　题：SVA recognition power matrix approach STP matrices 

摘      要：The semi-tensor product （STP） of matrices was used in the article, as a new matrix analysis tool, to investigate the problem of verification of self-verifying automata （SVA）. SVA is a special variant of finite automata which is essential to nondeterministic communication with a limited number of advice bits. The status, input and output symbols are expressed in vector forms, the dynamic behaviour of SVA is modelled as matrix product is STP. By such algebraic formulation, three an algebraic equation of the states and inputs, in which the necessary and sufficient conditions are presented for the verification problem, by which three algorithms are established to find out all the strings which are accepted, rejected, or unrecognized by a SVA. Testing examples show the correctness of the results.