Abstract:
It is an open problem whether definability in Propositional Dynamic Logic (PDL) on forests is decidable. Based on an algebraic characterization by Bojańczyk, et. al.,(2012) in terms of forest algebras, Straubing (2013) described an approach to PDL based on a k-fold iterated distributive law. A proof that all languages satisfying such a k-fold iterated distributive law are in PDL would settle decidability of PDL. We solve this problem in the case k=2: All languages recognized by forest algebras satisfying a 2-fold iterated distributive law are in PDL. Furthermore, we show that this class is decidable. This provides a novel nontrivial decidable subclass of PDL, and demonstrates the viability of the proposed approach to deciding PDL in general.
Reference:
Wreath Products of Distributive Forest AlgebrasMichael Hahn, Andreas Krebs, Howard StraubingLogic in Computer Science (LICS), 2018.
Bibtex Entry:
@INPROCEEDINGS{Hahn-Krebs-Straubing-2018,
author = {Michael Hahn and Andreas Krebs and Howard Straubing},
title = {Wreath Products of Distributive Forest Algebras},
booktitle = {Logic in Computer Science (LICS)},
png = {figs/lics.png},
year = {2018},
URL = {files/lics-2018-submitted.pdf},
github = {https://github.com/m-hahn/lics2018-wreath-products},
preprint = {https://arxiv.org/abs/1911.03493},
slides = {https://www.mhahn.info/files/lics2018.pdf},
abstract = {It is an open problem whether definability in Propositional Dynamic Logic (PDL) on forests is decidable. Based on an algebraic characterization by Bojańczyk, et. al.,(2012) in terms of forest algebras, Straubing (2013) described an approach to PDL based on a k-fold iterated distributive law. A proof that all languages satisfying such a k-fold iterated distributive law are in PDL would settle decidability of PDL. We solve this problem in the case k=2: All languages recognized by forest algebras satisfying a 2-fold iterated distributive law are in PDL. Furthermore, we show that this class is decidable. This provides a novel nontrivial decidable subclass of PDL, and demonstrates the viability of the proposed approach to deciding PDL in general.}
}