On Explicit Solutions to Fixed-Point Equations in Propositional Dynamic Logic
Fuente:
arXiv
Salvato in:
| Autore principale: | |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2024
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866910728466726912 |
|---|---|
| author | Lyon, Tim S. |
| author_facet | Lyon, Tim S. |
| contents | Propositional dynamic logic (PDL) is an important modal logic used to specify and reason about the behavior of software. A challenging problem in the context of PDL is solving fixed-point equations, i.e., formulae of the form $x \equiv ϕ(x)$ such that $x$ is a propositional variable and $ϕ(x)$ is a formula containing $x$. A solution to such an equation is a formula $ψ$ that omits $x$ and satisfies $ψ\equiv ϕ(ψ)$, where $ϕ(ψ)$ is obtained by replacing all occurrences of $x$ with $ψ$ in $ϕ(x)$. In this paper, we identify a novel class of PDL formulae arranged in two dual hierarchies for which every fixed-point equation $x \equiv ϕ(x)$ has a solution. Moreover, we not only prove the existence of solutions for all such equations, but also provide an explicit solution $ψ$ for each fixed-point equation. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2412_04012 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | On Explicit Solutions to Fixed-Point Equations in Propositional Dynamic Logic Lyon, Tim S. Logic in Computer Science Logic Propositional dynamic logic (PDL) is an important modal logic used to specify and reason about the behavior of software. A challenging problem in the context of PDL is solving fixed-point equations, i.e., formulae of the form $x \equiv ϕ(x)$ such that $x$ is a propositional variable and $ϕ(x)$ is a formula containing $x$. A solution to such an equation is a formula $ψ$ that omits $x$ and satisfies $ψ\equiv ϕ(ψ)$, where $ϕ(ψ)$ is obtained by replacing all occurrences of $x$ with $ψ$ in $ϕ(x)$. In this paper, we identify a novel class of PDL formulae arranged in two dual hierarchies for which every fixed-point equation $x \equiv ϕ(x)$ has a solution. Moreover, we not only prove the existence of solutions for all such equations, but also provide an explicit solution $ψ$ for each fixed-point equation. |
| title | On Explicit Solutions to Fixed-Point Equations in Propositional Dynamic Logic |
| topic | Logic in Computer Science Logic |
| url | https://arxiv.org/abs/2412.04012 |