Współbieżny MetateM
Concurrent MetateM to wieloagentowy język, w którym każdy agent jest programowany przy użyciu zestawu (rozszerzonych) specyfikacji logiki czasowej zachowania, które powinien wykazywać. Te specyfikacje są wykonywane bezpośrednio w celu wygenerowania zachowania agenta. W rezultacie nie ma ryzyka unieważnienia logiki, jak w przypadku systemów, w których specyfikacja logiczna musi zostać najpierw przetłumaczona na implementację niższego poziomu.
Podstawą koncepcji MetateM jest twierdzenie Gabbay'a o separacji ; dowolna formuła logiki temporalnej może zostać przepisana w logicznie równoważnej formie przeszłość → przyszłość . Egzekucja przebiega w procesie ciągłego dopasowywania reguł do historii i odpalania tych reguł, gdy poprzedniki są spełnione. Wszelkie ukonkretnione konsekwencje w czasie przyszłym stają się zobowiązaniami, które następnie muszą zostać spełnione, iteracyjnie generując model dla formuły złożonej z reguł programu.
Łączniki czasowe
Czasowe łączniki współbieżnego MetateM można podzielić na dwie kategorie, jak następuje:
- Ścisłe spójniki czasu przeszłego: „●” (ostatni słaby), „◎” (ostatni mocny), „◆” (był), „■” (do tej pory), „S” (od ) i „ Z ” ( cynk lub słaby od tego czasu).
- Spójniki czasu teraźniejszego i przyszłego: „◯” (następny), „◇” (kiedyś), „□” (zawsze), „ U ” ( do) i „ W ” (chyba że).
Spójniki {◎,●,◆,■,◯,◇,□} są jednoargumentowe; reszta jest binarna.
Ścisłe spójniki czasu przeszłego
Słaby ostatni
●ρ jest teraz spełnione, jeśli ρ było prawdziwe w poprzednim czasie. Jeśli ●ρ jest interpretowane na początku czasu, to jest spełnione pomimo braku rzeczywistego czasu poprzedniego. Stąd „słaby” ostatni.
Mocne ostatnie
◎ρ jest teraz spełnione, jeśli ρ było prawdziwe w poprzednim czasie. Jeśli ◎ρ jest interpretowane na początku czasu, nie jest spełnione, ponieważ nie ma faktycznego poprzedniego czasu. Stąd „mocny” ostatni.
Był
◆ρ jest teraz spełnione, jeśli ρ było prawdziwe w jakimkolwiek poprzednim momencie.
dotychczas
■ρ jest teraz spełnione, jeśli ρ było prawdziwe w każdym poprzednim momencie.
Od
ρ S ψ jest teraz spełnione, jeśli ψ jest prawdziwe w dowolnej chwili poprzedniej i ρ jest prawdziwe w każdej chwili po tej chwili.
Cynk lub słaby od tego czasu
ρ Z ψ jest spełnione teraz, jeśli (ψ jest prawdziwe w dowolnym momencie poprzednim i ρ jest prawdziwe w każdym momencie po tym momencie) OR ψ nie zdarzyło się w przeszłości.
Spójniki czasu teraźniejszego i przyszłego
Następny
◯ρ jest teraz spełnione, jeśli ρ jest prawdziwe w następnym momencie.
Czasami
◇ρ jest spełnione teraz, jeśli ρ jest prawdziwe teraz lub w dowolnym momencie w przyszłości.
Zawsze
□ ρ jest spełnione teraz, jeśli ρ jest prawdziwe teraz iw każdej przyszłej chwili.
Dopóki
ρ U ψ jest spełnione teraz, jeśli ψ jest prawdziwe w dowolnym momencie w przyszłości i ρ jest prawdziwe w każdym momencie wcześniejszym.
Chyba że
ρ W ψ jest spełnione teraz, jeśli (ψ jest prawdziwe w dowolnym momencie w przyszłości i ρ jest prawdziwe w każdym momencie wcześniejszym) OR ψ nie zachodzi w przyszłości.
Linki zewnętrzne
- Implementację Java interpretera MetateM można pobrać stąd