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

Document Formalization Choices for `HML` Data Type in the Theory File #14

Closed betawave closed 10 months ago

betawave commented 1 year ago

While casting the definition of HML formulas in the paper into an Isabelle data type we made some choices that diverge from the original definition:

  1. Inclusion of an HML_true data constructor
  2. Modelling infinite conjunctions via an index set and a map

We need to document the original definition in the Isabelle theory. Additionally, above list of divergence needs to be included. For each item on this list, a small justification shall be given, explaining:

  1. why the change was made
  2. why this is unproblematic
benkeks commented 1 year ago

As nobody has been assigned this issue, I assume that nothing has happened here and push the issue as “fresh” to the backlog.