并发MetateM

并发MetateM是一种多代理语言，在这种语言中，每个代理都是用一组它应该表现的行为的（增强的）时间逻辑规范来编程的。这些规范被直接执行以产生代理的行为。因此，不存在逻辑无效的风险，就像那些必须首先将逻辑规范翻译成低级别的实现的系统。MetateM概念的根源是Gabbay的分离定理；任何任意的时间逻辑公式都可以被改写成逻辑上等同于过去→未来的形式。执行的过程是不断地将规则与历史相匹配，并在前因得到满足时启动这些规则。任何实例化的未来时间的结果成为承诺，随后必须得到满足，反复生成由程序规则组成的公式模型。

下一个◯ρ现在满足，如果ρ在下一个时间点是真的。某个时候◇ρ现在满足，如果ρ在现在或在未来的任何时刻都是真的。如果ρ在现在和未来的每一时刻都是真实的，那么现在就满足了□ρ。如果ψ在未来任何时刻为真，且ρ在之前的每一时刻为真，则直到ρUψ现在得到满足。