Η αρχιτεκτονική των ιδιοτήτων στην TLA+
Η TLA+ προσεγγίζει τα συστήματα ως ακολουθίες καταστάσεων (sequences of states). Η ισχύς της έγκειται στη χρήση χρονικών τελεστών (temporal operators) όπως το [] (always) και το <> (eventually). Αυτοί οι τελεστές επιτρέπουν στους μηχανικούς να ορίσουν invariants, διασφαλίζοντας ότι μια συνθήκη παραμένει αληθής σε κάθε κατάσταση του συστήματος. Ωστόσο, η τυπική επαλήθευση (formal verification) περιορίζεται από την ικανότητα του χρήστη να μεταφράσει μια ανθρώπινη έννοια σε λογικό τύπο.
Περιορισμοί και το πρόβλημα των hyperproperties
Ένα κρίσιμο σημείο συμφόρησης (bottleneck) στην TLA+ είναι η αδυναμία της να ορίσει ιδιότητες πάνω σε σύνολα συμπεριφορών. Τα hyperproperties, τα οποία είναι απαραίτητα για την ανάλυση της ασφάλειας (π.χ. non-interference) ή στατιστικών παραμέτρων (π.χ. 95th percentile latency), δεν μπορούν να εκφραστούν φυσικά. Ενώ υπάρχουν τεχνικές όπως η αυτο-σύνθεση (self-composition), αυτές οδηγούν σε εκθετική αύξηση του state space, καθιστώντας τον έλεγχο μοντέλων (model checking) υπολογιστικά ακριβό.
Η παγίδα των τεχνικών παράκαμψης
Πολλοί μηχανικοί προσπαθούν να «μιμηθούν» ιδιότητες που η TLA+ δεν υποστηρίζει εγγενώς, χρησιμοποιώντας βοηθητικές μεταβλητές (auxiliary variables) για την αποθήκευση του ιστορικού καταστάσεων. Αν και λειτουργικές, αυτές οι προσεγγίσεις συχνά καθιστούν τα μοντέλα δυσνόητα και αλλοιώνουν τη σχέση μεταξύ του specification και του τελικού κώδικα. Η χρήση εξειδικευμένων εργαλείων όπως η CTL ή η PRISM ίσως είναι προτιμότερη όταν οι απαιτήσεις του συστήματος ξεφεύγουν από το πλαίσιο των invariants και της απλής ζωντάνιας.