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
issues
Newest
Newest
Most commented
Recently updated
Oldest
Least commented
Least recently updated
Bug: formalization error in lifted variant of reflexive and transative closure over silent steps
#75
betawave
closed
10 months ago
15
61 lemma 2 cheap wins imply cheap strat formulas
#74
Vervada
closed
10 months ago
1
Documenting HML and HML_SRBB data types
#73
betawave
closed
9 months ago
4
63 proof of theorem 1 characterization
#72
TheHllm
closed
10 months ago
0
69 cicd add tesst that checks that every thy file is transitvly imported
#71
TheHllm
closed
10 months ago
0
Treat logical equivalences on hml srbb
#70
betawave
closed
10 months ago
4
CI/CD: add check that every .thy file is (transitivly) imported
#69
TheHllm
closed
10 months ago
0
42 define strategy formulas on attacker won region
#68
Vervada
closed
10 months ago
0
63 proof of theorem 1 characterization
#67
TheHllm
closed
10 months ago
1
64 make wina upward closure apply to spectroscopy game
#66
crmrtz
closed
10 months ago
2
Show HML_srbb to characterize SRBB
#65
benkeks
closed
9 months ago
3
Make wina upward closure apply to spectroscopy game
#64
benkeks
closed
10 months ago
0
Proof of Theorem 1 characterization
#63
benkeks
closed
10 months ago
0
Lemma 3: Strat formulas distinguish
#62
benkeks
closed
10 months ago
0
Lemma 2: Cheap wins imply cheap Strat formulas
#61
benkeks
closed
10 months ago
3
Lemma 1: Cheap distinctions imply cheap wins
#60
benkeks
closed
6 months ago
1
Use subloclae instead of locale + for the spectroscopy game
#59
TheHllm
closed
10 months ago
2
Reduce resource usage of CI on PRs #44
#58
benkeks
closed
11 months ago
0
Stating Correctness Property - Theorem 1 of the Paper
#57
betawave
closed
11 months ago
0
Lifting Distinguishes Predicate to Sets of States
#56
betawave
closed
11 months ago
0
Lift `distinguishes` property to sets of states
#55
betawave
closed
11 months ago
0
53 documentation instantiation energy game
#54
Vervada
closed
10 months ago
1
Documentation of Instantiation Energy Game and Lemmas
#53
Vervada
closed
10 months ago
0
45 Check new definitions of finite play and energy level
#52
Vervada
closed
11 months ago
3
Bad Document Layout
#51
TheHllm
closed
11 months ago
5
Run workflow on pull_request
#50
TheHllm
closed
11 months ago
0
Change HML_SRBB Definition to exclude tau from Obs steps
#49
ekeln
closed
11 months ago
2
Flipping Order of Arguments |=
#48
betawave
closed
11 months ago
1
Revert Order of Arguments of |=
#47
betawave
closed
11 months ago
0
Fix: main CI fails
#46
TheHllm
closed
11 months ago
2
Check the new definitions with state and energy as input
#45
Vervada
closed
11 months ago
1
Investigate / Fix running CI/CD on PRs
#44
TheHllm
closed
11 months ago
8
Treat logical equivalences on HML_srbb
#43
benkeks
closed
10 months ago
10
Define strategy formulas on attacker-won region
#42
benkeks
closed
10 months ago
0
Define How Coordinates Define Equivalences
#41
betawave
closed
11 months ago
5
Define Expressiveness Price Function - Image Rework
#40
betawave
closed
11 months ago
0
Move files to import all theories in SilentStepSpectroscopy
#39
TheHllm
closed
11 months ago
1
Import HML files and Energy into SilentStepSpectroscopy.thy
#38
TheHllm
closed
11 months ago
2
32 sanity budgets (Upwardclosedness)
#37
Vervada
closed
11 months ago
1
9 define full spectroscopy game
#36
Vervada
closed
11 months ago
2
32-sanity-budgets-merge
#35
crmrtz
closed
11 months ago
0
23 set up continuous integration
#34
TheHllm
closed
11 months ago
0
19 formalize energy levels and updates
#33
TheHllm
closed
11 months ago
0
"Upwardclosedness" of winning budgets
#32
crmrtz
closed
11 months ago
0
Define Distinguishing Formulas and Induced Equivalences of HML Subsets
#31
betawave
closed
11 months ago
0
Define Expressiveness Price Function
#30
betawave
closed
11 months ago
0
Define HML Subset Expressing Stability Respecting Branching Bisimilarity (SRBB)
#29
betawave
closed
11 months ago
3
Define how coordinates define equivalences
#28
benkeks
closed
11 months ago
0
Express spectroscopy characterization theorem
#27
benkeks
closed
11 months ago
3
21 provide an instantiation energy game
#26
TheHllm
closed
11 months ago
0
Previous
Next