배우모델론

이 글은 검증을 위해 인용구가 추가로 필요하다. 신뢰할 수 있는 출처에 인용문을 추가하여 이 기사를 개선할 수 있도록 도와주십시오. 공급되지 않은 재료는 도전하여 제거할 수 있다. 출처 찾기: "배우 모델 이론" – 뉴스 · 신문 · 책 · 학자 · JSTOR(2011년 8월) (이 템플릿 메시지를 제거하는 방법과 시기 학습)

이론적 컴퓨터 과학에서, 배우 모델 이론은 배우 모델의 이론적 이슈와 관련이 있다.

액터들은 동시 디지털 계산의 액터 모델의 기초를 이루는 원시 요소들이다. 수신하는 메시지에 대응하여, 행위자는 로컬 결정을 내리고, 더 많은 행위자를 만들고, 더 많은 메시지를 보내고, 수신한 다음 메시지에 대한 응답 방법을 지정할 수 있다. 행위자 모델 이론은 행위자 계산의 사건 및 구조에 대한 이론, 그들의 증명 이론 및 변위적 모델을 통합한다.

이벤트 및 이벤트 순서

행위자의 정의에서, 지역적 결정, 행위자 만들기, 메시지 보내기, 메시지 받기, 수신한 다음 메시지에 대한 대응 방법 지정 등 수많은 사건이 일어나는 것을 알 수 있다.

그러나, 이 기사는 배우에게 보낸 메시지의 도착에 해당하는 사건에만 초점을 맞추고 있다.

본 기사는 Hewitt [2006년]에 발표된 결과를 보고한다.

계산법칙: 기껏해야 많은 사건들이 있다.

활성화 순서

활성화 순서(-≈→)는 한 이벤트를 다른 이벤트로 활성화하는 모델링을 하는 기본 순서다(어떤 이벤트에서 활성화되는 이벤트로 전달되는 메시지에 에너지 흐름이 있어야 한다).

• 에너지의 전송으로 인해 활성화 순서는 상대론적으로 불변한다. 즉, 모든 이벤트에 대해 e1.e2만일 e1 -≈→ e2, 그리고 그 시간 e1 의 시간보다 앞서다 e2 모든 관찰자의 상대론적 기준에서.
• 활성화 순서에 대한 엄격한 인과관계의 법칙: 어떤 사건도 일어나지 않는다. e -≈→ e.
• 활성화 순서에서 유한 사전 처리 법칙: 모든 이벤트에 대해 e1 세트 {e e -≈→ e1} 유한하다.

도착순서

배우의 도착 순서 x ( -x→ ) 메시지가 도착하는 이벤트의 (총) 순서를 모델링 x. 도착 순서는 메시지 처리에서 중재에 의해 결정된다(종종 조정자라 불리는 디지털 회로를 사용한다). 배우의 도착행사는 세계 일선에 있다. 도착 순서는 행위자 모델이 본질적으로 불변성을 가지고 있음을 의미한다(동시 계산의 불변성 참조).

• 왜냐하면 배우의 도착 순서에 따른 모든 사건들이 x …의 세계적 선에서 일어나다 x배우의 도착 순서는 상대론적으로 불변적이다. 즉, 모든 배우에게 x 그리고 사건들 e1.e2만일 e1 -x→ e2, 그리고 그 시간 e1 의 시간보다 앞서다 e2 모든 관찰자의 상대론적 기준에서.
• 도착 순서의 유한 사전 처리 법칙: 모든 이벤트에 대해 e1 앤 액터스 x 세트 {e e -x→ e1} 유한하다.

복합발주

결합된 주문(에 의해 표시됨) →)는 모든 행위자의 활성화 순서와 도착 순서의 전이적 폐쇄로 정의된다.

• 조합 순서는 상대적 비변동적 순서의 타동적 종결이기 때문에 상대적 비변동적 순서가 된다. 즉, 모든 이벤트에 대해 e1.e2만일 e1→e2...의 시간. e1 의 시간보다 앞서다 e2 모든 관찰자의 상대론적 기준에서.
• 복합 주문에 대한 엄격한 인과관계의 법칙: 어떤 사건도 일어나지 않는다. e→e.

조합된 순서는 분명히 정의상 전이적이다.

[베이커와 휴이트 197?]에서는 위의 법률이 다음과 같은 법을 수반할 수 있다고 추측하였다.

