issues
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 how coordinates define equivalences
#28
Closed
benkeks
closed
11 months ago
benkeks
commented
1 year ago
[x] Define how expressiveness coordinates induce HMLsrbb-subsets and equivalences (i.e. Def. 7 minus the specific coordinates of Fig. 2.)
[x] Show as example that $(\inf, 0,0,0,0,0,0,0)$ characterizes weak trace preoder/equivalence (cf. Ex. 4)
[x] requires to define weak traces and to express how this leads to an equivalence