A CS3959 course project
echo ... > TS.txt # the transition system
echo ... > benchmark.txt # LTL formulas
python3 -m pip install antlr4-python3-runtime
python3 main.py
The project uses Antlr4 to parse the given LTL formula. It will transform the LTL formula into an
AST whose structured is defined in ltl_ast.py
. Then the AST will be simplified by the following
rules:
- Double negation is eliminated
a \/ b
->!(!a /\ !b)
a -> b
->!(a /\ !b)
[]a
->!<>!a
-> simplified using the next rule<>a
->True U a
The AST can be printed in a recursive manner. The printed string is regarded as the key when comparing two LTL nodes.
The negation of the parsed LTL node will be used in the remaining code as we need to find the violating circumstances of the given LTL formula.
In ltl2nba.py
, we will use the algorithm discribed in P278 of Principles of Model Checking to
convert the LTL node into a generalized NBA. Firstly the closure of the formula is found as:
-
(a, !a)
for every non-negative, non-constant subformula a of$\phi$ -
True
if it is a subformula of$\phi$ -
(a, !a)
for all literals in AP and not existing in$\phi$
Then we will find the element set. For (a, !a)
above, exactly one in a
and !a
can exist in one
consistant. If True exists in True
. Then all such sets
are checked if they sastify other consistancy rules.
Then we will construct the GNBA according the given algorithm.
The generalized NBA will be converted into NBA with the algorithm in P195. The algorithm is
implemented in nba.py
.
The cross product of transition system and NBA is implemented in verification.py
, which
is described in P200.
The persistence checking is implemented in verification.py
. This checking implements the algorithm
described in P211.