דנה פיסמן

We study the relation between logical contradictions such as p Λ ¬p and structural contradictions such as p ∩ (p q). Intuitively, we expect the two to be treated similarly, but they are not by PSL, nor by SVA. We provide a solution that treats both kinds of contradictions in a consistent manner. The solution reveals that not all structural contradictions are created equal: we must distinguish between them in order to preserve important characteristics of the logic. A happy result of our solution is that it provides the semantics over the natural alphabet 2 ^P , as opposed to the current semantics of PSL/SVA that use an inflated alphabet including the cryptic letters ⊤ and ⊥. We show that the complexity of model checking PSL/SVA is not affected by our proposed semantics.