کد مقاله کد نشریه سال انتشار مقاله انگلیسی نسخه تمام متن
11021128 1715034 2018 20 صفحه PDF دانلود رایگان
عنوان انگلیسی مقاله ISI
A delayed promotion policy for parity games
موضوعات مرتبط
مهندسی و علوم پایه مهندسی کامپیوتر نظریه محاسباتی و ریاضیات
پیش نمایش صفحه اول مقاله
A delayed promotion policy for parity games
چکیده انگلیسی
Parity games are two-player infinite-duration games on graphs that play a crucial role in various fields of theoretical computer science. Finding efficient algorithms to solve these games in practice is widely acknowledged as a core problem in formal verification, as it leads to efficient solutions of the model-checking and satisfiability problems of expressive temporal logics, e.g., the modal μCalculus. Their solution can be reduced to the problem of identifying sets of positions of the game, called dominions, in each of which a player can force a win by remaining in the set forever. Recently, a novel technique to compute dominions, called priority promotion, has been proposed, which is based on the notions of quasi dominion, a relaxed form of dominion, and dominion space. The underlying framework is general enough to accommodate different instantiations of the solution procedure, whose correctness is ensured by the nature of the space itself. In this paper we propose a new such instantiation, called delayed promotion, that tries to reduce the possible exponential behaviors exhibited by the original method in the worst case. The resulting procedure often outperforms both the state-of-the-art solvers and the original priority promotion approach.
ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Information and Computation - Volume 262, Part 2, October 2018, Pages 221-240
نویسندگان
, , ,