Automata, Games, and Verification Bernd Finkbeiner


Solutions for WQ9.3/WQ9.4

Written: 14.12.2018 11:23 Written By: Bernd Finkbeiner

Questions 9.3 and 9.4.1 in today's warm-up questions were a little tricky. Here are the solutions:


First, interpret x as a second-order variable. Then, replace each x in \varphi by the first-order variable y. Finally, apply the last rule.
Note that, as many of you pointed out, the rule that replaces t=S(x) with S(t)∈x is not sound.

WQ9.4.1 (the formula on the top left)
The two languages are not the same.
For WS1S: L(\varphi ) is the set of all sequences over {∅,{Z}}.
For S1S: L(ψ)=L(\varphi ) - {∅ω}

Have a great weekend,
the Automata, Games, and Verification Team

Privacy Policy | Legal Notice
If you encounter technical problems, please contact the administrators