Undecidability of PDL with L = {a2i |; i ? 0} |
| |
| Authors: | D Harel MS Paterson |
| |
| Affiliation: | Department of Applied Mathematics, The Weizmann Institute of Science, Rehovot, Israel;Department of Computer Science, University of Warwick, Coventry, England |
| |
| Abstract: | 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. |
| |
| Keywords: | |
| 本文献已被 ScienceDirect 等数据库收录！ |
|
