Párhuzamos és elosztott rendszereket gyakran írunk le folyamathálózatok formájában [[???Hoa 78, ???Hoa 85]]. A folyamatokat dobozokkal jelöljük, a folyamatok közötti kommunikáció formája üzenetküldés. Az üzeneteket egyirányú kommunikációra alkalmas csatornákon keresztül juttatja el a feladó a címzettnek, címzetteknek. Feltételezzük, hogy az üzenettovábbítás megbízható, üzenetek nem veszenek el, nem sérülnek meg, csak a valóban elküldött üzenetek érkeznek meg. Az üzenetküldés aszinkron, a feladó általában rögtön folytatja tevékenységét miután a csatornára elhelyezte az üzenetet, nem kell megvárnia az üzenet átvételét. A csatornák sor típusú változóként viselkednek, átmenetileg képesek tárolni a már elküldött, de még nem fogadott üzeneteket. A csatorna kapacitása határozza meg a tárolható üzenetek számát. Ha a csatorna kapcitása korlátos, akkor előfordulhat, hogy a küldő fél nem tudja rögtön elhelyezni üzenetét és várakozni kell, amíg a csatorna képes nem lesz újabb üzenet fogadására. Minden csatornához két sor típusú változó tartozik, az egyik a csatornán várakozó üzeneteket tartalmazza (a csatorna aktuális állapota), a másik a csatorna története. A csatorna története minden olyan üzenetet tartalmaz helyes sorrendben, amelyik valaha rákerült a csatornára, a történetváltozóról a fogadó fél nem távolítja el az üzeneteket. A történetváltozót egy felülvonással jelöljük. A történetváltozó tárolása a valóságban nehezen vagy egyáltalán nem megoldható, mert egy hosszú ideig futó programban az üzenetek száma idővel minden korlátot meghaladhat. Történetváltozókat ezért csak úgy használunk értékadásokban, hogy értéküket csak saját új érték meghatározásához használjuk fel. Ezek az egyszerű értékadások elhagyhatóak anélkül, hogy a program többi részének működése megváltozna.

A ábrán két folyamatot és az őket összekötő csatornát láthatjuk. A csatornára a folyamat helyezhet el üzenetet, egész számok formájában. A folyamat olvas a csatornáról. Az alábbi műveletek tartoznak a csatorna típusú változókhoz:

Az alábbiakban megadjuk az egyes műveletek pontos jelentését is. Elemi műveletek jelentését megadhatjuk hatásrelációjukkal, vagy azzal ekvivalens módon a leggyangébb előfeltételük kiszámításának meghatározásával is.

Figyeljük meg, hogy üzenetküldés leggyengébb előfeltételének kiszámításakor a csatorna történetét is helyettesíteni kell az utófeltételben, míg az üzenet eltávolítása nem érinti a történetváltozót.

Ha a folyamatok közötti kommunikációra nem használunk osztott változókat, hanem kizárólag csatronaváltozók segítségével oldjuk meg az információ cseréjét, akkor az egyes folyamatok közötti kapcsolat jól ellenőrizhetővé válik. A lokalitás tétel állítását fogalmazhatjuk újra speciális formában: