Diffusion afp-devel a2c03373dc20

Implement equivalence relation with unfolding for LTL Master Theorem
a2c03373dc20
Actions

Tags

None

Subscribers

None

Description

Implement equivalence relation with unfolding for LTL Master Theorem

Details

Provenance

Benedikt Seidl <benedikt.seidl@tum.de>

Authored on

Parents

rAFPdb7040379c22: Proof of Restricted Master Theorem on LTL

Branches

Unknown

Tags

Unknown

Event Timeline

Changes (11)

Path

Size

LTL_Master_Theorem

Code_Export.thy

LTL_to_DRA/

DRA_Construction.thy

DRA_Implementation.thy

DRA_Instantiation.thy

Transition_Functions.thy

Logical_Characterization

Extra_Equivalence_Relations.thy

code/

ltl_to_dra_cli.sml

rAFPa2c03373dc20

thys/LTL_Master_Theorem/Code_Export.thy

Loading...

thys/LTL_Master_Theorem/LTL_to_DRA/DRA_Construction.thy

Loading...

thys/LTL_Master_Theorem/LTL_to_DRA/DRA_Implementation.thy

Loading...

thys/LTL_Master_Theorem/LTL_to_DRA/DRA_Instantiation.thy

Loading...

thys/LTL_Master_Theorem/LTL_to_DRA/Transition_Functions.thy

Loading...

thys/LTL_Master_Theorem/Logical_Characterization/Advice.thy

Loading...

thys/LTL_Master_Theorem/Logical_Characterization/Extra_Equivalence_Relations.thy

Loading...

thys/LTL_Master_Theorem/code/ltl_to_dra_cli.sml

Loading...