Na seminarium przedstawię (w zarysie) semantykę operacyjną i
denotacyjną rachunku procesów, nad którym ostatnio pracuję. Rachunek
przypomina CSP Hoare'a, ma jednak kilka nietypowych cech:
- Alfabety procesów podzielone są na akcje wejściowe i wyjściowe.
- Semantyka uwzględnia obliczenia nieskończone bezpośrednio (a nie
jako granice łańcuchów obliczeń skończonych).
- Obliczenia procesu reprezentowane są nie przez ciągi (czyli liniowe
porządki) akcji, a przez częściowe porządki etykietowane akcjami (tzw.
pomsety).
Nie jesteś zalogowany |
