Documentation

This is the documentation for the LTL model checking project of CS3959. The project implements a python program that checks whether a given transition system satisfies a given LTL formula. The project uses the ply package to parse the LTL formula. The GNBA construction, transformation from GNBA to NBA, product construction, and the nested DFS algorithm are implemented according to the textbook, "Principles of Model Checking" by Christel Baier and Joost-Pieter Katoen. The project is implemented by Youwei Zhong, with help from the textbook, the course notes, Github Copilot and GPT-4o.

Usage

Package dependency:

pip install ply

Input format:

See Input_Format.pdf.

See how to run the program:

python main.py -h

Run the program to output the result as in Canvas:

python main.py ts_file ltl_file

Run the program to output the result in detail, including parsing results, the GNBA, the NBA, the product construction, and the countercase:

python main.py ts_file ltl_file -d

Output the result to a file:

python main.py ts_file ltl_file -f output_file

or

python main.py ts_file ltl_file -f output_file -d

Help

python main.py -h

The output is as follows:

usage: main.py [-h] [-d] [-f OUTPUT_FILE] ts_file ltl_file

LTL Model Checking

positional arguments:
  ts_file         File containing the transition system
  ltl_file        File containing the LTL formulas

options:
  -h, --help      show this help message and exit
  -d
  -f OUTPUT_FILE

Example

(.venv) zhongyouwei@LAPTOP-7IF0SBG4:~/ltl$ python main.py TS.txt sample.txt
Generating LALR tables
WARNING: 32 shift/reduce conflicts
1
1
0
0

Generating LALR tables and WARNING: 32 shift/reduce conflicts will disappear after executing the program for the first time.

We can ignore the shift/reduce conflicts since we require that all input formulas to include enough parentheses to avoid ambiguity.

(.venv) zhongyouwei@LAPTOP-7IF0SBG4:~/ltl$ python main.py TS.txt sample.txt -d -f sample_output.txt

sample_output.txt includes an example of the detailed intermediate outputs and the countercase.

Construction details

The file main.py is the main program, which imports classes and functions defined in other .py files.

Transition System

The transition system is defined as a class in ts.py. The parse_transition_system() function in ts.py parses the transition system from a file.

LTL Formula

The file ltl_parser.py contains the code of a lexer and a parser for parsing LTL formulas. The parser used in main.py is the parser that parses an LTL formula into a tuple.

For example, the formula G(a \/ b) is parsed into ('always', ('or', ('atom', 'a'), ('atom', 'b'))).

parser.out and parsetab.py are two autogenerated files for the parser, which will be generated after the first execution.

Construction of the GNBA

After parsing the original formula, the function construct_gnba_from_ltl_formula() defined in gnba_cons.py construct a GNBA based on the parsed formula. It should be noting that the input of this function should be the negation of the original formula.

The function construct_gnba_from_ltl_formula() includes several steps, which will be introduced one by one in the following subsections.

Transform the original LTL formula

To get the formula for construction of a GNBA, we need to transform the formula into a form that only contains 'and', 'not', 'next', and 'until' operators. Then, we need to eliminate double negation in the formula. Finally, we eliminate the redundant subformula in the same 'and' operator.

new_formula = eliminate_same_and(eliminate_double_not(transform(ltl_formula)))

The implementation of these three functions is in translate_formula.py.

Calculate the closure of the formula

The function calculate_closure() in gnba_cons.py calculates the closure of the formula, which includes the formula and all its subformulas. Note that the closure is split into two halves: half_closure_first and half_closure_second, either includes a formula or its negation. In this way, we can construct the elemantary sets more easily in the following steps.

half_closure_first, half_closure_second = calculate_closure(new_formula)

Calculate the elementary sets

The function calculate_elementary_sets() calculates all elementary sets of the closure. The implementation is in calculate_elementary_sets.py.

Construct the GNBA

The function construct_gnba() constructions the GNBA that recognizes the transformed LTL formula. The implementation is in gnba_cons.py.

Transformation from the GNBA to an NBA

The function gnba_to_nba() in gnba_detect.py does this. This function also remedy the output NBA that is not nonblocking to an equivalent nonblocking one by adding a trap state ('trap', 0).

Product construction

The function product_construction() in gnba_detect.py does this. Note that the function only keeps the propositions that are used in the NBA in the transition system, and the initial states of the input transition system are modified to include only the initial state appointed by the LTL formula if it is a state formula.

Nest DFS algorithm

The function nested_dfs() in gnba_detect.py implements Algorithm 8 Persistence checking by nested depth-first search in the textbook.

The function uses reachable_cycle() to check a reachable cycle from the initial states. The function first does the outer DFS. U records the current path of the outer DFS. If the newly visited state refers to an acception conditions of the NBA. The function calls cycle_check() to do the inner DFS to check if there is a cycle that contain infinite states of the acception conditions. V records the current path of the inner DFS. If there is a cycle, then U + V represents a countercase of the original LTL formula.