不确定性,非发散进程的单向模拟

摘要

本文主要讨论不确定性、非发散进程的单向模拟。与Ｒ．Ｍｉｌｎｅｒ的双向模拟不同的是，本文定义的模拟是单向的。我们给出了不确定性、非发散进程的转换规则，阐述了该类进程的失败语义，讨论了单向模拟的组合定律，证明了单向模拟的正确性，并谁进程向模拟的完备性是不存在的。文章最后讨论实现与规格说明间的单向模拟问题。