Session LinearTimeBranchingTimeSpectroscopyAccountingForSilentSteps
View
theory dependencies
View
document
View
outline
Theories
Misc
Energy_Games
HOL-Library.Old_Datatype
File ‹~~/src/HOL/Tools/Old_Datatype/old_datatype.ML›
HOL-Library.Nat_Bijection
HOL-Library.Countable
File ‹~~/src/HOL/Tools/BNF/bnf_lfp_countable.ML›
HOL-Library.Infinite_Set
HOL-Library.Countable_Set
HOL-Library.Countable_Complete_Lattices
HOL-Library.Order_Continuity
HOL-Library.Extended_Nat
HOL-Lattice.Orders
Energy
LTS
Spectroscopy_Game
LTS_Semantics
HML_SRBB
Expressiveness_Price
Strategy_Formulas
Distinction_Implies_Winning_Budgets
Silent_Step_Spectroscopy
Weak_Traces
Eta_Bisimilarity
Branching_Bisimilarity
Example_Instantiation