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 ...
Get Good Math now with the O’Reilly learning platform.
O’Reilly members experience books, live events, courses curated by job role, and more from O’Reilly and nearly 200 top publishers.
