Loading...
Please wait, while we are loading the content...
A Bounded Model Checker for Three-Valued Abstractions of Software Systems – Proofs
| Content Provider | Semantic Scholar |
|---|---|
| Author | Timm, Nils Gruner, Stefan Harvey, Matthias |
| Copyright Year | 2016 |
| Abstract | Proof of Theorem 1. We prove Theorem 1 by showing that for each b-bounded path π in M there exits an assignment απ : Atoms[0,b] → {true, false} that exactly characterises π in [[Sys]]b , i.e. the transition values along π and απ([[Sys]]b) are identical and the labellings along π and απ([[Sys]]b) are identical as well (Lemma 1). Moreover, we show that the evaluation of an LTL property ψ on ψ yields the same result as απ([[ψ]]b) (Lemma 2). Note that the encoding of states (Definitions 7 and 8) always yields a conjunction of literals. Hence, for each state encoding enc(〈l , s〉)k (resp. enc(l)k and enc(s)k ) there exists exactly one assignment to its atoms that makes the encoding true. We denote such an assignment characterising a state 〈l , s〉 by α〈l,s〉 (resp. αl and αs): Definition 13. (Assignments Characterising States) Let 〈l , s〉 be a state of a Kripke structure M and let k ∈ N arbitrary but fixed. The encodings enc(l)k and enc(s)k are conjunctions of literals. Hence, there exists exactly one satisfying assignment to its atoms. We denote these satisfying assignment as αl resp. αs and we have by definition that the following holds: |
| File Format | PDF HTM / HTML |
| Alternate Webpage(s) | https://cs.up.ac.za/cs/ntimm/ProofTheorem1.pdf |
| Language | English |
| Access Restriction | Open |
| Content Type | Text |
| Resource Type | Article |
