동시 변형률m

이 글은 검증을 위해 추가 인용문이 필요합니다. 신뢰할 수 있는 출처에 인용문을 추가하여 이 기사를 개선하는 데 도움을 주십시오. 조달되지 않은 자재는 제거될 수 있습니다.출처 : "Concurrent MetateM" – 뉴스 · 신문 · 서적 · 학자 · JSTOR (2022년 5월) (이 템플릿 메시지 삭제 방법 및 삭제 시기 확인)

Concurrent MetateM은 각 에이전트가 보여야 하는 동작의 시간적 논리 사양 세트를 사용하여 프로그래밍되는 다중 에이전트 언어입니다.이러한 사양은 에이전트의 동작을 생성하기 위해 직접 실행됩니다.그 결과 논리 사양을 하위 레벨의 구현으로 변환해야 하는 시스템과 마찬가지로 논리를 무효화할 위험이 없습니다.

MetateM 개념의 근원은 Gabbay의 분리 정리이다. 임의의 시간 논리식은 논리적으로 동등한 과거 → 미래 형태로 다시 쓰여질 수 있다.실행은 규칙을 이력과 지속적으로 일치시키고 선행 요소가 충족되면 해당 규칙을 실행하는 프로세스로 진행됩니다.모든 인스턴스화된 미래 시간의 결과는 프로그램 규칙으로 구성된 공식에 대한 모델을 반복적으로 생성하면서 이후에 충족되어야 하는 확약이 됩니다.

시간적 접속

Concurrent MetateM의 Temporal Connectives는 다음과 ^[1]같이2개의 카테고리로 나눌 수 있습니다.

• 엄밀한 과거 시간 연결: '●'(약후), '◎'(강후), '◆'(과거), '■'(과거), 'S'(이후), 'Z'(과거 약후)
• 현재 및 미래 시간 연결: '접속'(다음), '◇'(다음), '□'(항상), 'U'(끝까지) 및 'W'(다만 해당)

연결 {●,◆,■,■,disc,◇,□}은(는) 단항식이고 나머지는 이진식입니다.

엄격한 과거 시간 연결

약한 꼴찌

●이전에는 ρ이 참이었다면 지금은 만족합니다.처음에 ●를 해석하면 실제 이전 시간이 없어도 만족합니다.그래서 '약하다'는 꼴찌죠.

마지막 강자

◎이전에는 ρ이 참이었다면 지금은 만족합니다.처음에 ◎를 해석하면 실제 이전 시간이 없기 때문에 만족하지 않습니다.그래서 '강함'이 마지막이다.

이었다

◆이전의 어느 순간에라도 ρ가 참이었다면, 현재는 만족하고 있습니다.

지금까지

■이전의 모든 순간에 was가 참이었다면, 지금은 만족하고 있습니다.

부터

「S」는, 어느 시점에서나 「」가 참이고, 그 이후의 모든 시점에서 「S」가 참이면 만족합니다.

Zince, 또는 그 이후로는 약함

(전순간에 true가 되고 그 후순간에 true가 된다) 또는 과거에 true가 발생하지 않은 경우, 「Z」는 현재 만족합니다.

현재와 미래의 시간 연결

다음 분.

다음 순간에 is이 참이면 지금 is이 만족합니다.

가끔.

◇지금이나 미래의 어느 순간에나 ρ가 맞다면 지금 만족합니다.

항상

□지금과 미래의 모든 순간에 ρ이 사실이라면 지금 만족합니다.

까지

「U」는, 장래의 어느 시점에서나, 「U」가 항상 참이면 만족합니다.

~하지 않는 한

「W」는, 장래의 어느 시점에서도 true, 「true」는 전회의 어느 시점에서도 true) 또는 「true」가 장래에 발생하지 않는 경우에 만족하고 있습니다.

레퍼런스

외부 링크

• MetateM 인터프리터의 Java 구현은 여기에서 다운로드할 수 있습니다.