Graded Courrent PDL
Fuente:
arXiv
Saved in:
| Main Author: | |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866929678135066624 |
|---|---|
| author | Lin, Chun-Yu |
| author_facet | Lin, Chun-Yu |
| contents | 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 Ł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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2501_09285 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Graded Courrent PDL Lin, Chun-Yu Logic in Computer Science 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 Ł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. |
| title | Graded Courrent PDL |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2501.09285 |