کد مقاله کد نشریه سال انتشار مقاله انگلیسی نسخه تمام متن
10329181 685328 2005 21 صفحه PDF دانلود رایگان
عنوان انگلیسی مقاله ISI
Spin-to-Grape: A Tool for Analysing Symmetry in Promela Models
موضوعات مرتبط
مهندسی و علوم پایه مهندسی کامپیوتر نظریه محاسباتی و ریاضیات
پیش نمایش صفحه اول مقاله
Spin-to-Grape: A Tool for Analysing Symmetry in Promela Models
چکیده انگلیسی
We provide two examples of Promela models of concurrent, distributed systems, whose associated Kripke structures have more complex symmetry groups than those of models commonly cited in the literature. We present a tool, Spin-to-Grape, which allows the state-graph of a Promela model to be manipulated using the group-theoretic package Gap and its graph-theoretic add on, Grape. Through studying these examples we show a correspondence between the symmetry group of the channel diagram of a system and the symmetry group of the Kripke structure associated with the system. We then identify some general classes of systems and describe the symmetry groups of the associated models. Finally we discuss ways in which symmetry reduction techniques incorporated within Spin, e.g. the SymmSpin package, could be extended to exploit symmetry in such models.
ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Electronic Notes in Theoretical Computer Science - Volume 139, Issue 1, 4 November 2005, Pages 3-23
نویسندگان
, , ,