결합 순서에서의 사건 사이의 유한 사슬의 법칙: 결합 순서 → 두 이벤트 사이에는 무한 체인(즉, 선형 순서 집합)이 없다.

복합순서에서의 사건간 유한체인의 독립성

그러나, [Clinger 1981]은 놀랍게도 결합 순서에서의 사건들 사이의 유한 사슬의 법칙이 이전 법, 즉, 이전 법률과 무관하다는 것을 증명했다.

정리. 복합 순서에서 사건 사이의 유한 사슬의 법칙은 앞서 언급한 법률에서 따르지 않는다.

증명. 이전에 언급된 법률은 충족하지만 결합 순서상 사건 사이의 유한 사슬에 관한 법칙을 위반하는 행위자 연산이 있다는 것을 보여주기에 충분하다.

배우 Initial이 전송될 때 시작되는 계산을 고려하십시오. Start 다음 작업을 수행하도록 하는 메시지

1. 메시지를 보낼 새 배우 그리터₁ 만들기 SayHelloTo 그리터₁ 주소로
2. 메시지 초기 전송 Again 그리터₁ 주소로

그 후에 이니셜의 행동은 다음과 같다. Again 주소 그리터_i(이벤트라고 부를 것)와 함께 하는 메시지 Againi):

1. 메시지를 보낼 새 배우 그리터_i+1 만들기 SayHelloTo 주소를 그리터_i(Greeter로
2. 메시지 초기 전송 Again 그리터_i+1 주소로

분명히 초기 전송 자체의 계산 Again 메시지는 결코 끝나지 않는다.

각 배우 그리터의_i 행동은 다음과 같다.

• 메시지를 수신할 때 SayHelloTo 그리터라는_i-1 주소와 함께. SayHelloToi() 를 전송한다. Hello 그리터에게_i-1 보내는 메시지
• A를 받을 때 Hello 메시지(이벤트라고 부를 것) Helloi)) 아무것도 하지 않는다.

이제 그럴 가능성이 있다. Helloi -Greeteri→ SayHelloToi 이러저러한 때 마다 Helloi→SayHelloToi.

또한 Againi -≈→ Againi+1 이러저러한 때 마다 Againi → Againi+1.

게다가, 조합 질서에 대한 엄격한 인과관계의 법칙 이전에 언급된 모든 법률이 충족된다.

그러나, 다음 사이의 결합 순서에는 무한한 수의 이벤트가 있을 수 있다. Again1 그리고 SayHelloTo1 아래와 같이

Again1→...→Againi→...${\displaystyle \infty }$...→Helloi→SayHelloToi→...→Hello1→SayHelloTo1

그러나 우리는 물리학을 통해 무한한 에너지가 유한한 궤적을 따라 팽창될 수 없다는 것을 알고 있다. 따라서, 행위자 모델은 물리학을 기반으로 하기 때문에, 결합 순서에서의 사건들 사이의 유한 사슬의 법칙은 행위자 모델의 공리로 받아들여졌다.

디스코티스의 법칙

결합 순서에서의 사건 사이의 유한 사슬의 법칙은 다음 법률과 밀접하게 관련되어 있다.

Discresentity의 법칙 모든 이벤트에 대해 e1 그리고 e2세트 {e e1→e→e2} 유한하다.

실제로 이전 두 법률은 다음과 동등한 것으로 나타났다.

정리 [클링거 1981] Discretity의 법칙은 (선택의 공리를 사용하지 않고) 결합 순서상 사건들 사이의 유한 사슬의 법칙에 해당한다.

불명확성의 법칙은 제노 기계를 배제하고 페트리 네트에서의 결과와 관련이 있다[Best et al. 1984, 1987].

디스코티스의 법칙은 무한의 비결정주의의 속성을 내포하고 있다. 복합 주문은 [Clinger 1981]가 액터들의 변위적 모델 구축에 사용한다(변위적 의미론적 의미론 참조).

변절 의미론

Clinger [1981]는 파워 도메인을 사용하는 행위자를 위한 변위적 모델을 구축하기 위해 위에서 설명한 행위자 이벤트 모델을 사용했다. 그 후 Hewitt [2006]는 기술적으로 이해하기 쉬운 기술적으로 단순한 변위 모델을 구성하기 위해 도착 시간으로 도표를 증강했다.

참고 항목

• 배우 모델 초기 역사
• 배우 모델 및 프로세스 캘컬리
• 행위자 모델 구현

