일반화 뷔치 오토마톤

오토마타 이론에서 일반화 뷔치 오토마톤은 뷔치 오토마톤의 변형이다.Büchi Automaton과의 차이점은 수용 조건, 즉 일련의 상태이다.자동이 허용 조건의 모든 집합 중 적어도 하나의 상태를 무한히 자주 방문하면 자동이 실행을 허용한다.일반화된 büchi automata는 Büchi automata와 동등한 표현력을 가지며, 여기서는 변혁을 제시합니다.

형식 검증에서 모델 체크 방법은 프로그램 속성을 지정하는 LTL 공식에서 오토마톤을 얻을 필요가 있다.LTL 공식을 일반화 Büchi 오토마톤으로 ^[1]^[2]^[3]^[4]변환하는 알고리즘이 있습니다.이 목적을 위해.일반화된 Büchi automaton의 개념은 이 번역에 특별히 도입되었습니다.

형식적 정의

공식적으로는 일반화된 Büchi 오토마톤은 다음과 같은 구성 요소로 구성된 태플 A = (Q, σ, q₀, f $,$ ${\cal {F}}$ , display, F { \ $displaystyle$ \ cal {\ $cal {F$

Q는 유한 집합입니다.Q의 요소를 A의 상태라고 합니다.
δ는 A의 알파벳이라고 불리는 유한 집합이다.
δ: Q × δ^Q → 2는 A의 전이 관계라고 하는 함수이다.
Q는₀ Q의 서브셋으로 초기 상태라고 불립니다.
${\cal {F}}$ F $(\$ 는 ${\cal {F}}$ 0개 이상의 수용 세트로 이루어진 수용 조건입니다. $각$ 수용 $F_{i}\in {\cal {F}}$ $†$ $F_{i}\in {\cal {F}}$ {\ $displaystyle$ F_ ${i}\in\$ cal ${F}}$ 는 $F_{i}\in {\cal {F}}$ Q의 서브셋입니다.

A는 무한히 자주 발생하는 상태의 집합이 각 수용 $F_{i}\in {\cal {F}}$ $F_{i}\in {\cal {F}}$ F { $displaystyle F_{i}\ in {cal {F$ 에서 적어도 상태를 포함하는 실행을 정확하게 받아들입니다.이 경우 수용 세트가 없을 수 있습니다.이 경우 무한 실행은 이 속성을 3차적으로 충족합니다.

보다 포괄적인 형식주의에 대해서는, 「자동화」도 참조해 주세요.

일반화된 Büchi Automaton이라는 라벨

라벨이 붙은 일반화된 Büchi 오토마톤은 입력이 전환이 아닌 상태와 라벨로 연관되는 또 다른 변형이다.그것은 Gerth 등에 ^[3]의해 소개되었다.

공식적으로, 라벨이 붙은 일반화 Büchi 오토마톤은 다음과 같은 구성 요소로 구성된 태플 A = (Q, δ, L, δ₀, $,$ F(\ $displaystyle {F$ 입니다.

Q는 유한 집합입니다.Q의 요소를 A의 상태라고 합니다.
δ는 A의 알파벳이라고 불리는 유한 집합이다.
L: Q → 2는^Σ A의 라벨링 함수라고 하는 함수이다.
δ: Q^Q → 2는 A의 전이 관계라고 불리는 함수이다.
Q는₀ Q의 서브셋으로 초기 상태라고 불립니다.
${\cal {F}}$ F $(\$ 는 ${\cal {F}}$ 0개 이상의 수용 세트로 이루어진 수용 조건입니다. $각$ 수용 $F_{i}\in {\cal {F}}$ $†$ $F_{i}\in {\cal {F}}$ {\ $displaystyle$ F_ ${i}\in\$ cal ${F}}$ 는 $F_{i}\in {\cal {F}}$ Q의 서브셋입니다.

w = aa₁₂ ...를 알파벳 σ 위에 있는 --word로 합니다.r₁,r₂, ...는 r q₀ Q의 경우₁ 단어 w에 대한 A의 실행이며 각 i 0 0, r_i+1 ∈ δ δ_i r L(r_i)에_i 대해 실행됩니다.A는 무한히 자주 발생하는 상태의 집합이 각 수용 $F_{i}\in {\cal {F}}$ $F_{i}\in {\cal {F}}$ F { $displaystyle F_{i}\ in {cal {F$ 에서 적어도 상태를 포함하는 실행을 정확하게 받아들입니다.이 경우 수용 세트가 없을 수 있습니다.이 경우 무한 실행은 이 속성을 3차적으로 충족합니다.

라벨이 부착되지 않은 버전을 얻기 위해 라벨은 노드에서 착신 전환으로 이동합니다.

레퍼런스

^ M.Y. 바르디와 P.울퍼, 무한연산에 관한 추론, 정보와 계산, 115(1994), 1-37.
^ Y. 케스텐, Z.Manna, H. McGuire, A. Pnueli, 완전 명제 시간 논리에 대한 결정 알고리즘, CAV'93, Elounda, 그리스, LNCS 697, Springer-Verlag, 97-109.
^ ^a ^b R. 거스, D.펠리드, M.Y. 바르디, P.Wolper, "Simple On-The-Fly" "Linear Temporary Logic 자동 검증", Proc.IFIP/WG6.1 Symp.프로토콜 사양, 테스트, 검증(PSTV95), 페이지 3-18, 폴란드 바르소, 채프먼 & 홀, 1995년 6월.
^ P. 개스틴과 D.Odoux, Fast LTL에서 Büchi Automata로의 번역, 제13차 컴퓨터 지원 검증 회의(CAV©01), LNCS 번호 2102, Springer-Verlag(2001), 페이지 53-65.

[VW94-1] M.Y. 바르디와 P.울퍼, 무한연산에 관한 추론, 정보와 계산, 115(1994), 1-37.

[KMMP93-2] Y. 케스텐, Z.Manna, H. McGuire, A. Pnueli, 완전 명제 시간 논리에 대한 결정 알고리즘, CAV'93, Elounda, 그리스, LNCS 697, Springer-Verlag, 97-109.

[GPVW93-3] R. 거스, D.펠리드, M.Y. 바르디, P.Wolper, "Simple On-The-Fly" "Linear Temporary Logic 자동 검증", Proc.IFIP/WG6.1 Symp.프로토콜 사양, 테스트, 검증(PSTV95), 페이지 3-18, 폴란드 바르소, 채프먼 & 홀, 1995년 6월.

[GOCAV01-4] P. 개스틴과 D.Odoux, Fast LTL에서 Büchi Automata로의 번역, 제13차 컴퓨터 지원 검증 회의(CAV©01), LNCS 번호 2102, Springer-Verlag(2001), 페이지 53-65.

[1]

[2]

[3]

[4]

Search

일반화 뷔치 오토마톤

네임스페이스

더

형식적 정의

일반화된 Büchi Automaton이라는 라벨

레퍼런스