Ordered Binary Decision Diagram-based Decision algorithm for Iteration-free CPDL

Propositional dynamic logic is one of the simplest applied modal logics designed for reasoning about the behavior of programs. Iteration-free converse propositional dynamic logic is an iteration-free fragment of propositional dynamic logic with converse of programs. Starting from a converse propositional dynamic logic formulas, the algorithm introduces the negative converse normal form transformation rule and the FLAT rule to do some preprocessing; then the model of set of formulas is reconstructed and transformed into some Boolean formulas; finally, these Boolean formulas are represented as ordered binary decision diagram, based on the existing ordered binary decision diagram software package that can be called for deciding the satisfiability of set of formulas. Proves that the algorithm is terminating, sound and complete, then realize the decision algorithm of iteration-free converse propositional dynamic logic.