Model checking interactive Markov chains against asCSL specifications

被引：0

作者：

Niu, Jun ^{[1
,2
]}

Zeng, Guosun ^{[2
]}

Zhan, Weihua ^{[1
]}

机构：

[1] Faculty of Information Science and Engineering, Ningbo University

[2] Department of Computer Science and Technology, Tongji University

来源：

Journal of Computational Information Systems | 2014年 / 10卷 / 03期

关键词：

Automaton; Interactive Markov chain; Model checking; Reachability analysis; Temporal logic;

D O I：

10.12733/jcis9616

中图分类号：

学科分类号：

摘要：

In this paper, the model checking procedure for IMCs (Interactive Markov Chains) against Continuous Stochastic Logic with actions and state labels (asCSL) specifications is addressed. The path properties of asCSL formulae are characterized by regular expressions over actions and state labels. We propose an embedded labelled transition system (LTS) of an IMC, in which all Markovian transitions are replaced with interactive ones which labelled with a new action label ○. For all pairs of state and action appeared in the regular expression component, we modify them by adding expression (true, ○)* for indicating possible Markovian transitions. We then investigate the model checking procedure by combining the resulting embedded LTS and extended regular expressions into a product IMC. The usefulness of our approach is illustrated with some examples. © 2014 Binary Information Press.

引用

页码：1211 / 1218

页数：7

共 14 条

[1]

Hermanns H., Herzog U., Katoen J.P., Process algebra for performance evaluation, Theoretical Computer Science, 274, 1, pp. 43-87, (2002)

[2]

Hermanns H., Interactive Markov chains, (1998)

[3]

Hermanns H., Interactive Markov chains: The quest for quantified quality, LNCS, 2428, (2002)

[4]

Guck D., Han T., Katoen J.P., Neuhauber M.R., Quantitative timed analysis of interactive Markov chains, NASA Formal Methods Symposium (NFM). LNCS, 7226, pp. 8-23, (2012)

[5]

Bravetti M., Revisiting interactive Markov chains, Electronic Notes in Theoretical Computer Science, 68, 5, pp. 65-84, (2003)

[6]

Kwiatkowska M., Norman G., Parker D., Stochastic model checking, Formal Methods for the Design of Computer, Communication and Software Systems: Performance Evaluation (SFM'07), volume 4486 of LNCS, pp. 220-270, (2007)

[7]

Wolovick N., Johr S., A characterization of meaningful schedulers for continuous-time Markov decision processes, FORMATS. Volume 4202 of LNCS, pp. 352-367, (2006)

[8]

Neuhauber M.R., Model checking nondeterministic and randomly timed systems, (2010)

[9]

Baier C., Cloth L., Haverkort B., Kuntz M., Siegle M., Model checking Markov chains with actions and state labels, IEEE Transactions on Software Engineering, 33, 4, pp. 209-224, (2007)

[10]

Cloth L., Haverkort B., Hermanns H., Katoen J.-P., Baier C., Model Checking pathCSL, Proceedings of PMCCS-6, pp. 19-22, (2003)

← 1 2 →