petri网理论及其应用 0 形式化表示

楔子

热点必须要了解，结合趋势。

为什么要形式化方法

形式化方法的研究高潮始于 20世纪60年代后期，针对当时所谓“软件危机”,人们提出种种解决方法,归纳起来有两类：一是采用工程方法来组织、管理软件的开发过程；二是深入探讨程序和程序开发过程的规律，建立严密的理论，以其用来指导软件开发实践。前者导致“软件工程”的出现和发展，后者则推动了形式化方法的深入研究。

形式化方法的基本含义是借助数学的方法来研究CS中的有关问题。目的是为开发过程提供一些技术和工具，用于发现并指出软件实现中潜在的缺陷问题。数学是完美的，无二义性的，可以用在航空航天工程中，当然工业界也在慢慢的从软件测试逐步变为形式化方法。

什么是形式化方法

根据表达能力，形式化方法可以分为五类：

基于模型的方法：通过明确定义状态和操作来建立一个系统模型（使系统从一个状态转换到另一个状态）。用这种方法虽可以表示非功能性需求（诸如时间需求），但不能很好地表示并发性。如：Z语言，VDM，B方法等。
基于逻辑的方法：用逻辑描述系统预期的性能，包括底层规约、时序和可能性行为。采用与所选逻辑相关的公理系统证明系统具有预期的性能。用具体的编程构造扩充逻辑从而得到一种广谱形式化方法，通过保持正确性的细化步骤集来开发系统。如：ITL（区间时序逻辑），区段演算（DC），hoare 逻辑，WP演算，模态逻辑，时序逻辑，TAM（时序代理模型），RTTL（实时时序逻辑）等。
代数方法：通过将未定义状态下不同的操作行为相联系，给出操作的显式定义。与基于模型的方法相同的是，没有给出并发的显式表示。如：OBJ， Larch族代数规约语言等；
进程代数方法：通过限制所有容许的可观察的过程间通信来表示系统行为。此类方法允许并发过程的显式表示。如：通信顺序过程（CSP），通信系统演算（CCS），通信过程代数（ACP），时序排序规约语言（LOTOS），计时CSP(TCSP），通信系统计时可能性演算（TPCCS）等。
基于网络的方法：由于图形化表示法易于理解，而且非专业人员能够使用，因此是一种通用的系统确定表示法。该方法采用具有形式语义的图形语言，为系统开发和再工程带来特殊的好处。如 Petri图，计时Petri图，状态图等。

形式化语言与自动机

以四类形式语言（短语结构语言、上下文有关语言、上下文无关语言、正则语言）

四种自动机（有穷自动机、下推自动机、图灵机、线性有界自动机）

自动机

自动机是有限状态机(FSM)的数学模型。

在编译当中有所应用。自动机描述的是顺序的，线性的。

有限自动机是指有限个状态，在语法，词法分析中有用到。编译解决的主要是上下文无关文法，日常生活中所用的语言是上下文有关的文法。科大讯飞在解决日常语言识别时使用到了大数据。

λ-演算与图灵机

这两者是等价的，都是回答了计算机可计算的边界这一问题。

不同的是，λ-演算使用的是数学的演算，而图灵机则是具有了一个物理的模型。