11 lines
800 B
Markdown
11 lines
800 B
Markdown
# coalgebraic-simulation
|
|
|
|
## Checklist
|
|
|
|
- [ ] Introduce HJ-simulation in relator-form, show uniqness of wittnesses.
|
|
- [ ] Prove a general theorem that symmetric simulation for symmetrized relator yields similarity that is sound and complete for behavioral equivalence (use "Relators and Notions of Simulation Revisited" soundness and compteleness criterion).
|
|
- [ ] Elaborate this for powerset
|
|
- [ ] When is symmetrized relator the Barr relator (definition is in "Relators and Notions of Simulation Revisited")?
|
|
- [ ] At least, try to prove it for the Jacobs-Hughes relator
|
|
- [ ] Introduce notions of simulation, diverging from HJ-simulation. Do we need two of them (with normalization and without)? How are all of them related?
|
|
- [x] Can we separate Hughes-Jacobs relator from one-sided lax relator? |