At first , temporal logic based on Manna Pnueli framework and concurrent program(transition diagrams) model based on shared variable are introduced, and mapping the model into basic transition systems; second,describing concurrent program and their properties(fairness, safety, liveness) by combing temporal logic with FTS model; at last,we point out temporal logic are more suitable than FSM and Petri net for specifies concurrent program.
