论文部分内容阅读
该文中,研究人员提出了一种二元的方法用来对并发系统进行建模和推理证明.在该方法中,研究人员将Petri网和时序逻辑结合在一起.其中,Petri网模型用来对并发系统的行为和结构进行建模和规约,而时序逻辑则用来形式化的表达和证明Petri网中的逻辑性质.研究选用一种称之为代数系统网的Petri网模型来作为形式化的建模规约工具;之后,在Unity逻辑的基础上提出了一种方法用来规约和证明代数系统网模型的逻辑性质.研究人员定义了一种简化的代数系统网及其偏序运行的概念.并提出了一种网性质的规约及证明方法.