Specifying State Machines with Temporal Logic
May 3, 2021Programming 12 Minute Read Quickstrom uses linear temporal logic (LTL) for specifying web applications. When explaining how it works, I’ve found that the basics of LTL are intuitive to newcomers. On the other hand, it’s not obvious how to specify real-world systems using LTL. That’s why I’m sharing some of my learnings and ideas from the past year in the form of blog posts. This post focuses on how to use LTL to specify systems in terms of state machines. It’s a brief overview that avoids going into too much detail. For more information on how to test web applicatio...
Source: wickstrom.tech