Doktorat

Opowiem o formalizmie, mojego autorstwa, do opisu systemów zbudowanych z komponentów, z których każdy porozumiewa się z otoczeniem za pośrednictwem akcji. Podobnie jak np. w CCS i CSP, komunikacja odbywa się przez synchronizację akcji: dwa komponenty można połączyć przez sparowanie 'wyjściowych' akcji jednego z nich, z 'wejściowymi' akcjami drugiego. Do specyfikacji komponentów używam logiki temporalnej (wariantu LTL, linear temporal logic) a za wszystkim stoi model formalny oparty o automaty (albo etykietowane systemy tranzycyjne) z pewnymi moimi rozszerzeniami. Postaram się skupić głównie na przykładzie specyfikacji, pomijając w miarę możliwości technikalia.