Definizione: Due modelli di Kripke $M_1$ e $M_2$ con stati iniziali $q_0$ e $s_0$, si ha che essi sono equivalenti rispetto ad una logica $I$ (che può essere LTL, CTL, ecc…) se, per ogni formula $\alpha\in FBF_I$, si ha:

$$ M_1, q_0 \vDash \alpha \iff M_2, s_0 \vDash \alpha $$

Avendo che i due modelli sono effettivamente indistinguibili. L’equivalenza è quindi in funzione di proprietà della logica stessa.

• Esempi

Insiemi Parzialmente Ordinati

Definizione: Si ha che una relazione parziale $\leq$ su $A$

$$ \leq \ \subseteq A\times A $$

è:

• riflessiva, infatti $x\leq x$, $\forall x \in A$
• antisimmetrica, infatti $(x \leq y \land y \leq x)\implies x = y, \ \forall x, y \in A$
• transitiva, infatti $(x \leq y \land y \leq z)\implies x \leq z, \ \forall x , y, z\in A$

La notazione $x<y$ significa $x \leq y \land x \neq y$.

Definizione: Dato $(A, \leq )$ un insieme parzialmente ordinato e $B \subseteq A$ si definiscono:

• $x \in A$ è un maggiorante di $B$ se $y \leq x, \ \forall y \in B$
• $x \in A$ è un minorante di $B$ se $x \leq y, \ \forall y \in B$
• $B^*$ come insieme dei maggioranti di $B$
• $B_*$ come insieme dei minoranti di $B$
• $B$ è superiormente limitato se $B^* \neq \empty$
• $B$ è inferiormente limitato se $B_* \neq \empty$