전이 시스템

2. 형식적 정의

형식적으로, '''전이 시스템'''은 $(S,\; T)$ 쌍으로, 여기서 $S$는 상태 집합이고 $T$, 즉 ''전이 관계''는 $S\; \backslash times\; S$의 부분 집합이다. 상태 $p$에서 상태 $q$로의 전이가 존재하면 $(p,\; q)\; \backslash in\; T$라고 하며, 이를 $p\; \backslash rightarrow\; q$로 표기한다.

'''레이블 전이 시스템'''은 튜플 $(S,\; \backslash Lambda,\; T)$로, 여기서 $S$는 상태 집합, $\backslash Lambda$는 레이블 집합이고, $T$는 ''레이블 전이 관계''로 $S\; \backslash times\; \backslash Lambda\; \backslash times\; S$의 부분 집합이다. 상태 $p$에서 레이블 $\backslash alpha$를 가진 상태 $q$로의 전이가 있으면 $(p,\; \backslash alpha,\; q)\; \backslash in\; T$라고 하며, 이를 다음과 같이 표기한다.

:$$

p \xrightarrow{\alpha} q \,.



레이블은 관심 있는 언어에 따라 다른 것을 나타낼 수 있다. 레이블의 일반적인 용도로는 예상되는 입력, 전이를 트리거하기 위해 참이어야 하는 조건, 또는 전이 중에 수행되는 동작을 나타내는 것이 있다. 레이블 전이 시스템은 원래 ''명명된'' 전이 시스템으로 소개되었다.^[1]

라벨 없는 상태 전이 시스템은 형식적으로는 튜플 (S, →)로 표시되며, S는 상태의 집합, →는 → ⊆ S × S인 S 상의 이항 관계 (즉, 전이)이다. p, q ∈ S에서 (p, q) ∈ →일 때, 이를 p → q로 표기한다. 이는 즉, 상태 p에서 상태 q로의 전이가 존재함을 의미한다.

라벨이 있는 상태 전이 시스템은 튜플 (S, Λ, →)로 표시되며, S는 상태의 집합, Λ는 라벨의 집합, → ⊆ S × Λ × S는 (라벨이 있는 전이의) 삼항 관계이다. p, q ∈ S에서 α ∈ Λ일 때, (p, α, q) ∈ →라면, 이를 다음과 같이 표기한다.

:$$

\begin{matrix}

& \alpha & \\

p & \rightarrow & q

\end{matrix}



이는 상태 p에서 상태 q로의 라벨 α가 붙은 전이가 존재함을 의미한다. 라벨은 대상 언어에 따라 다양한 사항을 표현한다. 일반적으로는 전이에 필요한 입력을 나타내는 경우, 전이의 트리거가 되는 조건을 나타내는 경우, 전이에 따라 실행되는 행동을 나타내는 경우가 있다.

2. 1. 레이블 없는 전이 시스템

2. 2. 레이블 전이 시스템

2. 2. 1. 특수한 경우

2. 2. 2. 코대수 표현