Podobieństwa i różnice w głównych algebrach procesowych

Według mojej wiedzy istnieją trzy główne algebry procesowe, które zainspirowały szeroki zakres badań nad formalnymi modelami współbieżności. To są:

• CCS i -calculus oba autorstwa Robina Milnera$\pi$
• CSP Tony Hoare i
• ACP: Jan Bergstra i Jan Willem Klop

Wydaje się, że wszyscy trzej mają do dzisiaj dość aktywną obserwację i przeprowadzono na nich ogromne ilości badań.

Jakie są kluczowe podobieństwa i różnice tych podejść? Dlaczego badania algebry procesowej są rozbieżne zamiast zbieżne, w tym sensie, że nie ma jednego uniwersalnego modelu ujednolicającego pole?

Znam tylko CSP i CCS / rachunek pi (nie ACP).

CSP było motywowane imperatywnymi procesami programowania komunikującymi się za pośrednictwem wiadomości. Hoare następnie próbował wyprowadzić z niego prosty rachunek różniczkowy. Z drugiej strony CCS było próbą stworzenia podstawowego rachunku różniczkowego, takiego jak rachunek lambda. Biorąc pod uwagę ich pierwotne punkty początkowe i ostateczną formę, powiedziałbym, że raczej się zbiegli niż rozeszli.

Wspólne dla CSP i CCS jest to, że oba oparte są na pojęciu „procesu” (a przez to rozumiem abstrakcyjne pojęcie wydarzeń ułożonych w czasie). Główna różnica między nimi polega na tym, że CSP ma dwie formy wyboru (wewnętrzny / zewnętrzny lub niedeterministyczny / deterministyczny). W CCS oba pomysły są połączone w jeden. Myślę, że to nie do pogodzenia różnica.

Rozróżnienie między wyborem wewnętrznym i zewnętrznym pozwala CSP na semantykę pod względem śladów liniowych. Z drugiej strony semantyka CCS musi opierać się na drzewach.

Myślę, że obecny plan Hoare'a dotyczący „teorii ujednolicenia” polega na umieszczeniu ich obu w jednym systemie. Musimy poczekać i zobaczyć, co on wymyśli!

Kolejna częściowa odpowiedź.

Podejście do semantyki stosowane przez różne społeczności różniło się, przynajmniej pierwotnie.

• Semantyka ACP jest aksjomatyczna / algebraiczna.
• Semantyka CSP jest denotacyjna, ogólnie pod względem śladów.
• Semantyka CCS / -calculus działa, ogólnie w kategoriach oznaczonych systemów przejściowych.$\pi$

Oczywiście od oryginalnej semantyki opracowano więcej modeli. Ale z pewnością interesujące jest to, że oryginalni badacze zaczęli od różnych podejść semantycznych.

Odpowiadając (przynajmniej) na część pytania dotyczącą tego, dlaczego badania rozeszły się zamiast zbiegły.

Nie będąc ekspertem od algeb procesu, zastanawiałem się kiedyś dokładnie nad tym samym: dlaczego jest tyle teorii? Parrow: Expressiveness of Process Algebras, 2008 wskazał mi ankietę . Myślę, że jest bardzo ładnie napisany i nawet nowicjusz mógłby to zrozumieć.

Parrow bada wyrazistość algeb i odpowiada na pytanie. Krótko mówiąc, różne teorie są różnego rodzaju narzędziami do rozwiązania wielkiego zadania.