کد مقاله کد نشریه سال انتشار مقاله انگلیسی نسخه تمام متن
433207 1441644 2015 28 صفحه PDF دانلود رایگان
عنوان انگلیسی مقاله ISI
On-the-fly PCTL fast mean-field approximated model-checking for self-organising coordination
موضوعات مرتبط
مهندسی و علوم پایه مهندسی کامپیوتر نظریه محاسباتی و ریاضیات
پیش نمایش صفحه اول مقاله
On-the-fly PCTL fast mean-field approximated model-checking for self-organising coordination
چکیده انگلیسی


• We show a new procedure combining on-the-fly model-checking and mean-field.
• We prove the asymptotic correctness of the on-the-fly model-checking procedure.
• We present a prototype implementation of the model-checking.
• We use the technique to analyze selection of simple and more elaborate scenarios.

Typical self-organising collective systems consist of a large number of interacting objects that coordinate their activities in a decentralised and often implicit way. Design of such systems is challenging and requires suitable, scalable analysis tools to check properties of proposed system designs before they are put into operation. We present a novel scalable, on-the-fly approximated model-checking procedure to verify bounded PCTL properties of selected individuals in the context of very large systems of independent interacting objects. The proposed procedure combines on-the-fly model-checking techniques with deterministic mean-field approximation in discrete time. The asymptotic correctness of the procedure is proven and a prototype implementation of the model-checker is presented. The potential of the verification approach is illustrated by its application on self-organising collective systems and an overview of remaining open issues and future extensions is provided.

ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Science of Computer Programming - Volume 110, 15 October 2015, Pages 23–50
نویسندگان
, , ,