反应系统需要和环境频繁的发生作用且不会停止,具有以下特性:
A Kripke structure is a variation of the transition system, originally proposed by Saul Kripke,[1] used in model checking[2] to represent the behavior of a system. It is basically a graph whose nodes represent the reachable states of the system and whose edges represent state transitions. A labelling function maps each node to a set of properties that hold in the corresponding state. Temporal logics are traditionally interpreted in terms of Kripke structures. -wikipedia Kripke structure (model checking)
Kripke 结构即过渡(迁移)系统的变化,在模型检查中用来表示系统的行为,也可以用来描述上述的反应系统。Kripke 结构由状态集合(S)、过渡集合(R)以及标记函数(L)组成。该标记函数标记各状态下使得该状态为true的变量集合。Kripke 结构是一个状态过渡图,路径可以建模反应系统的计算。基于此,使用一阶逻辑公式形式化并发系统。 定义AP为一组原子命题,则Kripke结构M为在原子命题上的一个四元组M=(S,S0,R,L),其中