입출력자동화

입출력 오토마타는 대부분의 유형의 비동기 동시 시스템을 설명하는 데 적용할 수 있는 공식적인 모델을 제공한다.그 자체로 I/O 오토메이션 모델에는 다양한 유형의 분산 시스템을 모델링할 수 있는 매우 기본적인 구조가 포함되어 있다.특정 유형의 비동기 시스템을 설명하려면 이 기본 모델에 추가 구조를 추가해야 한다.모델은 임의의 상대적 속도로 작동하면서 서로 상호작용하는 프로세스와 메시지 채널과 같은 시스템 구성요소에 대해 기술하고 추론할 수 있는 명시적인 방법을 제시한다.^[1]I/O 오토마타는 낸시 A에 의해 처음 소개되었다. 린치와 마크 R.1987년 "분산 알고리즘에 대한 계층적 정확성 증명"에서 다룬다.^[2]

"I/O 자동화는 다른 시스템 구성 요소와 상호 작용할 수 있는 분산 시스템 구성 요소를 모델링.그것은 전환이 명명된 동작과 연관되어 있는 단순한 형태의 상태 기계다."^[1]동작에는 입력, 출력, 내부 동작의 세 종류가 있다.자동화는 입력 및 출력 동작을 사용하여 환경과 통신하는 반면, 내부 동작은 자동자체에게만 보인다.자동화에 의해 선택되고 수행되는 내부 및 출력 동작과 달리, 단순히 환경에서 도착하는 입력 동작은 자동화의 통제 하에 있지 않다.^[1]

예

I/O 오토마타는 프로세스, 메시지 전달 시스템의 메시지 채널 또는 공유 메모리 시스템의 공유 데이터 구조와 같은 분산 시스템의 개별 구성요소를 모델링하는 데 사용될 수 있다.

프로세스 I/O 자동화

그림 1: 프로세스 I/O 자동화

그림 1은 비동기 메시지 전달 분산 시스템에서 프로세스에 대한 I/O 자동화의 예를 보여준다.이 설정에서 프로세스 P는_i 메시지 전달 시스템을 사용하여 다른 프로세스와 통신한다.출력 동작은 송신(m) 형태로,_i,j P를 처리하기 위해 내용_j m과 함께 메시지를 보내는 프로세스 P를_i 나타낸다.입력 동작은 수신(m) 형식이며,_k,i 프로세스 P로부터_k 프로세스 P에_i 의한 메시지 m의 수신을 나타낸다(프로세스 실행 알고리즘에 해당할 P의_i 내부 동작은 표시되지 않는다).

FIFO 메시지 채널

그림 2: FIFO 채널 I/O 오토매틱

메시지 채널은 또한 I/O 자동화에 의해 모델링될 수 있다.그림 2는 C라는_i,j 이름의 전형적인 단방향 FIFO 채널 자동화를 보여준다.송신(m)_i,j 형식의 입력 동작과 수신(m) 형식의 출력 동작이 있다._i,j각 메시지 m은 0 또는 1(m may {0,1})을 포함할 수 있다.자동화의 상태는 전송되었지만 아직 수신되지 않은 모든 메시지의 FIFO 대기열을 저장한다.

프로세스 오토마타와 통신 채널 오토마타가 모두 존재하는 전형적인 분산형 시스템에서, 그것들은 하나의 오토마톤의 출력 동작이 일치하고 다른 오토마타의 동일한 이름의 입력 동작으로 실행되는 방식으로 구성된다.예를 들어, P와_i P라는_j 두 개의 공정으로 구성된 시스템과 P를_j 처리하기 위한 프로세스 P의_i 통신 채널 C를_i,j 생각해 보자.이 설정에서 프로세스 P는_i 채널_i,j C가 송신(m)_i,j 입력 동작을 실행하는 경우에만 출력 동작 송신(m)을 실행한다._i,j

원자성 읽기/쓰기 레지스터

