Precisely deciding CSL formulas through approximate model checking for CTMCs

Feng, Y; Zhang, L

Precisely deciding CSL formulas through approximate model checking for CTMCs

Feng, Y

Zhang, L

Permalink

Publication Type:: Journal Article
Citation:: Journal of Computer and System Sciences, 2017, 89 pp. 361 - 371
Issue Date:: 2017-11-01

Closed Access

	Filename	Description	Size
	1-s2.0-S0022000017300855-main.pdf	Published Version	401.81 kB	Adobe PDF	View/Open

Copyright Clearance Process

Recently Added
In Progress
Closed Access

This item is closed access and not available.

Full metadata record

Field	Value	Language
dc.contributor.author	Feng, Y https://orcid.org/0000-0002-3097-3896	en_US
dc.contributor.author	Zhang, L	en_US
dc.date.issued	2017-11-01	en_US
dc.identifier.citation	Journal of Computer and System Sciences, 2017, 89 pp. 361 - 371	en_US
dc.identifier.issn	0022-0000	en_US
dc.identifier.uri	http://hdl.handle.net/10453/125311
dc.description.abstract	© 2017 Elsevier Inc. The model checking problem of continuous-time Markov chains with respect to continuous-time stochastic logic was introduced and shown to be decidable by Aziz et al. [1,2 in 1996. Unfortunately, their proof is only constructive, but highly unpractical. Later in 2000, an efficient approximate algorithm was proposed by Baier et al. [3,5 for a sublogic with binary until. In this paper, we apply transcendental number theory and classical linear algebra to bridge the gap between the precise but unpractical algorithm, and the imprecise but efficient approximate algorithm. We prove that the approximate algorithm in [3,5 can be used as an off-the-shell tool for a precise model checking algorithm for binary until formulas. Further, we discuss extensions of our results to nested until and continuous-time Markov decision processes.	en_US
dc.relation	http://purl.org/au-research/grants/arc/DP160101652
dc.relation	http://purl.org/au-research/grants/arc/DP130102764
dc.relation.ispartof	Journal of Computer and System Sciences	en_US
dc.relation.isbasedon	10.1016/j.jcss.2017.05.014	en_US
dc.subject.classification	Computation Theory & Mathematics	en_US
dc.title	Precisely deciding CSL formulas through approximate model checking for CTMCs	en_US
dc.type	Journal Article
utslib.citation.volume	89	en_US
utslib.for	0802 Computation Theory and Mathematics	en_US
utslib.for	0805 Distributed Computing	en_US
utslib.for	0806 Information Systems	en_US
pubs.embargo.period	Not known	en_US
pubs.organisational-group	/University of Technology Sydney
pubs.organisational-group	/University of Technology Sydney/Faculty of Engineering and Information Technology
pubs.organisational-group	/University of Technology Sydney/Strength - QSI - Centre for Quantum Software and Information
utslib.copyright.status	closed_access
pubs.publication-status	Published	en_US
pubs.volume	89	en_US

Abstract:

© 2017 Elsevier Inc. The model checking problem of continuous-time Markov chains with respect to continuous-time stochastic logic was introduced and shown to be decidable by Aziz et al. [1,2 in 1996. Unfortunately, their proof is only constructive, but highly unpractical. Later in 2000, an efficient approximate algorithm was proposed by Baier et al. [3,5 for a sublogic with binary until. In this paper, we apply transcendental number theory and classical linear algebra to bridge the gap between the precise but unpractical algorithm, and the imprecise but efficient approximate algorithm. We prove that the approximate algorithm in [3,5 can be used as an off-the-shell tool for a precise model checking algorithm for binary until formulas. Further, we discuss extensions of our results to nested until and continuous-time Markov decision processes.

Please use this identifier to cite or link to this item:

http://hdl.handle.net/10453/125311