文章基本信息

标题：Parity to Safety in Polynomial Time for Pushdown and Collapsible Pushdown Systems
本地全文：下载
作者：Matthew Hague ; Roland Meyer ; Sebastian Muskalla 等
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2018
卷号：117
页码：1-15
DOI：10.4230/LIPIcs.MFCS.2018.57
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：We give a direct polynomial-time reduction from parity games played over the configuration graphs of collapsible pushdown systems to safety games played over the same class of graphs. That a polynomial-time reduction would exist was known since both problems are complete for the same complexity class. Coming up with a direct reduction, however, has been an open problem. Our solution to the puzzle brings together a number of techniques for pushdown games and adds three new ones. This work contributes to a recent trend of liveness to safety reductions which allow the advanced state-of-the-art in safety checking to be used for more expressive specifications.
关键词：Parity Games; Safety Games; Pushdown Systems; Collapsible Pushdown Systems; Higher-Order Recursion Schemes; Model Checking