SymbolicModelCheckingforConverse Propositional Dynamic Logicbased Industry 4.0

Propositional Dynamic Logic with Converse (CPDL) is a modal logic developed for reasoning about programs with applications for instance in knowledge representation. This paper presents a symbol model checking algorithm for propositional dynamic logic with converse. First of all, according to the analysis of symbolic model checking technology by ordered binary decision diagram, we describe how to represent propositional dynamic logic with converse model system symbolically using ordered binary decision diagram. Then a symbolic model checking algorithm for propositional dynamic logic with converse is proposed. Finally, the proof of the algorithm is given, and the validity of this algorithm was verified by an example.