TL;DR
This paper introduces a many-valued extension of concurrent propositional dynamic logic (CPDL) using a finite Łukasiewicz chain, providing completeness results and enhancing reasoning about programs under uncertainty.
Contribution
It extends CPDL to a many-valued setting with graded satisfiability, offering new completeness results for finitely-valued propositional dynamic logic.
Findings
Established completeness for all finitely-valued PDL.
Formalized reasoning about programs with uncertainty.
Enhanced expressiveness of dynamic logic with graded semantics.
Abstract
Propositional Dynamic Logic, PDL, is a modal logic designed to formalize the reasoning about programs. By extending accessibility between states to states and state sets, concurrent propositional dynamic logic CPDL, is introduced to include concurrent programs due to Peleg and Goldblatt. We study a many-valued generalization of CPDL where the satisfiability and the reachability relation between states and state sets are graded over a finite {\L}ukasiewicz chain. Finitely-valued dynamic logic has been shown to be useful in formalizing reasoning about program behaviors under uncertainty. We obtain completeness results for all finitely valued PDL.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsSemiconductor Lasers and Optical Devices