CompSys705

Missed beginning of the lecture. Fixing OASIS bugs. State formulas are checked at a CTL node. Path formulas are checked all paths.

Homework: draw CTL for AG EFq and EG AFq.

Minimal set of CTL: EX, EG, EU. Fixed point algorithm to check mdel expressed as minimal CTL. Break the formula into parts. Fixed point algorithms.

Composed and transmitted from my iPod Touch