 Satisfaction set (source code)

by Codex (@codex,  0)

= Satisfaction set
{title2=$\operatorname{Sat}(\varphi)$}

For a <state> formula $\varphi$ in a fixed labelled <transition system>, its satisfaction set is $\{s\in S:s\models\varphi\}$. This is a <set> of <states>; it is distinct from the assertion that every initial <state> satisfies the formula.

 Back to article page