Selected Topics in Design & Verification

Model Checking and Synthesis with SMT

1. Verifying system against LTL spec → checking emptiness for NBW → finding bad lassos in run graph → checking existence of ranking functions → SMT model checking
2. Synthesizing system from LTL spec → using UF to represent transition relation and iterating through the possible numbers of states ($\le ~|B|^{|B|}$) → SMT model checking
3. In 1989, Pnueli and Rosner solved the LTL synthesis problem (2EXPTIME-complete): LTL $\phi$ → NBW (~ $2^{|\phi|}$) → DPW (~ $2^{|\phi|^{|\phi|}}$) → solve the game (~ $2^{|\phi|^{|\phi|}}$)

(DPW: deterministic parity word automata; NBW: nondeterministic Buchi word automata)