| Autor: |
Eisner, Cindy, Fisman, Dana |
| Zdroj: |
Hardware & Software: Verification & Testing (9783642017018); 2009, p164-178, 15p |
| Abstrakt: |
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 2P, 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. [ABSTRACT FROM AUTHOR] |
| Databáze: |
Complementary Index |
| Externí odkaz: |
|
