전환 시스템

이론 컴퓨터 과학에서, 전이 시스템은 계산 연구에 사용되는 개념이다.이것은 이산 시스템의 잠재적인 동작을 설명하는 데 사용됩니다.상태 및 상태 간 전환으로 구성되며, 한 세트에서 선택한 레이블로 레이블이 지정될 수 있습니다. 두 개 이상의 전환에 동일한 레이블이 표시될 수 있습니다.라벨 세트가 싱글톤인 경우 시스템은 기본적으로 라벨이 없으며 라벨을 생략하는 간단한 정의가 가능합니다.

변환 시스템은 수학적으로 추상 개서 시스템(이 문서에서 자세히 설명) 및 지시 그래프와 일치합니다.유한 상태 오토마타와는 몇 가지 점에서 다릅니다.

• 상태 집합이 반드시 유한하거나 셀 수 있는 것은 아닙니다.
• 전환 집합이 반드시 유한하거나 셀 수 있는 것은 아닙니다.
• "시작" 상태 또는 "최종" 상태는 제공되지 않습니다.

전환 시스템은 방향 그래프로 나타낼 수 있습니다.

형식적 정의

공식적으로 전환 시스템은 쌍$({\displaystyle S}$, $\to {\displaystyle }$ $)(\displaystyle$ ($S,\right$ 화살표$)$입니다. $여기$서 S$(\displaystyle$$$S$)$는 상태 집합이고 $→(\displaystyle \right$ 화살표$)$는 상태 전환의 관계입니다(즉${\displaystyle ,}$ S ×$$\$displaystyle$ $\times$ S$\$$tes$).$상태{\displaystyle }$ p$(\displaystyle$ p$)$에서 $상태{\displaystyle }$q(\$displaystyle$q)$$$$ ($p,q$)\rightarrow$})$로의 이행은 p ${\displaystyle \to }$$$q$(\displaystyle$ p$\rightarrow$q$)$로 $표시$됩니다.

레이블이 지정된 전환 시스템은 튜플$({\displaystyle S,}$ , $\to {\displaystyle }$ $)($$S$,\Lambda$,\rightarrow$)입니다$$. $여기$서 S$(\displaystyle$ S$)$는 상태 $집합$이고,$$→(\$displaystyle$$\Lambda }$는 레이블 집합이며, $→\$displaystyle $\rightarrow }$는 전환 관계입니다.$s \Lambda \times$ S$$}${\displaystyle }$（${\displaystyle p}$ ,${\displaystyle \alpha }$ ,${\displaystyle }$q ） $→\displaystyle$( $p$, \$alpha ,$ q )\$in \rightarrow }$는 다음과 같이 기술됩니다.

${\displaystyle pcoverset\alpha }{\rightarrow }}q,$

$(\displaystyle\alpha$가 붙은 $상태{\displaystyle }$ p$(\displaystyle$ p$)$에서 $상태{\displaystyle }$q(\$displaystyle$q)로의$$ 전환을 나타냅니다.라벨은 관심 언어에 따라 다른 것을 나타낼 수 있습니다.라벨의 일반적인 용도에는 예상되는 입력, 천이를 트리거하기 위해 참이어야 하는 조건 또는 천이 중에 수행되는 작업이 포함됩니다.라벨이 붙은 이행 시스템은 원래 명명된 이행 ^[1]시스템으로 도입되었다.

특수한 경우

• $특정{\displaystyle }$p {\$displaystyle$ $p$$}$ 및$α$ {\displaystyle \alpha$}$에 대해 $→$ {\$displaystyle \rightarrow$에 단일 튜플$p$$,$${\displaystyle }$q$)$만 존재하는 경우$$α {\$displaystyle \alpha }$이(p$,\displaystyle$ p$}$의 $경우{\displaystyle }$) 결정론이라고 합니다.
• $특정{\displaystyle }$p {\$displaystyle$ p$$$}$ $α$ {\$displaystyle$ \alpha$\}$에 대해 $→$ {\$displaystyle \rightarrow$에 하나 이상의 태플$p,$이 있는 경우$$α {\$displaystyle \alpha }$이 실행 가능함을 $나타냅니다{\displaystyle }$($p{\displaystyle }${\$displaystyle$p}).$$

범주 이론 공식화

공식적인 정의는 범주 이론의 관점에서 바꿔 말할 수 있다.라벨이 부착된 모든 상태 전이 시스템$({\displaystyle }$ ${\displaystyle \mathrm{S},}$ ,$$、 ${\displaystyle {\to }_{}}$ $)(S,\Lambda,\right$ 화살표$)$은$$S$(\displaystyle$ S$)$에서 $S{\displaystyle \mathrm{}}$$(\displaystyle$ S$)$의 거듭제곱에 이르는 $함수{\displaystyle {}_{}}$ $→(\$ _${\rightarrow$})이다$.$$style {Mathcal {P}}(Lambda \times$ S$),$ 정의

${\displaystyle p\mapsto }${ (${\displaystyle \alpha }$ ,${\displaystyle }$q )${\displaystyle }$∈ ${\displaystyle \mathrm{\lambda }\lambda S}$ :$$ ${\displaystyle \to \stackrel{}{}}$ ${\displaystyle \alpha }$ q$}$ 。{\$style$p\mapsto $\{(\alpha$ ,$q)\in \Lambda$ \$times S:p{\overset$ {\alpha }{\$rightarrow }}$q\} } } }.

따라서 라벨이 부착된 상태 전이 시스템은 $펑터{\displaystyle }$ P${\displaystyle (\mathrm{\delta }}$ ×${\displaystyle \to }$)의 F-석탄 대수가 됩니다(\$displaystyle$ P$(\Lambda \times \rightarrow$

라벨 부착 및 라벨 부착되지 않은 전이 시스템 간의 관계

이 개념들 사이에는 많은 관계가 있다.라벨 세트가 하나의 요소로만 구성되어 있는 라벨 부착 전이 시스템이 라벨 부착되지 않은 전이 시스템과 동등하다는 것을 관찰하는 것과 같이 일부는 단순하다.그러나 이 모든 관계가 똑같이 사소한 것은 아니다.

추상 개서 시스템과의 비교

수학적 객체로서 라벨이 없는 전이 시스템은 (인덱스화되지 않은) 추상적인 개서 시스템과 동일하다.만약 우리가 개서 관계를 색인화된 관계 집합으로 간주한다면, 라벨이 붙은 전이 시스템은 인덱스가 라벨인 추상적인 개서 시스템과 동등하다.그러나 연구의 초점과 용어는 다르다.전환 시스템에서는 라벨을 동작으로 해석하는 데 관심이 있는 반면 추상적인 개서 시스템에서는 오브젝트가 어떻게 다른 ^[2]것으로 변환(재작성)될 수 있는지에 초점이 맞춰집니다.

내선번호

모델 확인에서 전환 시스템은 상태에 대한 추가 라벨링 기능을 포함하도록 정의되어 크립케 ^[3]구조의 개념을 포함시키기도 한다.

동작 언어는 F의 집합, 값 V의 집합 및 F × ^[4]S를 V에 매핑하는 함수를 추가하는 전이 시스템의 확장입니다.

「 」를 참조해 주세요.

• 전이 모노이드
• 변환모노이드
• 반군 작용
• 시뮬레이션 사전 주문
• 쌍시뮬레이션
• 운용 의미론
• 크립케 구조
• 유한 상태 기계
• 모달 μ-calculus

레퍼런스