Concurrent MetateM is a multi-agent

Multi-agent system

A multi-agent system is a system composed of multiple interacting intelligent agents. Multi-agent systems can be used to solve problems that are difficult or impossible for an individual agent or a monolithic system to solve...

 language in which each agent is programmed using a set of (augmented) temporal logic

Temporal logic

In logic, the term temporal logic is used to describe any system of rules and symbolism for representing, and reasoning about, propositions qualified in terms of time. In a temporal logic we can then express statements like "I am always hungry", "I will eventually be hungry", or "I will be hungry...

 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.

The root of the MetateM concept is Gabbay's separation theorem

Gabbay's separation theorem

In mathematical logic and computer science, Gabbay's separation theorem, named after Dov Gabbay, states that any arbitrary temporal logic formula can be rewritten in a logically equivalent "past → future" form. I.e. the future becomes what must be satisfied. This form can be used...

; any arbitrary temporal logic formula can be rewritten in a logically equivalent

Logical equivalence

In logic, statements p and q are logically equivalent if they have the same logical content.Syntactically, p and q are equivalent if each can be proved from the other...

 past → future form. Execution proceeds by a process of continually matching rules against a history, and firing those rules when antecedent

Antecedent

An antecedent is a preceding event, condition, cause, phrase, or word. It may refer to:* Antecedent moisture, a hydrologic term describing the relative wetness condition of a sewershed.* Antecedent , the first half of a hypothetical proposition....

s 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, as follows:

• Strict past time connectives: '●' (weak last), '◎' (strong last), '◆' (was), '■' (heretofore), S (since), and Z (zince, or weak since).

• Present and future time connectives: '◯' (next), '◇' (sometime), '□' (always), U (until), and W (unless).

The connectives {◎,●,◆,■,◯,◇,□} are unary; the remainder are binary.

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.

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.

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.