Η πληροφορική έχει μπει στα σπίτια σχεδόν όλων μας – το γνωρίζουμε. Η πληροφορική βρίσκεται παντού γύρω μας – το νιώθουμε. Ελέγχει κάθε «έξυπνο» μηχάνημα, σε στεριά, νερό και αέρα – μας λένε… και εκεί αρχίζουμε να τα χάνουμε. Γιατί; Δείτε μέσα από την πόρτα του κυβερνήτη την επόμενη φορά που θα ανεβείτε σε αεροπλάνο και θα καταλάβετε: μυριάδες ηλεκτρονικά υποσυστήματα καταλήγουν σε οθόνες και πλήκτρα μπροστά του, και εμείς – και αυτός – εμπιστευόμαστε τη ζωή μας στο ότι «κάπως» η πληροφορική τα ελέγχει. Πώς μπορούμε να είμαστε σίγουροι; Οταν όλα αυτά δουλεύουν ταυτόχρονα και υπόκεινται κάθε στιγμή σε πολλαπλάσιες αλλαγές παραμέτρων και συνθηκών, πώς είμαστε όλοι – κατασκευαστές, πιλότοι και επιβάτες – σίγουροι ότι όλα δουλεύουν όπως είχαν σχεδιαστεί να δουλέψουν και να αντεπεξέλθουν;
Ε, λοιπόν, είμαστε. Και αυτή τη σιγουριά την οφείλουμε στη σκληρή δουλειά πολλών επιστημόνων, αλλά ιδιαίτερα τριών ανθρώπων. Τριών συναδέλφων από τρεις μεριές της Γης, στους οποίους απονεμήθηκε στις 4 Φεβρουαρίου 2008 το ισοδύναμο ενός Νομπέλ της πληροφορικής, το βραβείο Turing. Οπως μας ενημέρωσε η βραβεύουσα ACM – η κορυφαία παγκοσμίως οργάνωση επιστημόνων πληροφορικής – οι τρεις προμηθείς της ψηφιακής αξιοπιστίας ήταν ο Edmund Clarke (του Πανεπιστημίου Carnegie Mellon), o Allen Emerson (του Πανεπιστημίου Austin του Τέξας) και ο Joseph Sifakis (του Εθνικού Κέντρου Επιστημονικής Ερευνας της Γαλλίας, CNRS). Ο Joseph… Ποιος;
Συλλογάται καλά όποιος…
Μου είπαν ότι ήταν κάποτε ένα παιδί-ζουζούνι στο Ηράκλειο. Σήφη τον φωνάζανε και έπαιζε δυνατά, όπως όλα τα παιδιά της Κρήτης. Μεγάλωσε σε χρόνια τσιτωμένα για τη δημοκρατία μας και δεν άντεχε τα ψέματα. Τη χρονιά που τελείωνε το Καπετανάκειο Λύκειο, το ’64, η δημοκρατία οδηγούνταν ήδη «στο απόσπασμα». Σπούδασε ηλεκτρολόγος-μηχανολόγος στο Μετσόβιο, υπό τη σκέπη του «πουλιού». Αναζήτησε καταφύγιο στα εφαρμοσμένα μαθηματικά και στα θεωρητικά μοντέλα μιας πιο δίκαιης κοινωνίας. Οι άγριες ημέρες πέρασαν, η μεταπολίτευση ήρθε, η πληροφορική βγήκε παγανιά. Το πήρε απόφαση. «Τσίμπησε» μια γαλλική υποτροφία και ξενιτεύτηκε στην Εσπερία για μεταπτυχιακό στην πληροφορική. Μετά την αποφοίτηση παρέμεινε εκεί. Εργάστηκε σκληρά και πεισματάρικα, αλλά δεν τον τρόμαζε πια τίποτε. Είχε μάθει να συλλογάται ελεύθερα και να βλέπει μακριά. Η πολυπλοκότητα των αλγορίθμων και η θεωρία ελέγχου των δικτύων ήταν για αυτόν εκδρομές στον πνευματικό του Ψηλορείτη. Ηθελε ταίρι που να αντέχει στις «ορειβασίες του μυαλού του»; Το βρήκε στο πρόσωπο της Κατερίνας Καπετανάκη, μιας εξαίρετης οικονομολόγου, διακεκριμένης και αυτής σήμερα στον τομέα της. Του έλειπε η πατρίδα; Εμαθε να απαγγέλλει από στήθους όλο τον Σεφέρη και τον Ελύτη. Λαχταρούσε τα αγριοβότανα της Κρήτης; Τραγουδούσε όλα τα ριζίτικα. Και όταν ένιωσε ότι σε κάποιον πρέπει να τα μεταγγίσει όλα αυτά, ήλθαν τα γλυκά του κουτσούβελα: η Ελένη και ο Μανώλης. Πώς λοιπόν να μη λένε όσοι έτυχαν να φιλοξενηθούν στο σπιτικό του, στην Γκρενόμπλ, «ένιωσα την ευγένεια του οικογενειάρχη, την οικογενειακή θαλπωρή, να με περιβάλλουν. Ανευ ορίων, άνευ όρων»…
Ελεγχος μοντέλου
Με αυτόν τον ψυχικό και πνευματικό πλούτο, με αυτή τη στήριξη της ευτυχισμένης οικογένειας, ο Σήφης ανέβηκε γοργά στην εκτίμηση των συναδέλφων του. Η δουλειά του ήταν πάντα πρωτοποριακή και αψεγάδιαστη. Ετσι, όταν άρχισε η αναζήτηση λύσης στη μοντελοποίηση των συστημάτων πραγματικού χρόνου και στην επαλήθευσή τους, ο Σήφης «μπούκαρε στη μάχη» χωρίς φοβίες. Στην αντίπερα όχθη του Ατλαντικού δύο γίγαντες του τομέα, οι Κλαρκ και Εμερσον, είχαν ήδη θέσει τις πρώτες θεωρητικές βάσεις του «Model Checking» όπως το βάφτισαν. Το Model Checking (έλεγχος μοντέλου) είναι αλγοριθμική μέθοδος επαλήθευσης του κατά πόσον ένα μοντέλο συστήματος κυκλωμάτων – ή ενός σύνθετου λογισμικού – πληροί τις προδιαγραφές. Επιπλέον, αν το μοντέλο δεν επαληθευτεί, η μέθοδος παράγει αντιπαραδείγματα τα οποία βοηθούν στον εντοπισμό της πηγής του προβλήματος. Για να μπορέσει όμως το Model Checking να ανταποκριθεί με επιτυχία στην επαλήθευση πολύπλοκων και σύνθετων συστημάτων, έπρεπε να δημιουργηθούν θεωρητικά αποτελέσματα, κατάλληλες μέθοδοι και εργαλεία, ώστε να επιτευχθεί η αποτελεσματική αντιμετώπιση της πολυπλοκότητας του προβλήματος της «έκρηξης καταστάσεων». Ο Σήφης πήρε τη σκυτάλη και τα κατάφερε.
Οι εργασίες και των τριών τους ήταν αυτές που έκαναν τη διεθνή επιστημονική κοινότητα να παραληρεί από τη χαρά της για το ότι «η επίλυση του προβλήματος προήλθε από αξιοσημείωτα γοργή πρόοδο». Οι αλγόριθμοι του Σήφη βρήκαν εφαρμογές παντού – στα αεροπλάνα, στα αυτοκίνητα, στις τηλεπικοινωνίες και στο Διάστημα. Συνεργάστηκε με επιχειρήσεις κολοσσούς, όπως η Airbus, η Schneider Electric, η STMicroelectronics και η France Telecom. Σήμερα, είναι πια διευθυντής έρευνας του Εθνικού Κέντρου Επιστημονικής Ερευνας της Γαλλίας και ιδρυτής του εργαστηρίου Verimag στην Γκρενόμπλ.
Εσπευσα να επικοινωνήσω μαζί του για να τον συγχαρώ. Μου τηλεφώνησε αμέσως μόλις πήρε το μήνυμά μου – αργά το βράδυ, στο γραφείο του. Μου μίλησε ζεστά, σαν να είχαμε πιει κιόλας τσικουδιά – και ας μη με γνώριζε. Πήγα να του πω «πώς γίνεται να ψέλνει σχεδόν ανελλιπώς στην ελληνορθόδοξη εκκλησία της Γκρενόμπλ κάποιος που καθημερινά ασχολείται με… «σενάρια συνωμοσίας» του ψηφιακού κόσμου;». Αλλά δεν τον ρώτησα. Είχα νιώσει ότι «συλλογάται ελεύθερα».