참조

• 칼 휴이트 외 1974년 1월, 프로그래밍 언어의 원리에 관한 ACM 심포지엄의 배우 인덕션 및 메타 평가 컨퍼런스 기록.
• 아이린 그리프. MIT EECS 박사논문 전달 병렬 프로세스 의미론. 1975년 8월.
• 에드거 디크스트라 프렌티스 홀 프로그래밍의 규율 1976.
• 프로그래밍 개념에 대한 공식적인 설명에 관한 IFIP 실무회의의 Carl Hewitt와 Henry Baker 배우 및 연속 기능 진행. 1977년 8월 1일~5일.
• Henry Baker와 Carl Hewitt는 인공지능 프로그래밍 언어에 관한 심포지엄의 진행 과정의 증분적 쓰레기 모음입니다. SIGPlan 통지서 1977년 8월 12일.
• Carl Hewitt와 Henry Baker Laws for Communication Parallel Process IFIP-77, 1977년 8월.
• 메시지 전달 의미론 MIT EECS 박사논문에 기초한 병렬 프로그램의 아키 요네자와 사양 및 검증 기법 1977년 12월.
• 피터 비숍 매우 큰 주소 공간 모듈식으로 확장 가능한 컴퓨터 시스템 MIT EECS 박사 논문 1977년 6월.
• 칼 휴이트 제어 구조를 인공지능의 전달 메시지 저널 패턴으로 보는 것. 1977년 6월.
• 헨리 베이커. 실시간 계산을 위한 배우 시스템 MIT EECS 박사 논문. 1978년 1월.
• 칼 휴이트와 러스 앳킨슨. 소프트웨어 엔지니어링에 관한 시리얼라이저 IEEE 저널의 사양 및 증명 기법. 1979년 1월.
• 칼 휴이트, 베페 아타르디, 헨리 리버먼. AL, 분산 시스템 헌츠빌 제1차 국제 회의 메시지 전달 절차 대표단 1979년 10월.
• 러스 앳킨슨 일련 번호 MIT 박사 논문 자동 검증. 1980년 6월.
• 빌 콘펠트와 칼 휴이트. 과학 커뮤니티 시스템, 인간 및 사이버네틱스에 대한 IEEE 거래 은유. 1981년 1월.
• 게리 바버 MIT EECS 박사학위 논문 변경에 관한 고찰 1981년 8월.
• 빌 콘펠트 MIT EECS 박사 논문 문제 해결의 병행성. 1981년 8월.
• 윌 클린저 배우 의미론 MIT 수학 박사 논문의 기초. 1981년 6월.
• 아이케 베스트. 동시 행동: 컴퓨터 과학 Vol.197 1984의 시퀀스, 프로세스 및 악시오즈 강의 노트
• 굴 아그하. 배우: 분산 시스템 박사 논문의 동시 연산 모델. 1986.
• 아이케 베스트와 R.디빌러. Petri Net 이론 이론 이론 컴퓨터 과학 Vol.55/1. 1987의 순차 및 동시 거동
• 굴 아그하, 이안 메이슨, 스콧 스미스, 캐롤린 탤콧. 1993년 1월 배우 연산 저널 기능 프로그래밍.
• 마츠오카 사토시, 요네자와 아키노리. 동시 객체 지향 프로그래밍에서 객체 지향 동시 프로그래밍 언어의 상속 이상 분석. 1993.
• 자야데프 미즈라 동시 프로그래밍의 논리: 컴퓨터 소프트웨어 엔지니어링의 안전 저널. 1995.
• 루카 데 알파로, 조하르 마나, 헨리 시프마, 토마스 우리베. 반응형 시스템 TACAS 1997의 시각적 검증.
• 테리, 프라산나, 캐롤린 탈콧, 굴 아그하. 사양 도표 실행 및 추론 기법, 2004년 대수 방법론 및 소프트웨어 기술에 관한 국제 회의(AMAST),
• 주세페 밀리시아와 블라디미로 사소네 상속 이상 징후: 2004년 3월 14~17일, 키프로스 니코시아의 응용 컴퓨팅에 관한 2004 ACM 심포지엄의 10년 후 과정
• 페트루스 팟지터 제노머신과 하이퍼컴퓨팅 2005
• 칼 휴이트 헌신이 무엇인가?Physical, Organization and Social CONES@AAMAS. 2006.