Z-自动机与分划逻辑

Z Automata and Partition Logics

本文分解Ｚ自动机成为ω自动机偶的复合；建立了Ｚ的Ｌ（ＭＰ）理论，利用Ｚ自动机的技巧证明了Ｚ的Ｌ（ＭＰ）理论的可判定性．作为应用，证明了有限状态过程的正确性问题是可判定的．

This paper divides Z automata into pairs of ω automata, develops the L(MP) theory of Z . Using the technique of Z automata, it proves that the L (MP) theory of Z is decidable. As an application it also proves that the correctness problem for the finite state process is decidable.