有限状态机及其扩展

刻符j)， j有Q。限，在状那这态么里机下规处一定于时q某刻=一将状处(q态于，q一i)个Q；确，定并的接状收态一q个 =输入(字qi， ④ q0 Q是初始状态，有限状态机由此状态开始接收输入； ⑤ F Q是终结状态集合，有限状态机在达到终结态后不
再接收输入。
6
（1） 基本概念
：字母表 字符串：字母表上的字符组成的有限序列（为空串） 语言：字母表上的字符串的集合
A
A 1
C
2
B
3
A
4
B,C
终结状态
身份认证系统 （合法身份：ABA） accepting state
状态集合Q = {1, 2, 3, 4} ； 初始状态 q0 = 1； 终结状态集合 F = {4}； 输入集合 = {A, B, C} 状态转移关系集合 (1,A)=2；(1,B)=1；(1,C) =1；(2,A)=2；(2,B)=3；
前
后
缓
缓
冲
冲
区
区
状态集合Q = {closed, open}；初始状态 q0 = closed； 输入集合 = {front, rear, both, neither}
状态转移关系集合 (closed, rear) =closed；(closed,both)=closed； (closed, neither)=closed；(closed,front)=open； (open, rear) = open； (open,both) =open； (open, front) = open；(open, neither) = closed
closed：闭合状态； open：打开状态；front：前缓冲区有顾客；rear：后缓冲区有顾客； both = front rear：前、后缓冲区都有顾客； neither = front rear：前、后缓冲区都无顾客
（1） 基本概念
inc
0 inc dec
1 dec
dec inc 2
带输出的自动机器模型，按照输出的不同分成两 类：输出与状态有关—Moore机；输出与状态和 输入有关—Mealy机。
11
（2） Moore机
Moore机形式定义为六元组M = (Q, , , , , q0)，其中
超级商场的自动门控制器 自动门的前、后分别有两个缓
冲区。自动门的前缓冲区用来检测是否有人接近。自动门
的后缓冲区，使得控制器把门打开足够长的时间让人走进
去，并且不让门在打开的时候碰到站在它附近的人。自动
门控制器依据前缓冲区、后缓冲区的检测信息给出打开或 闭合的动作指令。
前
后
自动门的动作控制应满足如下要求（规格）：
Chapter 2 有限状态机及其扩展
有限状态机
有限状态机是有限计算的基本模型，也 是许多形式化规格、验证方法的基础模 型。
Statecharts
Statecharts是通过定义递阶状态、状 态的AND或OR分解等高级特性的有限 状态机的一种扩展形式。
1
（一） 有限状态机
（1） 基本概念
有限状态机（finite state machine）或有限自动机 （finite automata）是有限计算的基本模型，是许多形式化 规格、验证方法的基础模型。
inc：增加1 dec：减少1
模3计数器
状态集合Q = {0, 1, 2} ； 初始状态 q0 = 0； 输入集合 = {inc, dec} 状态转移关系集合
(0,inc)=1；(0,dec)=2；(1,inc)=2；(1,dec)=0；(2,inc)=0；(2,dec)=1
4
（1） 基本概念
B,C
当={a,b}，{aabb,ab,abab,bba},{}等都是上的语言 有限状态机接受的语言：L(M)={x|(q0,x) F}
有限状态机可用四元组 , )来表示。
M
=
(Q,
,
,
ቤተ መጻሕፍቲ ባይዱq0)或三元组
M
=
(Q,
状态转移函数:刻画其行为的最关键部分, 一个从Q到Q 的二元函数。状态转移函数通常可以用关系矩阵、状 态转移表或状态转移图的形式来表示。
缓
缓
冲
冲
① 当前缓冲区和后缓冲区均无顾客出现，则自动门处于
区
区
闭合状态；
② 当后缓冲区有顾客出现，则自动门维持其原有状态；
③ 当前缓冲区有顾客且后缓冲区无顾客，则打开自动门。
2
（1） 基本概念
both,rear,neither closed
both,rear,front front
neither
open
(2,C) =1；(3,A) =4；(3,B)=1；(3,C) =1
ABCACA
AABCABA
(1,AB)=3
5
（1） 基本概念
有限状态机是一个五元组 M = (Q, , , q0, F)，其中
① Q刻=，有{q限0,状q态1,…机,只q能n}处是于有一限个状确态定集的合状。态在q任i；一确定的时 ② 的=时刻{，1,有2限,…状,态机m}只是能有接限收输一入个字确符定集的合输。入在任j；一确定 ③ ：Q Q是状态转移函数。如果在某一确定的时
7
（1） 基本概念
状态转移矩阵 用行表示状态机所处的当前状 态，列表示将要到达的下一个状态，行列交叉 处表示输入字符。称该矩阵为转移函数的关 系矩阵，或者有限状态机M的状态转移矩阵。
inc
0
1
dec
inc dec
dec inc
2
0
0 1 dec
12
inc dec inc
2 inc dec
状态转移矩阵
inc
模3计数器
0 inc dec
1 dec
dec inc 2
状态转移图
10
（1） 基本概念
前面讨论的有限状态机，可以看作仅接受输入符 号并发生状态改变，但无任何输出的自动机器。
现实生活中的许多有限状态系统,对于不同的输入 信号，除内部状态不断改变外，还不断向系统外 部输出各种信号。
将有限状态机进行推广，引出具有输出机制的自 动机器模型。
模3计数器
8
状态转移表 用表格的行表示状态机所处的当 前状态，列表示当前的输入字符，行列交叉处 表示要到达的下一个状态。
inc
0
1
dec
inc dec
dec inc
2
模3计数器
输入字符 状态 inc dec
0
12
1
20
2
01
状态转移表
9
状态转移图 用圆圈（结点）表示状态；将存 在转移关系的状态用有向弧连接，并标注相应 的输入字符在有向弧旁；用标有箭头的结点表 示初始状态；属于终结状态集中的状态用双圈 表示。