search

equivio / silent-step-spectroscopy

Isabelle formalization of linear-time–branching-time spectroscopy accounting for silent steps
https://equivio.github.io/silent-step-spectroscopy/AFP/LinearTimeBranchingTimeSpectroscopyAccountingForSilentSteps/index.html
Other
0 stars 0 forks source link

Define HML Subset Expressing Stability Respecting Branching Bisimilarity (SRBB) #29

Closed betawave closed 11 months ago

betawave commented 12 months ago

This PR adds a data type representing a subset of the full hml data type which is able to express stability respecting branching bisimilarity (currently conjectured not proven). Also it defines a translation function, mapping each hml_srbb term to a hml term. Using this translation the semantic function |=SRBB was simply implemented by referring to hmls semantic function |=.

We weight three different implementation strategies:

  1. via a custom data type hml_srbb, wherein the conjunctions use index sets and mapping functions
  2. via a custom data type hml_srbb, wherein the conjunctions use csets
  3. via a predicate on the hml data type, selecting the proper subset

With @benkeks help, we selected the first option, since it seems sufficiently easy to work with, while not constraining the range of LTS that could be described. The second option (using csets), would have provided a nicer representation, while constraining the range of LTS to only such wherein each derivatives set is countable. We discarded the third option, since it was unclear to us, how one would define the expressiveness price function when using this approach.

betawave commented 12 months ago

closes #4

benkeks commented 12 months ago

Would be really nice to merge this soon so that it becomes easier to read the diffs in other PRs!

betawave commented 11 months ago

@benkeks @ekeln Since the two open items (move of TT constructor and renaming of translation sub-function neg to conjunct) have been addressed, i'd like to merge this PR. Do you have any objections?