PSL构造双向交换自动机及非确定自动机的方法

PSL(property specification language)是一种用于描述并行系统的属性规约语言,包括线性时序逻辑FL(foundation language)和分支时序逻辑OBE(optional branching extension)两部分.由于OBE就是CTL(computation tree logic),并且具有时钟声明的公式很容易改写成非时钟公式,因此重点研究了非时钟FL逻辑.为便于进行模型检验,每个FL公式必须转化成为一种可验证形式,通常是自动机(非确定自动机).构造非确定自动机的过程主要是通过中间构建交换自动机来实现.详细给出了由非时钟FL构造双向交换自动机的构造规则.构造规则的核心逻辑不仅仅局限于是在LTL(linear temporal logic)基础上的正规表达式,而且全面而充分地考虑了各种FL操作算子的可能性.并且给出了将双向交换自动机转化为非确定自动机的一种方法.最后,编写了将PSL转化为上述自动机的实现工具.FL双向交换自动机的构造规则计算复杂度仅是FL公式长度的线性表达式,验证了构造规则的正确性.在此基础上,证明了双向交换自动机与其转化的等价的非确定自动机接受的语言相同.上述工作对解决复杂并行系统建模和模型验证问题具有重要的理论意义和应用价值.

仿真非确定性计算模型

逻辑程序设计模型的一个特性是它的非确定性,而Prolog语言所具有的非确定性对于编写非确定性计算模型的解释程序提供了坚实的语言基础,通过几个非确定性机的仿真程序,对于实现其他一些计算模型的仿真具有很好的借鉴意义。

判定非确定离散事件系统稳定性的多项式复杂度算法

本文讨论基于非确定自动机/形式语言模型的非确定离散事件系统稳定性的多项式算法.在引入拟距离的概念之后,根据拟距离形式化地定义了非确定离散事件系统稳定性.以往判定非确定离散事件系统稳定性的算法基于系统的观测器实现,该观测器在结构上具有指数复杂度,因此本文分析系统结构和观测器结构之间的关系,基于对系统状态对的讨论,提出了判定系统稳定性的有效多项式搜索算法.

判定非确定离散事件系统稳定性的梯度搜索算法

讨论基于非确定自动机/形式语言模型的非确定离散事件系统(NDES)稳定性问题.引入非确定离散事件系统稳定性的定义,并得到了稳定性的判据定理.给出了基于梯度的搜索算法,该算法可有效消除观测器的冗余,从而降低了计算复杂度.