Published January 1, 2018
| Version v1
Publication
Open
A Hierarchy of Scheduler Classes for Stochastic Automata
- 1. Universidad Nacional de Córdoba
- 2. University of Twente
- 3. University of Waterloo
Description
Stochastic automata are a formal compositional model for concurrent stochastic timed systems, with general distributions and nondeterministic choices. Measures of interest are defined over schedulers that resolve the nondeterminism. In this paper we investigate the power of various theoretically and practically motivated classes of schedulers, considering the classic complete-information view and a restriction to non-prophetic schedulers. We prove a hierarchy of scheduler classes w.r.t. unbounded probabilistic reachability. We find that, unlike Markovian formalisms, stochastic automata distinguish most classes even in this basic setting. Verification and strategy synthesis methods thus face a tradeoff between powerful and efficient classes. Using lightweight scheduler sampling, we explore this tradeoff and demonstrate the concept of a useful approximative verification technique for stochastic automata.
Translated Descriptions
⚠️
This is an automatic machine translation with an accuracy of 90-95%
Translated Description (Arabic)
الأتمتة العشوائية هي نموذج تركيبي رسمي للأنظمة العشوائية المتزامنة، مع توزيعات عامة وخيارات غير حتمية. يتم تحديد مقاييس الاهتمام على الجدولة التي تحل عدم الحتمية. في هذه الورقة، نقوم بالتحقيق في قوة مختلف فئات المجدولين ذات الدوافع النظرية والعملية، مع الأخذ في الاعتبار عرض المعلومات الكاملة الكلاسيكي والقيود المفروضة على المجدولين غير البيولوجيين. نثبت التسلسل الهرمي لفئات الجدولة مع إمكانية الوصول الاحتمالي غير المحدود. نجد أنه، على عكس الشكليات الماركوفية، تميز الأوتوماتيكية العشوائية معظم الفئات حتى في هذا الإعداد الأساسي. وبالتالي تواجه طرق التحقق وتوليف الاستراتيجية مفاضلة بين الطبقات القوية والفعالة. باستخدام عينات جدولة خفيفة الوزن، نستكشف هذه المقايضة ونوضح مفهوم تقنية التحقق التقريبي المفيدة للأتمتة العشوائية.Translated Description (French)
Les automates stochastiques sont un modèle de composition formel pour les systèmes temporels stochastiques concurrents, avec des distributions générales et des choix non déterministes. Les mesures d'intérêt sont définies sur les ordonnanceurs qui résolvent le non-déterminisme. Dans cet article, nous étudions la puissance de diverses classes d'ordonnanceurs motivées théoriquement et pratiquement, en tenant compte de la vue classique de l'information complète et d'une restriction aux ordonnanceurs non prophétiques. Nous prouvons une hiérarchie de classes d'ordonnanceur w.r.t. atteignabilité probabiliste non bornée. Nous constatons que, contrairement aux formalismes markoviens, les automates stochastiques distinguent la plupart des classes même dans ce cadre de base. Les méthodes de vérification et de synthèse de stratégie sont donc confrontées à un compromis entre les classes puissantes et efficaces. À l'aide d'un échantillonnage de programmateur léger, nous explorons ce compromis et démontrons le concept d'une technique de vérification approximative utile pour les automates stochastiques.Translated Description (Spanish)
Los autómatas estocásticos son un modelo de composición formal para sistemas cronometrados estocásticos concurrentes, con distribuciones generales y elecciones no deterministas. Las medidas de interés se definen sobre los programadores que resuelven el no determinismo. En este artículo investigamos el poder de varias clases de programadores motivados teórica y prácticamente, considerando la visión clásica de información completa y una restricción a los programadores no proféticos. Demostramos una jerarquía de clases de programador con accesibilidad probabilística ilimitada. Encontramos que, a diferencia de los formalismos de Markov, los autómatas estocásticos distinguen a la mayoría de las clases incluso en este entorno básico. Por lo tanto, los métodos de verificación y síntesis de estrategias se enfrentan a una compensación entre clases poderosas y eficientes. Utilizando un muestreo de planificador ligero, exploramos esta compensación y demostramos el concepto de una técnica de verificación aproximativa útil para los autómatas estocásticos.Files
10.1007%2F978-3-319-89366-2_21.pdf.pdf
Files
(1.3 MB)
| Name | Size | Download all |
|---|---|---|
|
md5:6bfc2f7c769cf4ae4356dd27b1674c8d
|
1.3 MB | Preview Download |
Additional details
Additional titles
- Translated title (Arabic)
- تسلسل هرمي لفئات الجدولة لـ Stochastic Automata
- Translated title (French)
- Une hiérarchie de classes de planificateur pour les automates stochastiques
- Translated title (Spanish)
- Una jerarquía de clases de programador para autómatas estocásticos
Identifiers
- Other
- https://openalex.org/W2767054264
- DOI
- 10.1007/978-3-319-89366-2_21
References
- https://openalex.org/W106209860
- https://openalex.org/W113236070
- https://openalex.org/W1498432697
- https://openalex.org/W1499021164
- https://openalex.org/W1556729131
- https://openalex.org/W1589318611
- https://openalex.org/W1597655219
- https://openalex.org/W1629580170
- https://openalex.org/W1851152565
- https://openalex.org/W1983635508
- https://openalex.org/W2011177514
- https://openalex.org/W2014582618
- https://openalex.org/W2028079360
- https://openalex.org/W2073841996
- https://openalex.org/W2092865915
- https://openalex.org/W2102609194
- https://openalex.org/W2118912801
- https://openalex.org/W2119027795
- https://openalex.org/W2154144595
- https://openalex.org/W2163234015
- https://openalex.org/W2164880134
- https://openalex.org/W2169764001
- https://openalex.org/W2200793582
- https://openalex.org/W2262106677
- https://openalex.org/W2294463118
- https://openalex.org/W2401679532
- https://openalex.org/W2482035342
- https://openalex.org/W2492599963
- https://openalex.org/W2511317331
- https://openalex.org/W2555199731
- https://openalex.org/W275084143
- https://openalex.org/W4237257906
- https://openalex.org/W4241531936