index.md (2171B)
1 +++ 2 title = 'Model transformations (tree unravelling, bisimulation contraction)' 3 template = 'page-math.html' 4 +++ 5 # Transforming and constructing models 6 Disjoint union of models: combine models by union of states, relations, and valuations. 7 A state in one of the models is modally equivalent with the state in the union. 8 9 Generated submodel: starting from state w, only take its future. 10 11 ## Tree unraveling 12 Tree unravelling: unravelling of world s in (W,R,V) is: 13 - $W' : (s_{1} \dots s_{n})$ with $s_{1} = s$ and $Rs_{i} s_{i+1}$ 14 - $R'$ relates ($s_{1} \dots s_{n}$) to ($s_{1} \dots s_{n+1}$) if $Rs_{n} s_{n+1}$ 15 - $V'(p) = \{ (s_{1} \dots s_{n} | s_{n} \in V(p) \}$ 16 - a state in (W',R',V') is bisimilar to $s_{n}$ in (W,R,V) 17 - if φ is satisfiable in M,w it is satisfiable in tree unravelling of s in M 18 19 Basically taking the states with possible paths between them, and drawing a tree. 20 21 Example: 22 23 <table> 24 <tr> <th>Model</th> <th>Tree unraveling</th> </tr> 25 26 <tr> 27 <td> 28 29  30 31 <details> 32 <summary>Graphviz code</summary> 33 34 <!-- :Tangle(dot) model-diagram.dot --> 35 ```dot 36 digraph g { 37 1 -> 2 38 1 -> 1 39 } 40 ``` 41 42 </details> 43 </td> 44 <td> 45 46  47 48 <details> 49 <summary>Graphviz code</summary> 50 51 <!-- :Tangle(dot) tree-unraveling.dot --> 52 ```dot 53 digraph g { 54 a [label="(1)"] 55 b [label="(1,2)"]; a -> b 56 c [label="(1,1)"]; a -> c 57 d [label="(1,1,2)"]; c -> d 58 e [label="(1,1,1)"]; c -> e 59 f [label="(1,1,1,2)"]; e -> f 60 g [label="..."]; e -> g 61 } 62 ``` 63 64 </details> 65 66 </td> 67 </tr> 68 </table> 69 70 If two trees have the same structure, the models are bisimilar. 71 72 ## Model contraction 73 Bisimulation contraction 74 - W' consists of equivalence classes |s| = { t such that $s \underline{\leftrightarrow} t$ } 75 - R' relates |s| to |t| if Ruv for some u ∈ |s| and some v ∈ |t| 76 - V'(p) = { |s| | s ∈ V(p) } 77 78 Basically getting rid of 'unnecessary' states. 79 See in this diagram, model on the left and contraction on the right: 80 81  82 83 ## Validity and satisfiability 84 If φ is satisfiable, then it is satisfiable using a model with at most $2^{s(\phi)}$ elements with s(φ) the number of subformulas of φ.