그림 3: 원자성 읽기/쓰기 레지스터 I/O 자동화

그림 3은 P와₁ P라는₂ 두 가지 프로세스를 가진 공유 메모리 시스템에서 원자 읽기/쓰기 레지스터 I/O 자동화를 보여준다.레지스터에 저장된 V 값은 정수형(V z Z)이다.자동화의 상태는 이 값을 저장한다.입력 작업은 기록부에 값 V를 쓰도록 요청하는 프로세스_i P(여기서 i { {1,2}, V ∈ Z)와 read를_i 나타내는 write_i(V)로 구성되며, 이는 레지스터에 현재 저장된 값을 읽도록 요청하는 프로세스 P에_i 해당한다.출력 동작 ack는_i 프로세스 P에_i 쓰기 요청이 성공적으로 완료되었음을 알리는 데 사용된다.출력 작용 V는_i 프로세스 P의_i 읽기 요청에 대한 응답으로 반환되는 V 값을 나타낸다.

자동화는 내부 동작 perform_Write(V), 레지스터에 값 V를 쓰는 perform_Write(V), 상태에 저장된 값 V를 읽는 데 사용되는 perform_Read도 포함한다.(이러한 내부 조치는 그림 3에 나와 있지 않다.)

형식 사양

I/O 자동화 A 또는 단순한 자동화는 다음 5가지 구성 요소로 구성된다.

시그(A)
주(A)
출발(A)
전보(A)
작업(A)^[1]^[3]

이 다섯 가지 구성요소는 아래에 설명되어 있다.

서명

I/O 자동 A 공식화의 첫 단계는 서명인 시그니처(A)의 정의다.시그너처 S는 다음과 같은 세 가지 불연속 조치 세트를 사용하여 I/O 자동화의 조치를 설명한다.

in(S): 입력 작업,
출력 작업 및
int(S): 내부 조치.

상기 입력, 출력, 내부 동작의 공식화를 바탕으로 다음과 같은 객체를 정의할 수 있다.

ext(S): ∪out(S)에 정의된 외부 조치
local(S): out(S) ∪ int(S)로 정의된 로컬 제어 조치
extsig(S): (S), out(S), ø로 정의된 외부 서명
행위(S)는 서명 S의 모든 행위의 집합으로 정의된다.^[1]^[3]

미국.

자동자동 A 상태 집합(A)은 유한할 필요가 없다.이는 카운터와 무한 길이 대기열과 같은 무한 데이터 구조를 가진 모델링 시스템을 가능하게 하기 때문에 유한한 오토마타라는 일반적인 개념을 상당히 일반화한 것이다.시작 상태 집합(초기 상태라고도 함)은 비어 있지 않은 상태의 하위 집합이다.일부 입력 정보가 시작 상태에 포함될 수 있도록 다중 시작 상태가 허용된다.^[1]^[3]

전환관계

자동 A의 상태-변환 관계는 transfer(A) ) state(A) × acts(sig(A) × state(A)로 표시된다.그것은 "모든 상태 s와 모든 입력 작용 π에 대해 전환(s, π, s)" trans trans(A)가 있는 속성을 만족한다."

I/O 자동 A의 단계라고도 하는 전환은 트랜스(A)의 요소(s, π, s')로 정의된다.입력 전환은 π이 입력 동작일 때 전환(s, π, s')을 말하며, 출력 전환은 π이 출력 동작일 때 전환(s, π, s')을 나타낸다.어떤 상태 s와 조치 π에 대해서, I/O 자동 A가 형태(s, π, s')의 어느 정도 전환이 있다면, s에서 π이 활성화된다고 한다.모든 입력 동작이 모든 상태에서 활성화되어야 하기 때문에 I/O 오토마타는 입력이 가능한 것으로 설명된다.대기 상태 s는 입력 작업만 활성화된 상태로 정의된다.^[1]^[3]

임무들

I/O 자동 A의 다섯 번째 구성 요소인 태스크(A)는 태스크 파티션으로, A의 로컬 제어 동작에 대한 동등성 관계로서 정의되며, 최대 카운트할 수 있는 많은 동등성 클래스를 가지고 있다.비공식적으로 태스크 분할 태스크(A)는 A 내에서 "태스크" 또는 "제어 스레드"에 대한 추상적인 설명을 나타낸다.

이 파티션은 자동 실행의 공정성 조건을 정의하는 데 사용된다.이 조건들은 자동화가 그것의 실행 동안에 각각의 임무를 공정하게 계속 돌릴 것을 요구한다.이것은 특히 다중 작업을 수행하는 시스템 구성요소를 모델링할 때 유용하다.예를 들어 주기적으로 상태 정보를 환경에 동시에 보고하면서 진행 중인 알고리즘에 참여하는 구성요소는 두 가지 작업을 하게 된다.칸막이는 또한 구성의 모든 오토마타가 구성된 시스템에서 계속 단계를 수행하도록 지정할 때 몇 개의 오토마타가 구성될 때(더 큰 시스템 자동화를 생산하기 위해) 유용하다.^[1]^[3]

예:채널 I/O 자동화에 대한 공식 정의

위에서 설명한 것처럼 C는 프로세스_i,j P에서_i 프로세스 P까지_j 단방향 FIFO 채널을 나타내는 I/O 자동화의 예다.m을 이진 메시지로 설정: m 0 {0,1}.자동측정기 C는_i,j 다음과 같이 공식적으로 정의될 수 있다.

서명:

sig(C_i,j)는 자동화에 두 가지 종류의 작업이 있음을 명시한다.

(C_i,j)의 입력 작업은 send(m) 형식이며 여기서 m ∈ {0,1}._i,j
(C_i,j)의 출력 동작은 (m) 형식이며 여기서 m _i,j∈{0,1}.

직관적으로 조치 송신(m)_i,j은 프로세스 P가_i 메시지 m을 송신할 때 채널에 진입했음을 나타내고 조치 수신(m)_i,j은 메시지 m이 프로세스 P로_j 전달될 때 채널을 떠났음을 나타낸다.^[1]

상태:

상태(C_i,j)는 m sequences {0,1} 요소의 모든 유한 시퀀스 집합이다.직관적으로 상태는 송신자, 프로세스 P에서_i 수신자, 프로세스 P로_j 현재 전송되고 있는 메시지의 순서를 나타낸다.

대기열의 초기 상태를 나타내는 start(C_i,j)는 빈 시퀀스만 포함한다.^[1]

전환

전환 관계는 각각의 특정 유형의 조치를 포함하는 모든 전환이 하나의 코드로 그룹화되는 전제 조건-효과 스타일로 모델링될 수 있다.이 코드에서, 어떤 조치가 일어나도록 허용하기 전에 충족되어야 하는 조건들은, 조치가 일어나기 전의 상태인 사전 상태 s에 대한 술어로 공식화된다.조치의 실행에 따른 상태에 대한 결과적 변화는 단순한 프로그램의 형태로 코딩된다.이 프로그램은 단일 전환으로서 불가침하게 실행된다.이 프로그램을 주 s에 적용하면, 새로운 주의 결과가 나온다.

C의_i,j 전환은 다음과 같이 설명된다.

발송용(m):_i,j

전제 조건:없음
효과: m이 상태에 저장된 시퀀스 끝에 추가됨(여기서 m sequence {1,0})

수신용(_i,jm):

전제 조건: m은 상태에 저장된 시퀀스의 첫 번째 요소(여기서 m ∈ {1,0})
효과: 상태에 저장된 시퀀스의 첫 번째 요소 제거

직관적으로, 송신 동작은 언제든지 실행될 수 있다; 그것은 체 채널의 메시지 대기열의 끝에 메시지 m을 추가하게 한다.수신 작업은 대기열의 첫 번째 요소를 제거하고 반환한다.^[1]

임무들

태스크(C_i,j)는 폼의 모든 액션을 하나의 태스크로 그룹화하는 태스크 파티션을 나타낸다.직관적으로 P프로세스에_j 메시지를 넘기는 것은 하나의 작업으로 간주된다.

{receive(m)_i,j : m ∈ {0,1}}.^[1]

실행 및 추적

실행

자동화된 실행에서, 자동화된 모델의 구성요소의 동작을 설명하는 문자열이 생성된다.^[3]"I/O Automaton A의 실행 파편은 다음 중 하나 입니다.

유한 순서, s₀, s₁₁, s, π₂, ..., π_r, s 또는_r
무한 시퀀스, s₀, s₁₁, s, s₂, s, ..., s_r, s_r,

(s, π_k_k+1, s_k+1)가 모든 k ≥ 0에 대해 A의 전환인 것과 같은 A의 상태와 작용의 교대.

유한한 순서는 상태와 함께 종료되어야 한다.실행은 시작 상태에서 시작하는 실행 조각으로 정의된다.A의 사형집계는 집행관(A)으로 대표된다.I/O 자동 A에서 도달 가능한 상태는 A의 유한한 실행의 최종 상태 입니다.

가정 α는 상태 s로_f 끝나는 A의 유한 실행 조각이다.더 나아가 α'는 s로_f 시작하는 A의 실행 파편, 즉 α의 마지막 상태라고 가정한다.이 경우 α와 α'를 결합하고, s의_f 중복 발생을 제거하여 생성된 시퀀스는 α의 마지막 상태로 나타낸다.α' 이 시퀀스는 I/O 자동 A의 실행 파편이기도 하다.^[1]

트레이스

I/O 자동 A의 추적은 A의 일부 실행 α에서 발생하는 외부 작용의 순서다.A의 모든 트레이스 세트는 트레이스(A)로 표현된다.^[1]

예:세 번의 실행

실행 a, b 및 c는 채널 I/O 자동화의 공식 정의(여기서 메시지 m ∈ {0, 1)에 설명된 자동 실행 C의_i,j 세 가지 실행이다.이 예에서 상태는 메시지 순서를 대괄호로 묶어서 표시하며 빈 순서는 λ으로 표시된다.

(a) [수신], [1],_i,j [1], [수신],_i,j [수신], [0],_i,j [수신]_i,j

(b) [b)], [send(1)],_i,j [1], [recept(1)],_i,j [recept(1), [send(0),_i,j [0]

(c) [c], [send(1)],_i,j [110], [send(1),_i,j [11], send(0),_i,j [110]...^[1]

오토마타 작업

구성작업

각각의 개별 시스템 구성요소를 설명하는 여러 개의 자동화를 구성하여 더 크고 복잡한 시스템을 나타내는 자동화를 산출할 수 있다.이 경우, 각 구성 오토마타에서 동일한 이름을 가진 조치를 함께 식별한다.따라서 구성품 자동화가 동작 includes을 포함하는 단계를 밟으면 서명에 π이 포함된 다른 모든 구성품 자동자도 그 동작을 수행한다.다음은 허용되는 자동마타 A와 A'의 구성 조건을 개략적으로 설명한다.

A의 내부행동은 A'의 행위로부터 분리되어야 한다.이는 A'의 동작과 이름이 같은 A의 내부 동작이 수행될 때 A'의 스텝 수행을 방지한다.
A와 A'의 출력 작용은 분리되어야 한다.이 조건은 오직 하나의 구성 요소만이 출력 작용의 성능을 제어한다는 것을 보장한다.

만약 구성이 셀 수 없을 정도로 무한한 오토마타 모음으로부터 구성된다면, 추가적인 제약이 있다: 각각의 행동은 오직 많은 구성 오토마타의 작용일 필요가 있다.오토마타의 무한한 구성은 많은 논리적인 요소들로 구성될 수 있는 논리 시스템의 모델링을 가능하게 한다.논리 시스템은 종종 더 적은 구성요소를 포함하는 물리적 시스템에서 구현된다.^[1]

예: 구성

그림 4: 구성

그림 4는 P와_i P_j, FIFO 메시지 채널 C라는_i,j 두 공정의 구성을 나타내며, 한 자동자의 출력 작용과 다른 자동자의 동일한 이름의 입력 작용을 일치시킨다.따라서 공정 P에_i 의해 수행되는 송신(m)_i,j 출력은 채널 C에_i,j 의해 수행되는 송신(m)_i,j 입력을 매칭하여 수행한다.

프로세스 P는_i 채널 C를_i,j 통해 프로세스 P로_j m ∈{1,0} 메시지를 전송한다.프로세스 P는_j 수신된 메시지 m의 비트를 그림에는 표시되지 않은 내부 동작 역순으로 P에서_i 반전시키고 시스템의 다른 부분에 메시지를 전달한다.

숨기기 작업

"내부 작용으로 재분류"를 통해 I/O 자동화의 출력 동작을 숨길 수 있다.이는 시스템의 다른 부분과의 통신에서 이들을 배제하는 효과가 있다.형식적으로는 서명을 위한 은닉작전을 다음과 같이 기술한다.

S는 서명이 되고 φ은 out 아웃(S)으로 하자.hide_Φ(S)는 새로운 서명 S'로, 여기서

인(S)'=인(S)에
아웃(S')=아웃(S) - φ
int(S') =int(S) ∪ φ

따라서 "A가 자동자이고 out ⊆ out(A)이라면, hide_Φ(A)는 sig(A) = hide_Φ(A)를 sig(A) = hide(A)로 대체하여 A로부터 얻은 automaton A"이다.^[1]

공정성

태스크 파티션이 I/O 자동의 로컬 제어 동작에 대한 동등성 관계로서 정의되며, 최대 카운트할 수 있는 많은 동등성 클래스를 포함한다는 점을 기억하십시오.이 설정에서 공정성은 각 과제에 지속적으로 조치를 수행할 수 있는 기회를 제공하는 것으로 정의할 수 있다.

I/O 자동 A에서 C가 작업 클래스(A)를 나타내도록 하십시오.형식적으로 A의 실행 파편 α는 아래 기준이 모든 등급 C에 대해 유지된다면 공정하게 간주된다.

"α가 유한하면 α의 최종 상태에서는 C가 활성화되지 않는다."
"α가 무한하다면, α는 C로부터 무한히 많은 사건이나 C가 활성화되지 않은 상태의 발생을 무한히 많이 포함한다."

이벤트는 "실행 또는 추적과 같은 일련의 동작 발생"으로 정의된다."무한하게 자주"라는 공정성의 정의에 기초하여 각 과제(또는 동등성 등급 C)는 행동을 수행할 기회를 얻는다.작업(또는 동등성 등급) C가 작업을 수행할 기회를 얻는 경우, C의 작업이 현재 상태에서 활성화되어 수행될 수 있는 경우 또는 C의 어떤 작업도 현재 상태에서 활성화되지 않아 수행할 수 없는 경우 등 두 가지 경우가 가능하다.따라서 최종 상태 S를_f 가진 유한한 공정집행은 자동화가 라운드 로빈 방식으로 모든 직무에 지속적으로 회전을 주지만, S에서_f 활성화되는 것이 없기 때문에 어떤 조치도 실행되지 않는 실행으로 정의할 수 있다.

I/O 자동 A의 공정한 실행 세트는 fairexecs(A)로 표현된다.β를 A의 공정한 실행의 흔적이 되게 하라.그렇다면 β는 A의 공정한 흔적이다.A의 정해진 공정한 흔적은 페어트레이스(A)로 표현된다.

실행 예에서, 실행 (a)은 공정한데, 최종 상태에서는 수신 조치가 활성화되지 않기 때문이다.실행 (b)은 유한하지만, 수신 동작은 최종 상태에서 활성화된다.따라서 집행(b)은 공평하지 않다.실행(c)은 무한하며, 수신 이벤트를 포함하지 않으며, 첫 번째 단계 이후의 모든 지점에서 수신 작업이 활성화된다.따라서 공정한 집행이 아니다.^[1]^[3]공정성의 정의는 "구성요소의 공정한 집행은 구성 요소의 공정한 집행의 구성" 즉, 공정(Fair)(A)= fair_i_i 공정_i(A_i)^[2]이다.

특성 및 증명 방법

I/O 오토마타는 비동기 시스템에 대한 정확한 설명을 제공한다.그들은 또한 "시스템이 할 수 있는 일"에 대한 "청구권"을 공식화하고 증명하는 데 이용된다.이 절에서는 여러 가지 중요한 유형의 속성에 대해 설명한다.이러한 특성 및 증빙 방법은 분산 알고리즘에 설명되어 있다.^[1]

입력 활성화 속성

입력을 활성화하는 속성은 자동화가 입력 동작의 발생을 차단할 수 없다고 명시한다.이 속성을 갖는 두 가지 중요한 이점은 다음과 같다.

임의의 입력에 대처하도록 설계된 모델로서, 예기치 않은 입력에 대한 처리 실패로 인한 시스템 오류의 주요 원인이 제거된다.
입력 활성화 속성은 "외부 동작의 순서에 기초하여 자동화를 위한 간단한 외부 동작 개념"을 사용한다.모델에서 특정 이론에 대한 증명은 이 특성을 가정하지 않고 실패할 수 있다.

추적 속성

I/O 자동화의 내부 동작은 사용자에게 보이지 않으므로, I/O 자동화는 블랙박스로 보이며 사용자는 "자동화 실행(또는 공정한 실행)의 과정"만 볼 수 있다.I/O 오토마타의 특정 특성 및 그 증명은 일반적으로 "그들의 흔적 또는 공정한 흔적"으로 공식화된다.

P를 추적 속성으로 한다. P는 다음과 같은 구성 요소를 가지고 있다.

내부 동작이 없는 서명을 나타내는 시그널(P)
추적(P), 이는 일련의 "행동 중 행동 순서(sig(P)"에 해당한다.이 세트는 무한할 수 있다.

추적 속성은 외부 서명과 그 인터페이스에서 보는 시퀀스의 집합(또는 속성)을 설명한다.때로는 행위(sig(P))가 속기법 행위(P)로 표현되기도 한다.I/O 자동 A가 추적 속성 P를 만족한다고 언급될 때, (적어도) 두 가지 다른 의미가 의도될 수 있다.

"extsig(A) = sig(P) 및 trace(A) ⊆ trace(P)"
"extsig(A) = sig(P) 및 pairtraces(A) ⊆ trace(P)"

직관적으로, 그것은 A가 외부 행동을 생성할 때 속성 P에 의해 허용된다는 것을 의미한다.그러나 A가 실제로 P의 모든 흔적을 나타낼 필요는 없다.A는 입력이 가능하기 때문에 가능한 모든 입력 동작의 순서에 대해 페어트레이스(A) (따라서 트레이스(A))는 A의 응답을 포함한다.만약 페어트랙스(A) ⊆ 트레이스(P)가 유지된다면, 속성 P는 생성된 모든 시퀀스를 포함해야 한다.

안전 특성

직관적으로, 안전 속성은 어떤 "나쁜" 일도 일어나지 않는다는 사실을 나타낸다.좀 더 형식적으로 P를 추적 속성이 되게 하라.P는 추적(P)을 위해 다음 기준이 유지되는 경우 추적 안전 속성 또는 안전 속성이다.

트레이스(P)가 비어 있지 않음: 어떤 사건이 발생하기 전에는 나쁜 일이 일어날 수 없으므로, 비어 있지 않은 것은 트레이스(P)에 대한 합리적인 조건이다.
트레이스(P)는 "prefix-closed"이다. 렛트 β ∈ trace(P) 및 β'는 β의 유한 접두사를 나타낸다. 이 경우 β' ' trace(P)는 β의 유한한 접두사를 나타낸다.자세히 설명하자면, 나쁜 일이 일어나지 않는 흔적이 있다고 가정해 보자.그러므로 그 추적의 어떤 접두사에서도 나쁜 일은 일어나지 않는다.따라서 접두사 폐쇄는 추적(P)에 대한 합리적인 조건이다.
트레이스(P)는 "limit-close"이다: 렛 β₁, β₂, . . 트레이스(P)에서 유한 시퀀스의 무한 시퀀스를 나타낸다.또한 각 i에 대해 β가_i β의_i+1 접두사라고 가정한다.이 경우 "연속 연장 순서 하의 β 한계"인 고유 시퀀스 β도_i 트레이스(P)에 존재한다.그러므로 만일 추적에서 나쁜 일이 일어난다면, 그것은 추적에서 어떤 특정한 사건의 결과일 것이다.따라서 이 경우에 제한적인 폐쇄를 갖는 것은 트레이스(P)에 대한 합리적인 조건이다.

Livity 속성

비공식적으로, liven 속성은 어떤 "좋은" 것이 결국 일어나는 것으로 해석될 수 있다.따라서 일정 시점에 무슨 일이 일어났든 간에 미래 어느 시점에 좋은 일이 일어날 수 있다.좀 더 형식적으로 P를 추적 속성이 되게 하라.P는 추적성 속성, 즉 "행위에 대한 모든 유한 시퀀스(P)가 추적(P)에 어느 정도 확장된 경우"를 말한다.

추가 읽기

시간 지정 I/O 자동:Merritt, Michael; Modugno, Francesmary; Tuttle, Mark R. (August 1991). "Time constrained automata (Extended Abstract)". Proceedings of the 2nd International Conference on Concurrency Theory. CONCUR '91. Vol. 527. pp. 408–423.
확률론적 I/O 자동 분석:

참고 항목

참조

^ ^a ^b ^c ^d ^e ^f ^g ^h ⁱ ^j ^k ^l ^m ⁿ ^o ^p ^q ^r ^s Lynch, Nancy (1996). Distributed Algorithms (1st ed.). San Francisco, CA: Morgan Kaufmann Publishers. ISBN 978-1-55860-348-6.
^ ^a ^b Lynch, Nancy A.; Tuttle, Mark R. (August 1987). "Hierarchical correctness proofs for distributed algorithms". Proceedings of the sixth annual ACM Symposium on Principles of distributed computing. PODC '87. pp. 137–151.
^ ^a ^b ^c ^d ^e ^f ^g Lynch, Nancy A.; Tuttle, Mark R. (September 1989). "An introduction to input/output automata" (PDF). CWI-Quarterly. 2 (3): 219–246.

[lynch1997-1] ^ ^a ^b ^c ^d ^e ^f ^g ^h ⁱ ^j ^k ^l ^m ⁿ ^o ^p ^q ^r ^s Lynch, Nancy (1996). Distributed Algorithms (1st ed.). San Francisco, CA: Morgan Kaufmann Publishers. ISBN 978-1-55860-348-6.

[lynch-tuttle87-2] Lynch, Nancy A.; Tuttle, Mark R. (August 1987). "Hierarchical correctness proofs for distributed algorithms". Proceedings of the sixth annual ACM Symposium on Principles of distributed computing. PODC '87. pp. 137–151.

[lynch-tuttle-3] ^ ^a ^b ^c ^d ^e ^f ^g Lynch, Nancy A.; Tuttle, Mark R. (September 1989). "An introduction to input/output automata" (PDF). CWI-Quarterly. 2 (3): 219–246.

[1]

[2]

[3]

Search