SymbolicModelCheckingforConverse Propositional Dynamic Logicbased Industry 4.0

1Leelavathi Rajamanicham, Qin FenPing, Chen Jia

147 Views
45 Downloads
Abstract:

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.

Keywords:

model checking, Converse propositional dynamic logic(CPDL), Ordered Binary Decision Diagram (OBDD)

Paper Details
Month6
Year2020
Volume24
IssueIssue 6
Pages18851-18862