操作语义的结构方法

定义1. 一个转换系统 (ts) 仅仅是一个结构$⟨\mathrm{\Gamma },\to ⟩$, 其中$\mathrm{\Gamma }$是配置$\gamma$的集合, $\to \subseteq \mathrm{\Gamma }\times \mathrm{\Gamma }$被称为转换关系. $\gamma \to {\gamma }^{\prime }$应该被读作从配置$\gamma$到配置${\gamma }^{\prime }$的转换.

定义2. 一个终止转换系统 (tts) 是一个结构$⟨\mathrm{\Gamma },\to ,T⟩$, 其中$⟨\mathrm{\Gamma },\to ⟩$是一个ts, 而终配置集$T\subseteq \mathrm{\Gamma }$满足$\forall y\in T.\forall y^{\prime }\in \mathrm{\Gamma }.y\nrightarrow y^{\prime }$.

定义6. 一个标签转换系统 (lts) 是一个结构$⟨\mathrm{\Gamma },A,\to ⟩$, 其中$\mathrm{\Gamma }$是配置的集合, $A$是动作 (或者说标签或操作) 的集合, 并且$\to \subseteq \mathrm{\Gamma }\times A\times \mathrm{\Gamma }$是转换关系. 我们将一个转换记成$\gamma \stackrel{a}{\to }{\gamma }^{\prime }$, 其中$\gamma$和${\gamma }^{\prime }$是配置, $a$是动作. 动作给出了转换的内部或外部信息.

定义. 一个有限自动机是五元组$M=⟨Q,\mathrm{\Sigma },\delta ,q_0,F⟩$, 其中

• $Q$是状态的有限集合
• $\mathrm{\Sigma }$是有限的输入字母表
• $\delta :Q\times \mathrm{\Sigma }\to 𝒫(Q)$是状态转换关系
• $q_0\in Q$是初状态
• $F\subseteq Q$是终状态的集合

为了获得一个转换系统, 我们令$$\mathrm{\Gamma }=Q\times {\mathrm{\Sigma }}^{⁎}$$于是任意的配置$\gamma =⟨q,w⟩$的资料由一个状态分量$q$和一个控制分量$w$构成.
对于转换, 每当$q^{\prime }\in \delta (q,a)$, 我们置$$⟨q,aw⟩⊢⟨q^{\prime },w⟩$$有限自动机的行为不过就是其所接受的字符串的集合$L(M)$:$$L(M)=\{w\in {\mathrm{\Sigma }}^{⁎}|\exists q\in F.⟨q_0,w⟩{⊢}^{⁎}⟨q,\epsilon ⟩\}$$当然我们也可以定义终配置为$$T=\{⟨q,\epsilon ⟩|q\in F\}$$那么$$L(M)=\{w\in {\mathrm{\Sigma }}^{⁎}|\exists \gamma \in T.⟨q_0,w⟩{⊢}^{⁎}\gamma \}$$实际上我们可以更抽象一点. 令$⟨\mathrm{\Gamma },\to ,T⟩$是一个tts, 输入函数为$\mathrm{in}:I\to \mathrm{\Gamma }$而其所接受的语言是$L(\mathrm{\Gamma })\subseteq I$, 其中$$L(\mathrm{\Gamma })=\{i\in I|\exists \gamma \in T.\mathrm{in}(i){\to }^{⁎}\gamma \}$$对于有限自动机而言, 我们取$I={\mathrm{\Sigma }}^{⁎}$而$\mathrm{in}(w)=⟨q_0,w⟩$.