CAJ | 학술논문

本文定义了量子线性时间属性，包括量子安全性，量子不变性，讨论了它们的关系和性质。结合测量一次、测量多次的单向量子有穷自动机，构建了两类乘积量子马尔可夫链，提出了基于自动机技术的量子正则安全性检测方法。通过验证乘积量子马尔可夫链的可达终状态来判断量子正则安全性的可满足性，并给出了可满足性的概率计算公式。作为应用，分析了广义量子loop程序，将程序终止归结为验证量子正则安全性的可满足性。
본문정의료양자선성시간속성，포괄양자안전성，양자불변성，토론료타문적관계화성질。결합측량일차、측량다차적단향양자유궁자동궤，구건료량류승적양자마이가부련，제출료기우자동궤기술적양자정칙안전성검측방법。통과험증승적양자마이가부련적가체종상태래판단양자정칙안전성적가만족성，병급출료가만족성적개솔계산공식。작위응용，분석료엄의양자loop정서，장정서종지귀결위험증양자정칙안전성적가만족성。
Quantum linear time property is defined ,including quantum safety property ,quantum invariant which their rela-tionships and properties are studied .Together with measure-one and measure many one way quantum finite automata ,two kinds of the product quantum markov chains are constructed ,the checking method of quantum regular propertyis provided based on automa-ton technique .This method shows the satisfaction of quantum regular safety is decided by the reachable termination verification of the product quantum markov chain ,and thecomputation formula of satisfaction probability is given .As an application example ,the generalized quantum loop program is analyzed .It shows the termination of program is turned into the satisfaction for the verification of quantum regular safety property .