Once a requirement is expressed as an LTL formula, a model checker can automatically verify this property against the model.
Όταν μια απαίτηση εκφράζεται σαν πρόταση LTL, ένας ελεγκτής μοντέλων μπορεί αυτόματα να επαληθεύσει αυτήν την ιδιότητα σε σχέση με το μοντέλο.