Inproceedings3404: Unterschied zwischen den Versionen
Aus International Center for Computational Logic
Keine Bearbeitungszusammenfassung Markierung: Manuelle Zurücksetzung |
Keine Bearbeitungszusammenfassung |
||
| Zeile 6: | Zeile 6: | ||
|Referiert=1 | |Referiert=1 | ||
|Title=On Explicit Solutions to Fixed-Point Equations in Propositional Dynamic Logic | |Title=On Explicit Solutions to Fixed-Point Equations in Propositional Dynamic Logic | ||
|To appear= | |To appear=0 | ||
|Year=2025 | |Year=2025 | ||
|Booktitle=Proceedings of the Eleventh International Conference on Fundamentals of Software Engineering (FSEN) | |Booktitle=Proceedings of the Eleventh International Conference on Fundamentals of Software Engineering (FSEN) | ||
|Pages=113-119 | |||
|Publisher=Springer | |Publisher=Springer | ||
|Editor=Hossein Hojjat, Georgiana Caltais | |||
|Series=LNCS | |Series=LNCS | ||
|Volume=15593 | |||
}} | }} | ||
{{Publikation Details | {{Publikation Details | ||
|Abstract=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 ≡ ϕ(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 ψ ≡ ϕ(ψ), 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 ≡ ϕ(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. | |Abstract=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 ≡ ϕ(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 ψ ≡ ϕ(ψ), 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 ≡ ϕ(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. | ||
|Link=https://arxiv.org/abs/2412.04012 | |Link=https://arxiv.org/abs/2412.04012 | ||
|DOI Name=https://doi.org/10.1007/978-3-031-87054-5_8 | |||
|Projekt=DeciGUT | |Projekt=DeciGUT | ||
|Forschungsgruppe=Computational Logic | |Forschungsgruppe=Computational Logic | ||
Aktuelle Version vom 26. März 2025, 20:41 Uhr
Tim Lyon
On Explicit Solutions to Fixed-Point Equations in Propositional Dynamic Logic
In Hossein Hojjat, Georgiana Caltais, eds., Proceedings of the Eleventh International Conference on Fundamentals of Software Engineering (FSEN), volume 15593 of LNCS, 113-119, 2025. Springer
On Explicit Solutions to Fixed-Point Equations in Propositional Dynamic Logic
In Hossein Hojjat, Georgiana Caltais, eds., Proceedings of the Eleventh International Conference on Fundamentals of Software Engineering (FSEN), volume 15593 of LNCS, 113-119, 2025. Springer
- KurzfassungAbstract
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 ≡ ϕ(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 ψ ≡ ϕ(ψ), 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 ≡ ϕ(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. - Weitere Informationen unter:Further Information: Link
- Projekt:Project: DeciGUT
- Forschungsgruppe:Research Group: Computational LogicComputational Logic
@inproceedings{L2025,
author = {Tim Lyon},
title = {On Explicit Solutions to Fixed-Point Equations in Propositional
Dynamic Logic},
editor = {Hossein Hojjat and Georgiana Caltais},
booktitle = {Proceedings of the Eleventh International Conference on
Fundamentals of Software Engineering (FSEN)},
series = {LNCS},
volume = {15593},
publisher = {Springer},
year = {2025},
pages = {113-119},
doi = {https://doi.org/10.1007/978-3-031-87054-5_8}
}
