Ordered Binary Decision Diagram-based Decision algorithm for Iteration-free CPDL
DOI:
https://doi.org/10.61841/wr8cww12Keywords:
propositional dynamic logic;, satisfiability-checking, ordered binary decision diagramAbstract
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.
Downloads
References
[1] FISCHER M, LADNER R. (1979). Propositional dynamic logic of regular programs. Computer System Science, 18(2):194-211.
[2] BAADER F, SATTLER U. (2001). An overview of tableau algorithms for description logic .Studia Logical,
3(69):5-40.
[3] BRYANT RE. (1986). Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers, 35(8):677-691.
[4] PAN GQ, SATTLER U, VARDI MY. (2006). BDD-based decision procedures for the modal logic K.Journal of Applied Non-Classical Logics, 16(1-2):169-208.
[5] SCHILD K. (1991).A correspondence theory for terminological logics: Preliminary report. Proceedings of the 12th on Artificial Intelligence, 466-471.
[6] RUDOLPH S, KROTZSCH M, HITZLER P. (2008).Description Logic Reasoning with Decision Diagrams-Compiling SHIQ to Disjunctive Datalog.Proc of the 7th International Semantic Web Conference,435-450.
[7] PHILIPE BALBIANI, DIMITER VIKARELOV. (2001). Iteration-free PDL with Intersection: a Complete Axiomatization.Fundamental Informaticae, 4(5):173-194.
[8] DRECHSLER .R, SIELING.D. Special Section on BDD: Binary Decision Diagrams in Theory and Practice [J].
International Journal on Software Tools for Technology Transfer, 2001, 2(3):112-136.
[9] GU TIANLONG,XUZHOUBO, (2015).Ordered binary decision diagram and application.Science Press,35-60
[10] Christian Doczkal, Joachim Bard (2018) Completeness and Decidability of Converse PDL in the Constructive Type Theory of Coq
Downloads
Published
Issue
Section
License
This work is licensed under a Creative Commons Attribution 4.0 International License.
You are free to:
- Share — copy and redistribute the material in any medium or format for any purpose, even commercially.
- Adapt — remix, transform, and build upon the material for any purpose, even commercially.
- The licensor cannot revoke these freedoms as long as you follow the license terms.
Under the following terms:
- Attribution — You must give appropriate credit , provide a link to the license, and indicate if changes were made . You may do so in any reasonable manner, but not in any way that suggests the licensor endorses you or your use.
- No additional restrictions — You may not apply legal terms or technological measures that legally restrict others from doing anything the license permits.
Notices:
You do not have to comply with the license for elements of the material in the public domain or where your use is permitted by an applicable exception or limitation .
No warranties are given. The license may not give you all of the permissions necessary for your intended use. For example, other rights such as publicity, privacy, or moral rights may limit how you use the material.
