Beregning af interagerende systemer
Calculus of Communicating Systems ( CCS ) i datalogi er en procesregning udviklet af Robin Milner i 1980. Beregningen arbejder med en model af uadskillelig kommunikation mellem præcis to deltagere. Det formelle sprog indeholder primitiver til at beskrive parallel komposition, valg mellem handlinger og begrænsningsrammer. CCS er nyttigt til at evaluere den kvalitative korrekthed af egenskaber såsom mutex eller " livelock " [1] .
Ifølge Milner "er der intet kanonisk ved valget af grundlæggende kombinatorer, selvom de er valgt med stor omhu for økonomi. Det, der kendetegner vores beregning, er ikke det præcise valg af kombinatorer, men valget af fortolkning og matematisk struktur . "
Sprogudtryk fortolkes som et mærket transitivt system . Mellem disse modeller bruges gensidig lighed som en semantisk ækvivalens.
Syntaks
For et givet sæt handlingsnavne er sættet af CCS-processer defineret af følgende Backus-Naur-grammatik :
![{\displaystyle P::=\emptyset \,\,\,|\,\,\,a.P_{1}\,\,\,|\,\,\,A\,\,\,|\ ,\,\,P_{1}+P_{2}\,\,\,|\,\,\,P_{1}|P_{2}\,\,\,|\,\,\,P_ {1}[b/a]\,\,\,|\,\,\,P_{1}{\backslash }a}](https://wikimedia.org/api/rest_v1/media/math/render/svg/5ead99e00ed96fff0df7c972472973159922c998)
Dele af syntaksen i ovenstående rækkefølge:
tom proces en tom proces er en gyldig CCS-proces handling en proces kan tage en handling og fortsætte som en proces proces-id skriv for at bruge id til at henvise til en proces valg processen kan fortsætte enten som , eller som parallel komposition processer og som eksisterer samtidigt omdøbning proces med handlinger omdøbt til begrænsning proces uden handling
![{\displaystyle P_{1}[b/a]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/e3845d90265f5e16fb07f1cec4e9d827838f4dad)
Relaterede beregninger og modeller
- Calculus of interacting processes ( eng. Communicating sekventielle processer ), CSP er et sprog udviklet af Anthony Hoare , som dukkede op samtidig med CCS.
- Pi-calculus , udviklet af Milner i slutningen af 1980'erne, giver mobilitet til kommunikationsforbindelser ved at tillade processer at rapportere navnene på selve kommunikationskanalerne.
- PEPA Process Algebra , udviklet af Jane Hillston , introducerer handlingstid og sandsynlighedsvalg, hvilket gør det muligt at beregne præstationsmålinger.
Nogle notationer baseret på CCS:
Modeller, der bruges i studiet af CCS-systemer:
- Historie monoid ;_ _
- Skuespillermodellen .
Links
- Robin Milner: A Calculus of Communicating Systems , Springer Verlag, ISBN 0-387-10235-3 . 1980.
- Robin Milner, Communication and Concurrency , Prentice Hall, International Series in Computer Science, ISBN 0-13-115007-3 . 1989
- ↑ Takling af store tilstandsrum i præstationsmodellering // Formelle metoder til præstationsevaluering / Herzog, Ulrich. - Springer, 2007. - Vol. 4486. - S. 318-370. — (Forelæsningsnotater i datalogi). - doi : 10.1007/978-3-540-72522-0 .