Formal Verification of Stochastic Max-Plus-Linear Systems

被引：12

作者：

Soudjani, Sadegh Esmaeil Zadeh ^{[1
]}

Adzkiya, Dieky ^{[2
]}

Abate, Alessandro ^{[1
]}

机构：

[1] Univ Oxford, Dept Comp Sci, Oxford OX1 2JD, England

[2] Inst Teknol Sepuluh Nopember, Dept Math, Surabaya 60111, Indonesia

来源：

IEEE TRANSACTIONS ON AUTOMATIC CONTROL | 2016年 / 61卷 / 10期

关键词：

Continuous-state processes; discrete-time stochastic processes; finite abstractions; linear-time logic; max-plus algebra; max-plus-linear (MPL) systems; probabilisticmodel checking; MODEL CHECKING; INTERVAL SYSTEMS; TIME; DOMAIN;

D O I：

10.1109/TAC.2015.2502781

中图分类号：

TP [自动化技术、计算机技术];

学科分类号：

0812 ;

摘要：

This work investigates the computation of finite abstractions of Stochastic Max-Plus-Linear (SMPL) systems and their formal verification against general bounded-time linear temporal specifications. SMPL systems are probabilistic extensions of discrete-event MPL systems, which are widely employed for modeling engineering systems dealing with practical timing and synchronization issues. Departing from the standard existing approaches for the analysis of SMPL systems, we newly propose to construct formal, finite abstractions of a given SMPL system: the SMPL system is first re-formulated as a discrete-time Markov process, then abstracted as a finite-stateMarkov Chain (MC). The derivation of precise guarantees on the level of the introduced formal approximation allows us to probabilistically model check the obtained MC against bounded-time linear temporal specifications (which are of rather general applicability), and to reliably export the obtained results over the original SMPL system. The approach is practically implemented on a dedicated software and is elucidated and run over numerical examples.

引用

页码：2861 / 2876

页数：16

共 50 条

[11]

Baier C, 2008, PRINCIPLES OF MODEL CHECKING, P1

[12]

Baier C, 1999, LECT NOTES COMPUT SC, V1664, P146

[13] Eigenvectors of interval matrices over max-plus algebra [J].

Cechlárová, K .

DISCRETE APPLIED MATHEMATICS, 2005, 150 (1-3) :2-15

[14] Interval systems of max-separable linear equations [J].

Cechlárová, K ;

Cuninghame-Green, RA .

LINEAR ALGEBRA AND ITS APPLICATIONS, 2002, 340 (1-3) :215-224

[15] Approximating Markov Processes by Averaging [J].

Chaput, Philippe ;

Danos, Vincent ;

Panangaden, Prakash ;

Plotkin, Gordon .

JOURNAL OF THE ACM, 2014, 61 (01)

[16] Bisimulation for labelled Markov processes [J].

Desharnais, J ;

Edalat, A ;

Panangaden, P .

INFORMATION AND COMPUTATION, 2002, 179 (02) :163-193

[17] Optimal Control of Markov Decision Processes With Linear Temporal Logic Constraints [J].

Ding, Xuchu ;

Smith, Stephen L. ;

Belta, Calin ;

Rus, Daniela .

IEEE TRANSACTIONS ON AUTOMATIC CONTROL, 2014, 59 (05) :1244-1257

[18]

Farahani S., 2010, P 10 INT WORKSH DISC, P386

[19]

Farahani S., 2013, DISCRETE EVENT DYN S, P1

[20]

Gaubert S., 2000, RR3971 INRIA

← 1 2 3 4 5 →