What’s CTL Good For?
I said that CTL, despite its simplicity, is actually very useful. What’s it really good for?
One of the main uses of CTL is something called model checking. (I’m not going to go into detail, because the details have easily filled whole books themselves. If you want to know more about model checking with CTL, I recommend Clarke’s textbook [CGP99].) Model checking is a technique used by both hardware and software engineers to check the correctness of certain temporal aspects of their system. They write a specification of their system in terms of CTL, and then they use an automated tool that compares an actual implementation of a piece of hardware or software to the specification. The system can then verify whether or not ...
Become an O’Reilly member and get unlimited access to this title plus top books and audiobooks from O’Reilly and nearly 200 top publishers, thousands of courses curated by job role, 150+ live events each month,
and much more.
Read now
Unlock full access