Acta Metallurgica Sinica(English letters) ›› 2014, Vol. 21 ›› Issue (4): 96-104.doi: 10.1016/S1005-8885(14)60322-8

• Others • 上一篇    

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

闫永义1,陈增强1,刘忠信2   

  1. 1. College of Computer and Control Engineering, Nankai University, Tianjin 300071, China 2. College of Science, Civil Aviation University of China, Tianjin 300300, China
  • 收稿日期:2013-12-12 修回日期:2014-06-14 出版日期:2014-08-31 发布日期:2014-08-30
  • 通讯作者: 闫永义 E-mail:yyyan@mail.nankai.edu.cn
  • 基金资助:

    国家自然科学基金;教育部新世纪杰出人才计划;天津市自然科学基金

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

  1. 1. College of Computer and Control Engineering, Nankai University, Tianjin 300071, China 2. College of Science, Civil Aviation University of China, Tianjin 300300, China
  • Received:2013-12-12 Revised:2014-06-14 Online:2014-08-31 Published:2014-08-30
  • Supported by:

    National Natural Science Foundation of China;Ministry of Education program for New Century Excellent Talents;Tianjin Natural Science Foundation of China

摘要: 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 an algebraic equation of the states and inputs, in which the matrix product is STP. By such algebraic formulation, three 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.

关键词: SVA, recognition power, matrix approach, STP matrices

Abstract: 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 an algebraic equation of the states and inputs, in which the matrix product is STP. By such algebraic formulation, three 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.

Key words: SVA, recognition power, matrix approach, STP matrices