Concurrent MetateM is a
multi-agent
A multi-agent system (MAS or "self-organized system") is a computerized system composed of multiple interacting intelligent agents.Hu, J.; Bhowmick, P.; Jang, I.; Arvin, F.; Lanzon, A.,A Decentralized Cluster Formation Containment Framework fo ...
language in which each agent is programmed using a set of (augmented)
temporal logic In logic, temporal logic is any system of rules and symbolism for representing, and reasoning about, propositions qualified in terms of time (for example, "I am ''always'' hungry", "I will ''eventually'' be hungry", or "I will be hungry ''until'' I ...
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
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
Logic is the study of correct reasoning. It includes ...
; any arbitrary temporal logic formula can be rewritten in a
logically equivalent
Logic is the study of correct reasoning. It includes both formal and informal logic. Formal logic is the science of deductively valid inferences or of logical truths. It is a formal science investigating how conclusions follow from premises ...
''past → future'' form. Execution proceeds by a process of continually matching rules against a history, and ''firing'' those rules when
antecedent
An antecedent is a preceding event, condition, cause, phrase, or word.
The etymology is from the Latin noun ''antecedentem'' meaning "something preceding", which comes from the preposition ''ante'' ("before") and the verb ''cedere'' ("to go").
...
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.
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
External links
* A Java implementation of a MetateM interpreter can be downloaded fro
here
{{DEFAULTSORT:Concurrent Metatem
Artificial intelligence