Continuing Labs 12

More demos, with more complex invariant for reachability

• Singly Linked List
• Tree with Parents

Using Automata to Decide WS1S

Examples (using mona and dot) of automata built automatically using MONA.

Expressing finite automata in MSOL over strings

Not covered:

• Remarks on WS1S Complexity

• Tree automata and WSkS

Continue with Lecture 14