A forum for Spin users
You are not logged in.
Pages: 1
The LTL/CTL patterns database is a well-known useful resource that can provide help in finding the right formalization of temporal properties:
http://patterns.projects.cis.ksu.edu/documentation/patterns.shtml
The Buchi Store http://buchi.im.ntu.edu.tw/ is a similar repository of Buchi automata and their complements for common specification patterns and temporal formula. The three smallest automata known for each formula are provided. You can upload new automata if you discover a smaller equivalent.
The Goal tool http://goal.im.ntu.edu.tw/ is a graphical interactive tool for defining and manipulating Buchi automata and temporal logic formulae.
Offline
Pages: 1