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

Remove index set from hml datatype definition #17

Closed robincgit closed 12 months ago

robincgit commented 1 year ago

Is there anything obviously wrong with this? See this discussion for my choice of countable sets.

Btw, does anyone here know Manuel Eberl personally? I would really like to meet him :)

benkeks commented 1 year ago

It's not wrong per se. You might have seen that we too used cset in https://github.com/maxpohlmann/Reducing-Reactive-to-Strong-Bisimilarity/blob/master/isabelle/HM_Logic.thy . The downside is that the Hennessy–Milner theorem then only works on transition systems with countable branching degree.

robincgit commented 1 year ago

No, I haven't seen that repo yet. Thanks for the link, I'll take a look.

Regarding the downside: isn't that also the case if we take our index set to be the state set. Or are we aiming for a theory admitting uncountably infinite states?

benkeks commented 1 year ago

If the state type (not set!) is the same as the index type, then you automatically get matching cardinality. Then, the theory also works if the state type is real, for instance.

benkeks commented 1 year ago

@robincgit Would you be okay with us closing this PR to increase overview?

betawave commented 12 months ago

I think we may close this PR. We decided for taking another approach.