Concurrent MetateMは、各エージェントが示すべき動作を記述した（拡張された）時相論理仕様を用いてプログラムされるマルチエージェント言語です。これらの仕様は直接実行され、エージェントの動作を生成します。そのため、論理仕様をまず低レベルの実装に変換しなければならないシステムのように、ロジックが無効化されるリスクはありません。
MetateM コンセプトの根底にあるのは、 Gabbay の分離定理です。任意の時相論理式は、論理的に等価な 過去→未来形式に書き換えることができます。実行は、ルールを履歴と継続的に照合し、前提が満たされたときにそれらのルールを発火させるプロセスによって進行します。インスタンス化された未来時間の後件部は、その後必ず満たされなければならないコミットメントとなり、プログラムルールで構成される式のモデルを反復的に生成します。
時間接続詞
並行メタテムの時間的接続詞は、次の2つのカテゴリーに分けられます。[1]
- 厳密な過去接続詞: '●' (弱過去)、 '◎' (強過去)、 '◆' (was)、 '■' (heretofore)、' S ' (since)、' Z ' (zince、または弱過去)。
- 現在および未来の時間接続詞: 「◯」(次)、「◇」(いつか)、「□」(いつも)、「U 」 (まで)、「W 」 (ない限り)。
接続詞{◎,●,◆,■,◯,◇,□}は単項接続詞であり、残りは二項接続詞です。
厳密な過去接続詞
最後の弱点
●ρは、前回ρが真であった場合、現在成立する。●ρが時間の始まりにおいて解釈された場合、実際の前回が存在しなくても成立する。したがって、最後に「弱い」が現れる。
強い最後
◎ρは、前回ρが真であった場合、現在成立する。◎ρが時間の始まりにおいて解釈された場合、実際の前回が存在しないため成立しない。したがって、「強い」は最後にある。
だった
◆ ρ が過去のどの瞬間においても真であったならば、ρ は現在も満たされている。
これまで
■ ρ が過去のすべての瞬間に真であった場合、ρ は今満たされます。
以来
ψ が以前のどの瞬間にも真であり、ρ がその瞬間以降のすべての瞬間に真である場合、 ρ S ψは満たされます。
亜鉛、または弱いので
ρ Z ψが満たされるのは、(ψ が以前のどの瞬間にも真であり、ρ がその瞬間以降のすべての瞬間に真である場合)、または ψ が過去に発生していない場合です。
現在と未来の接続詞
次
ρが次の瞬間に真であれば、 ◯ρは今満たされます。
いつか
◇ρが現在または将来の任意の時点で真である場合、ρ は現在満たされます。
いつも
□ ρが現在および将来のすべての瞬間に真である場合、 ρは現在満たされます。
それまで
ψ が将来のどの瞬間にも真であり、ρ がそれ以前のすべての瞬間に真である場合、 ρ U ψ は現在満たされます。
ない限り
ρ W ψ は、(ψ が将来のどの瞬間にも真であり、ρ がそれ以前のすべての瞬間に真である)、または ψ が将来発生しない場合に、現在満たされます。
参考文献
- ^ "core.ac.uk" (PDF) .
外部リンク
- MetateMインタープリタのJava実装はここからダウンロードできます。
