کد مقاله کد نشریه سال انتشار مقاله انگلیسی نسخه تمام متن
423278 685196 2006 16 صفحه PDF دانلود رایگان
عنوان انگلیسی مقاله ISI
How to Order Vertices for Distributed LTL Model-Checking Based on Accepting Predecessors
موضوعات مرتبط
مهندسی و علوم پایه مهندسی کامپیوتر نظریه محاسباتی و ریاضیات
پیش نمایش صفحه اول مقاله
How to Order Vertices for Distributed LTL Model-Checking Based on Accepting Predecessors
چکیده انگلیسی

Distributed automata-based LTL model-checking relies on algorithms for finding accepting cycles in a Büchi automaton. The approach to distributed accepting cycle detection as presented in [L. Brim, I. Černá, P. Moravec, J. Šimša. Accepting Predecessors are Better than Back Edges in Distributed LTL Model-Checking. In Formal Methods in Computer-Aided Design (FMCAD'04), volume 3312 of LNCS, pages 352–366. Springer, 2004] is based on maximal accepting predecessors. The ordering of accepting states (hence the maximality) is one of the main factors affecting the overall complexity of model-checking as an imperfect ordering can enforce numerous re-explorations of the automaton. This paper addresses the problem of finding an optimal ordering, proves its hardness, and gives several heuristics for finding an optimal ordering in the distributed environment. We compare the heuristics both theoretically and experimentally to find out which of these work well.

ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Electronic Notes in Theoretical Computer Science - Volume 135, Issue 2, 20 February 2006, Pages 3-18