论文部分内容阅读
本文提出了一个用于反应系统规范及验证的修改时序逻辑，它包含一个用于显示区分程序执行步同环境执行步的机制。环境的特性可以在系统开发时进行考虑。文中首先给出了程序的一个可复合计算模型－－－模块转换系统。基于此模型，给出了修改时序逻辑以及它的证明规则。本文提出了方法基于Ｍａｎｎａ－Ｐｎｕｅｌｉ的时序逻辑框架。经典的资源分配问题的例子用于此方法。最后给出了并行复合原理，它可以看成是Ａｂａｄｉ和Ｌａｍｐｏｒ