Propositional Dynamic Logic of Looping and Converse
Dynamic logic [5,6,15,16] applies concepts from modal logic to a relational semantics of programs to yield various systems for reasoning about the before-after behavior of programs. Analogues to the modal logic assertions ?p (possibly p) and ?p(necessarily p) are the dynamic logic constructs <a&g...
| Main Author: | |
|---|---|
| Published: |
2023
|
| Online Access: | https://hdl.handle.net/1721.1/149541 |
| _version_ | 1826214811442085888 |
|---|---|
| author | Streett, Robert S. |
| author_facet | Streett, Robert S. |
| author_sort | Streett, Robert S. |
| collection | MIT |
| description | Dynamic logic [5,6,15,16] applies concepts from modal logic to a relational semantics of programs to yield various systems for reasoning about the before-after behavior of programs. Analogues to the modal logic assertions ?p (possibly p) and ?p(necessarily p) are the dynamic logic constructs <a>p and [a]p. If a is a program and p is an assertion about the state of a computation, then ,<a>p asserts that after executing a, p can be the case, and [a]p asserts that after executing a, p must be the case. |
| first_indexed | 2024-09-23T16:11:32Z |
| id | mit-1721.1/149541 |
| institution | Massachusetts Institute of Technology |
| last_indexed | 2024-09-23T16:11:32Z |
| publishDate | 2023 |
| record_format | dspace |
| spelling | mit-1721.1/1495412023-03-30T03:06:52Z Propositional Dynamic Logic of Looping and Converse Streett, Robert S. Dynamic logic [5,6,15,16] applies concepts from modal logic to a relational semantics of programs to yield various systems for reasoning about the before-after behavior of programs. Analogues to the modal logic assertions ?p (possibly p) and ?p(necessarily p) are the dynamic logic constructs <a>p and [a]p. If a is a program and p is an assertion about the state of a computation, then ,<a>p asserts that after executing a, p can be the case, and [a]p asserts that after executing a, p must be the case. 2023-03-29T15:05:32Z 2023-03-29T15:05:32Z 1981-05 https://hdl.handle.net/1721.1/149541 8096978 MIT-LCS-TR-263 application/pdf |
| spellingShingle | Streett, Robert S. Propositional Dynamic Logic of Looping and Converse |
| title | Propositional Dynamic Logic of Looping and Converse |
| title_full | Propositional Dynamic Logic of Looping and Converse |
| title_fullStr | Propositional Dynamic Logic of Looping and Converse |
| title_full_unstemmed | Propositional Dynamic Logic of Looping and Converse |
| title_short | Propositional Dynamic Logic of Looping and Converse |
| title_sort | propositional dynamic logic of looping and converse |
| url | https://hdl.handle.net/1721.1/149541 |
| work_keys_str_mv | AT streettroberts propositionaldynamiclogicofloopingandconverse |