%0 Journal Article
%T 用于反应系统的修改时序逻辑
%A 贾国平？
%A 郑国梁？
%J 软件学报
%P 663-672
%D 1997
%X 本文提出了一个用于反应系统规范及验证的修改时序逻辑．它包含一个用于显示区分程序执行步同环境执行步的机制．环境的特性可以在系统开发时进行考虑．文中首先给出了程序的一个可复合计算模型──模块转换系统．基于此模型，给出了修改时序逻辑以及它的证明规则．本文提出的方法基于manna－pnueli的时序逻辑框架．经典的资源分配问题的例子用于说明此方法．最后给出了并行复合原理，它可以看成是abadi和lamport的关于复合假设／保证规范研究工作的具体应用．
%K 反应系统
%K 时序逻辑
%K 规范
%K 验证
%K 模块转换系统
%K 资源分配问题
%K 并行复合
%K 假设／保证规范
%U http://www.jos.org.cn/ch/reader/view_abstract.aspx?file_no=19970904&flag=1