کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
10329454 | 685407 | 2005 | 17 صفحه PDF | دانلود رایگان |
عنوان انگلیسی مقاله ISI
Finding Symmetry in Models of Concurrent Systems by Static Channel Diagram Analysis
دانلود مقاله + سفارش ترجمه
دانلود مقاله ISI انگلیسی
رایگان برای ایرانیان
کلمات کلیدی
موضوعات مرتبط
مهندسی و علوم پایه
مهندسی کامپیوتر
نظریه محاسباتی و ریاضیات
پیش نمایش صفحه اول مقاله
چکیده انگلیسی
Over the last decade there has been much interest in exploiting symmetry to combat the state explosion problem in model checking. Although symmetry in a model often arises as a result of symmetry in the topology of the system being modelled, most model checkers which exploit structural symmetry are limited to topologies which exhibit total symmetries, such as stars and cliques. We define the static channel diagram of a concurrent, message passing program, and show that under certain restrictions there is a correspondence between symmetries of the static channel diagram of a program and symmetries of the Kripke structure associated with the program. This allows the detection, and potential exploitation, of structural symmetry in systems with arbitrary topologies. Our method of symmetry detection can handle mobile systems where channel references are passed on channels, resulting in a dynamic communication structure. We illustrate our results with an example using the Promela modelling language.
ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Electronic Notes in Theoretical Computer Science - Volume 128, Issue 6, 23 May 2005, Pages 161-177
Journal: Electronic Notes in Theoretical Computer Science - Volume 128, Issue 6, 23 May 2005, Pages 161-177
نویسندگان
Alastair F. Donaldson, Alice Miller, Muffy Calder,