Model checking is an automatic modelbased propertyverification approach to verification of computer systems by using transition systems and temporal logic. The system to verify has to be translated in a formal model called transition system. An example of a temporal logic is Computation Tree Logic, or CTL for short. The algorithm used to do CTL model checking here is the labeling algorithm. If you want to read more about CTL model checking, please consider the book Logic in Computer Science written by Michael Huth and Mark Ryan.
Throughout this page, the following syntax notation is used:

separates alternatives""
surround literals()
specifies grouping[az]
means one character in the interval from a to z (any lower case letter)[abc]
means one character of those between the brackets?
means 0 times or 1 time*
means 0 or more times\
escapes special characters in literalsCMCV visualizes the steps involved for CTL model checking for better understanding. It is divided into three panels:
id
or name
of the state, while the lower one is called the labels
of this state,
i.e. the atoms it is labeled with. With nodes you can do the following things.
id
of a selected node by clicking on it.
labels
of a selected node by clicking on them.
They are separated by comma and/or whitespaces.
system: "{" sysCore ("," sysNotes)? "}" sysCore: "\"states\"" ":" states "," "\"transitions\"" ":" transitions sysNotes: "\"notes\"" ":" string states: "[" stateList? "]" stateList: state ("," state)* state: "{" stateCore ("," statePos)? "}" stateCore: "\"id\"" ":" string "," "\"labels\"" ":" labels statePos: "\"x\"" ":" number "," "\"y\"" ":" number labels: "[" labelList? "]" labelList: string ("," string)* transitions: "[" transitionList? "]" transitionList: transition ("," transition)* transition: "[" string "," string "]"  "{" transitionCore ("," bend)? ("," loopDir)? "}" transitionCore: "\"source\"" ":" string "," "\"target\"" ":" string bend: "\"bend\"" ":" (string  boolean) loopDir: "\"loopDir\"" ":" stringHere
number
and string
can be any JSON number and string, respectively, except
that any string
must be nonempty. Additionally, tokens can be separated by arbitrary many whitespaces.
If a JSON representation of a transition system specifies keys other than those above, they are ignored.
Note that the statePos
rule for specifying x and ycoordinates is optional. If not all states
specify a position, the option "Layout Graph Automatically" is activated in order to determine positions for all nodes.
An edge representing a transition s → t without bend
is bent to the left if t → s also exists, and
goes straight otherwise. If bend
is "r"
" or "right"
(case insensitive),
the edge is bent to the right, while for any other truthy value the edge is bent to the left. Moreover, the
loopDir
option can be used for specifying the orientation of loops with the (case insensitive)
values "n"
or "north"
, "e"
or "east"
, "s"
or
"south"
and "w"
or "west"
.
If no loopDir
is specified, the loop points away from the center.
The sysNotes
rule is also optional. If you omit this rule, the notes are considered to be empty.
formula: disjunctive (">" formula)? disjunctive: conjunctive ("" disjunctive)? conjunctive: unary ("&" conjunctive)? unary: "B"  "T"  [az][az09_]*  "!" unary  "EX" unary  "AX" unary  "EF" unary  "AF" unary  "EG" unary  "AG" unary  "E[" formula "U" formula "]"  "A[" formula "U" formula "]"  "(" formula ")"So the binding is
>
< 
< &
< unary
. All
symbols can be separated by arbitrary many spaces.unary
, respectively, represent
⊥, ⊤ and an atom. The latter contains lower case letters, digits or underscores
and begins with a lower case letter.
Furthermore, you can check "use adequate set of connectives" to automatically translate your input formula in an equivalent formula using only the connectives ⊥, ¬, ∧, EX, AF and EU.
Press enter or click
to start the labeling algorithm with the current transition system and the formula you specified.To explain the current step, the following highlighting is used in the table:
current  The cell we think about whether to label or not. 
good  Votes for labeling the current cell, but loses in the end. 
bad  Votes for not labeling the current cell, but loses in the end. 
good critical  Votes for labeling the current cell and wins. 
bad critical  Votes for not labeling the current cell and wins. 
some/or  Some cell with a green border must be labeled in order to label the current cell. In other words, green wins here. 
every/and  Every cell with a red border must be labeled in order to label the current cell. In other words, red wins here. 
result  After executing the very last step, the states satisfying the given formula are highlighted this way. 
Similarly to the table, the algorithm is explained also in the graph with the following differences: