Λογισμός των Επικοινωνούντων Συστημάτων

Από τη Βικιπαίδεια, την ελεύθερη εγκυκλοπαίδεια
Μετάβαση σε: πλοήγηση, αναζήτηση

Ο Λογισμός των Επικοινωνούντων Συστημάτων (Calculus of Communicating Systems ή CCS) είναι ένας λογισμός διεργασιών (process calculus) που εμφανίστηκε τη δεκαετία του 1980 από τον Robin Milner και ονομάστηκε από τον τίτλο του βιβλίου που περιέγραφε το λογισμό. Οι ενέργειές του μοντελοποιούν αδιαίρετες επικοινωνίες μεταξύ ακριβώς δύο συμμετεχόντων. Η τυπική γλώσσα περιλαμβάνει βασικά στοιχεία για την περιγραφή της παράλληλης σύνθεσης, της επιλογής μεταξύ ενεργειών και του περιορισμού εμβέλειας. Ο CCS είναι χρήσιμος για την εκτίμηση της ορθότητας ιδιοτήτων ενός συστήματος όπως τα αδιέξοδα (deadlocks) και τα ζωντανά αδιέξοδα (livelocks).[1]

Σύμφωνα με το Milner, "Δεν υπάρχει κάτι κανονικό σχετικά με την επιλογή των βασικών συνδυαστών, αν και επιλέχθηκαν με προσοχή στην οικονομία. Αυτό που χαρακτηρίζει το λογισμό μας δεν είναι η ακριβής επιλογή των συνδυαστών αλλά η επιλογή της ερμηνείας και του μαθηματικού πλαισίου".[2]

Οι εκφράσεις της γλώσσας ερμηνεύονται σαν συστήματα μεταβάσεων με ετικέτες (labelled transition systems). Ανάμεσα σε αυτά τα μοντέλα, σαν σημασιολογική ισοδυναμία χρησιμοποιείται η αμφιομοιότητα (bisimilarity).

Σύνταξη[Επεξεργασία | επεξεργασία κώδικα]

Δεδομένου ενός συνόλου από ονόματα ενεργειών, το σύνολο των διεργασιών του CCS ορίζεται από την εξής γραμματική BNF:

P ::= \emptyset\,\,\, | \,\,\,a.P_1\,\,\, | \,\,\,A\,\,\, | \,\,\,P_1+P_2\,\,\, | \,\,\,P_1|P_2\,\,\, | \,\,\,P_1[b/a]\,\,\, | \,\,\,P_1{\backslash}a\,\,\,

Τα μέρη της σύνταξης, με τη σειρά που δόθηκαν παραπάνω, είναι

κενή διεργασία 
η κενή διεργασία \emptyset είναι έγκυρη διεργασία του CCS
ενέργεια 
η διεργασία a.P_1 μπορεί να εκτελέσει μια ενέργεια a και συνεχίζει σαν διεργασία P_1
αναγνωριστικό διεργασίας 
γράφεται σαν A \overset{\underset{\mathrm{def}}{}}{=} P_1 για να χρησιμοποιήσει το αναγνωριστικό A για να αναφερθεί στη διαδικασία P_1
επιλογή 
η επιλογή P_1+P_2 μπορεί να προχωρήσει είτε σαν διαδικασία P_1 είτε σαν διαδικασία P_2
παράλληλη σύνθεση 
η P_1|P_2 δηλώνει ότι οι διεργασίες P_1 και P_2 υπάρχουν την ίδια στιγμή
μετονομασία 
η P_1[b/a] είναι η διεργασία P_1 με όλες τις ενέργειες με όνομα a να μετονομάζονται σαν b
περιορισμός 
η P_1{\backslash}a είναι η διεργασία P_1 χωρίς την ενέργεια a

Σχετικοί λογισμοί και μοντέλα[Επεξεργασία | επεξεργασία κώδικα]

  • Επικοινωνούσες Ακολουθιακές Διεργασίες (Communicating Sequential Processes, CSP), από τον Τόνυ Χόαρ, μια γλώσσα που εμφανίστηκε την ίδια εποχή με τον CCS.
  • Ο π-λογισμός (pi-calculus), που αναπτύχθηκε από το Milner στα τέλη της δεκαετίας του 1980, προσφέρει κινητικότητα (mobility) των επικοινωνιών, επιτρέποντας στις διεργασίες να ανταλλάσσουν ονόματα καναλιών επικοινωνίας.
  • Η PEPA, αναπτύχθηκε από τη Jane Hillston και εισάγει χρονισμό ενεργειών (activity timing) και πιθανοτική επιλογή (probabilistic choice), επιτρέποντας μετρήσεις αποδοτικότητας.

Κάποιες άλλες γλώσσες που βασίστηκαν στο CCS:

Μοντέλα που έχουν χρησιμοποιηθεί στη μελέτη συστημάτων τύπου CCS:

Παραπομπές[Επεξεργασία | επεξεργασία κώδικα]

  1. Herzog, Ulrich, επιμ. (May 2007). «Tackling Large State Spaces in Performance Modelling». Formal Methods for Performance Evaluation. Lecture Notes in Computer Science. 4486. Springer. σελ. 318–370. doi:10.1007/978-3-540-72522-0. http://aesop.doc.ic.ac.uk/pubs/large-state-spaces/. Ανακτήθηκε στις 2009-04-21. 
  2. "There is nothing canonical about the choice of the basic combinators, even though they were chosen with great attention to economy. What characterises our calculus is not the exact choice of combinators, but rather the choice of interpretation and of mathematical framework"

Αναφορές[Επεξεργασία | επεξεργασία κώδικα]

  • 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-131-15007-3. 1989
Στο λήμμα αυτό έχει ενσωματωθεί κείμενο από το λήμμα Calculus of communicating systems της Αγγλόγλωσσης Βικιπαίδειας, η οποία διανέμεται υπό την GNU FDL και την CC-BY-SA 3.0. (ιστορικό/συντάκτες).