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

1Leelavathi Rajamanicham, Qin FenPing, Chen Jia

171 Views
61 Downloads
Abstract:

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.

Keywords:

propositional dynamic logic, satisfiability-checking, ordered binary decision diagram

Paper Details
Month3
Year2020
Volume24
IssueIssue 4
Pages8301-8312