Undecidability of PDL with L = {a2i |; i ⩾ 0}
作者：
Highlights：
•
摘要
It is shown that the validity problem for propositional dynamic logic (PDL), which is decidable and actually DEXPTIME-complete for the usual class of regular programs, becomes highly undecidable, viz. Π11-complete, when the single nonregular one-letter program L = {a2i |; i ⩾ 0} is added. This answers a question of Harel, Pnueli, and Stavi.
论文关键词：
论文评审过程：Received 30 January 1984, Revised 15 June 1984, Available online 2 December 2003.
论文官网地址：https://doi.org/10.1016/0022-0000(84)90005-9
