Concurrent MetateM

Concurrent MetateM is a multi-agent language in which each agent is programmed using a set of (augmented) temporal logic specifications of the behaviour it should exhibit. These specifications are executed directly to generate the behaviour of the agent. As a result, there is no risk of invalidating the logic as with systems where logical specification must first be translated to a lower-level implementation.

MetateM is motivated by the separated normal form, where any formula in linear temporal logic can be rewritten as finitely many formulas of the form "past implies future". Execution proceeds by a process of continually matching rules against a history, and firing those rules when antecedents are satisfied. Any instantiated future-time consequents become commitments which must subsequently be satisfied, iteratively generating a model for the formula made up of the program rules.

Temporal Connectives

The Temporal Connectives of Concurrent MetateM can divided into two categories. The connectives {◎,●,◆,■,◯,◇,□} are unary; the remainder are binary. The semantics of each operator is listed below.

Strict past time connectives

Weak Last: ●ρ is satisfied now if ρ was true in the previous time. If ●ρ is interpreted at the beginning of time, it is satisfied despite there being no actual previous time. Hence "weak" last.
Strong Last: ◎ρ is satisfied now if ρ was true in the previous time. If ◎ρ is interpreted at the beginning of time, it is not satisfied because there is no actual previous time. Hence "strong" last.
Was: ◆ρ is satisfied now if ρ was true in any previous moment in time.
Heretofore: ■ρ is satisfied now if ρ was true in every previous moment in time.
Since: ρSψ is satisfied now if ψ is true at any previous moment and ρ is true at every moment after that moment.
Zince, or weak since: ρZψ is satisfied now if (ψ is true at any previous moment and ρ is true at every moment after that moment) OR ψ has not happened in the past.

Present and future time connectives

Next: ◯ρ is satisfied now if ρ is true in the next moment in time.
Sometime: ◇ρ is satisfied now if ρ is true now or in any future moment in time.
Always: □ρ is satisfied now if ρ is true now and in every future moment in time.
Until: ρUψ is satisfied now if ψ is true at any future moment and ρ is true at every moment prior.
Unless: ρWψ is satisfied now if (ψ is true at any future moment and ρ is true at every moment prior) OR ψ does not happen in the future.

References

1 2 3 Barringer, H.; Fisher, M.; Gabbay, D.; Gough, G.; Owens, R. (1995-09-01). "MetateM: An introduction". Formal Aspects of Computing. 7 (5): 533–549. doi:10.1007/BF01211631. ISSN 1433-299X.
↑ Fisher, Michael (1997). "A Normal Form for Temporal Logics and its Applications in Theorem-Proving and Execution". Journal of Logic and Computation. 7 (4): 429–456. doi:10.1093/logcom/7.4.429. ISSN 1465-363X.

[:0-1] 1 2 3 Barringer, H.; Fisher, M.; Gabbay, D.; Gough, G.; Owens, R. (1995-09-01). "MetateM: An introduction". Formal Aspects of Computing. 7 (5): 533–549. doi:10.1007/BF01211631. ISSN 1433-299X.

[2] Fisher, Michael (1997). "A Normal Form for Temporal Logics and its Applications in Theorem-Proving and Execution". Journal of Logic and Computation. 7 (4): 429–456. doi:10.1093/logcom/7.4.429. ISSN 1465-363X.