refinement relation between nondetE trees #42

Activity

1. gmalecha commented on Jan 11, 2019

   

   gmalecha

   on Jan 11, 2019

   Collaborator

   More actions

   We wrote some of this out, didn't we?
2. Lysxia commented on Jan 12, 2019

   

   Lysxia

   on Jan 12, 2019

   Collaborator

   More actions

   There is something like that in our DeepWeb experiment but it's unused. In the VST proof we use trace inclusion, which is a coarser relation, but I'm pretty sure the lemmas we actually proved are all compatible with this tree refinement relation, which is a kind of simulation.
3. Lysxia

   added

   enhancementNew feature or requestNew feature or request

   on Mar 6, 2019
4. Lysxia

   added

   itreesParticular to theory and implementation of itreesParticular to theory and implementation of itrees

   on Mar 27, 2019
5. jeehoonkang commented on Apr 8, 2019

   

   jeehoonkang

   on Apr 8, 2019

   Contributor

   More actions

   I'd also like to use interaction trees for proving behavior refinement (not equivalence) and wonder if supporting simulation (not bisimulation) is on the roadmap. If not, people in my group are willing to contribute to it.
6. Lysxia commented on Apr 8, 2019

   

   Lysxia

   on Apr 8, 2019 via email

   Collaborator

   More actions

   This is in fact likely one of the sooner destinations on the roadmap. I only have very vague ideas at the moment, it would definitely be useful to have more discussion about this. - In our CPP paper we use trace inclusion, where nondeterminism (visible by default) is erased from traces beforehand. That's coarser than simulation of course, but for our purposes of modelling externally visible behavior without liveness concerns it was good enough. But it will take work to generalize. - Since our discussions with Gil about the recent developments in paco, I have a fuzzy idea that there may be a solution using some variant of the concept of respectful closure. - Another place to draw inspiration from is in the literature about the resumption monad (which itree is a variant of). I recently got a sense that they're trying to answer closely related questions, in highly more abstract terms.

   …

   On Mon, Apr 8, 2019, 14:45 Jeehoon Kang ***@***.***> wrote: I'd also like to use interaction trees for proving behavior refinement (not equivalence) and wonder if supporting simulation (not bisimulation) is on the roadmap. If not, people in my group are willing to contribute to it. — You are receiving this because you commented. Reply to this email directly, view it on GitHub <#42 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/ACZhARub46XoI-ymnuUdOn2HUM9C3pb8ks5veznagaJpZM4Z8SyG> .
7. jeehoonkang commented on Apr 9, 2019

   

   jeehoonkang

   on Apr 9, 2019

   Contributor

   More actions

   @Lysxia Thank you for your detailed answer. Your second and third bullet explains ideas on solutions, but I don't quite understand the problem. May I ask if why it would be difficult to support interaction tree refinement?
8. Lysxia commented on Apr 10, 2019

   

   Lysxia

   on Apr 10, 2019

   Collaborator

   More actions

   Good question. I think the main problem is a problem of generality, so I may be getting carried away. Simulation is one example out of many other relations we may want to support, and we might even want to be able to combine some of them. To fit them all under a common framework is why I'm looking at those solutions.

   In this light, a different way to approach this issue is to look at some concrete definition of simulation and decide that it is good enough for most purposes.