一句话：证明满足二重迭代分配律的森林代数所识别语言均属于 PDL，并给出该子类的可判定性。
论文研究森林上命题动态逻辑（PDL）可定义性是否可判定这一开放问题。基于 Bojańczyk 等人用森林代数给出的代数刻画，Straubing 提出用 k 重迭代分配律逼近 PDL：若能证明所有满足该律的语言都在 PDL 中，则可判定 PDL。本文解决 k=2 的情形，证明由满足二重迭代分配律的森林代数识别的语言都属于 PDL，并进一步证明该语言类是可判定的。这给出了 PDL 的一个新的非平凡可判定子类，也表明上述基于迭代分配律的总体路线是可行的。
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.