Computation Tree Logic (CTL)

A Matlab package for verifying CTL properties

Description

Computation tree logic (CTL) is a temporal logic used in formal verification of state machines. This package implements the basic CTL model checking algorithm using labels. The content of this package is taken from the package CheckMate and restructured to use independently.

For introduction and a simple demo, please go to ./html/ directory.

• MATLAB release: MATLAB 7.4 (R2007a)
• Other requirements: AT&T graphviz is supported for visualizing the transition system.
• Published M Files: DEMOCTL1.m

Other Files

witness/ce.m,
witness/witAF.m,
witness/witAR.m,
witness/witAX.m,
witness/witgraph.m,
witness/witAG.m,
witness/witAU.m,
Contents.m,
demo1.gif,
demo1.jpg,
demo1.png,
demo1.svg,
demoCTL1.m,
eval_strong_negate.m,
evaluate.m,
install_ctl.m,
model_check.m,
revtran.m,
@region/and.m,
@region/checkAF.m,
@region/checkAG.m,
@region/checkAR.m,
@region/checkAU.m,
@region/checkAX.m,
@region/checkEF.m,
@region/checkEG.m,
@region/checkER.m,
@region/checkEU.m,
@region/checkEX.m,
@region/display.m,
@region/findSCCf.m,
@region/get_region_param.m,
@region/isempty.m,
@region/isinregion.m,
@region/isuniverse.m,
@region/not.m,
@region/or.m,
@region/reach.m,
@region/region.m,
@region/set_state.m,
@region/get_state.m,
@region/get_transitions.m,
graph/movingrectangle.m,
graph/plot_tran.m,
graph/write_dot.m,
parser/parse.m,
html/demoCTL1_01.png,
html/demo1.jpg,
html/demoCTL1_02.png,
html/demoCTL1.png,
parser/visit.m,
parser/apply_production.m,
parser/compile_ap.m,
parser/create_production.m,
parser/find_key_symbol.m,
parser/identerm.m,
parser/match_paren.m,
parser/match_production.m,
graph/dotdraw.m