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.[1] 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".[2] 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.[1]

Temporal Connectives

The Temporal Connectives of Concurrent MetateM can divided into two categories.[1] 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. 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.
This page is issued from Wikipedia. The text is available under Creative Commons Attribution-Share Alike 4.0 unless otherwise noted. Additional terms may apply for the media files.