sawine@1: Linear-Time Temporal Logic and Büchi Automata:
sawine@1: 
sawine@1: + examples
sawine@1: + referencing
sawine@1: - bad title
sawine@1: - syntax mixed with interpretation
sawine@1: - no introduction to omega-regular languages
sawine@1: - short introduction to LTL semantics
sawine@4: - no automata complement construction
sawine@41: - on-the-fly construction is too short
sawine@28: 
sawine@12: - error on page 5: there must not be a state g in G along r
sawine@28: - error on page 12: V : S -> 2^P
sawine@34: - error on page 15: dnf: Phi^+ -> set of subsets (power set)
sawine@1: 
sawine@1: graphs:
sawine@1: 
sawine@1: + time progression, linear time ect.
sawine@1: + infinite words as functions
sawine@1: + ltl model as graph
sawine@4: + state space culling