On-the-fly verification and optimization of DTA-properties for large Markov chains. Mikeev, L., Neuhäußer, M., Spieler, D., & Wolf, V. Formal Methods in System Design, 2013. doi abstract bibtex We consider continuous-time Markov chains (CTMC) with very large or infinite state spaces which are, for instance, used to model biological processes or to evaluate the performance of computer and communication networks. We propose a numerical integration algorithm to approximate the probability that a process conforms to a specification that belongs to a subclass of deterministic timed automata (DTAs). We combat the state space explosion problem by using a dynamic state space that contains only the most relevant states. In this way we avoid an explicit construction of the state-transition graph of the composition of the DTA and the CTMC. We also show how to maximize the probability of acceptance of the DTA for parametric CTMCs and substantiate the usefulness of our approach with experimental results from biological case studies. © 2012 Springer Science+Business Media, LLC.
@article{
title = {On-the-fly verification and optimization of DTA-properties for large Markov chains},
type = {article},
year = {2013},
keywords = {[Continuous-time Markov chains, Deterministic time},
volume = {43},
id = {85c6c212-8683-3ff8-9a2e-0f1162032fde},
created = {2017-01-02T09:34:03.000Z},
file_attached = {false},
profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
last_modified = {2017-03-22T13:51:34.979Z},
read = {false},
starred = {false},
authored = {true},
confirmed = {false},
hidden = {false},
private_publication = {false},
abstract = {We consider continuous-time Markov chains (CTMC) with very large or infinite state spaces which are, for instance, used to model biological processes or to evaluate the performance of computer and communication networks. We propose a numerical integration algorithm to approximate the probability that a process conforms to a specification that belongs to a subclass of deterministic timed automata (DTAs). We combat the state space explosion problem by using a dynamic state space that contains only the most relevant states. In this way we avoid an explicit construction of the state-transition graph of the composition of the DTA and the CTMC. We also show how to maximize the probability of acceptance of the DTA for parametric CTMCs and substantiate the usefulness of our approach with experimental results from biological case studies. © 2012 Springer Science+Business Media, LLC.},
bibtype = {article},
author = {Mikeev, L. and Neuhäußer, M.R. and Spieler, D. and Wolf, V.},
doi = {10.1007/s10703-012-0165-1},
journal = {Formal Methods in System Design},
number = {2}
}
Downloads: 0
{"_id":"HKkpeRTYBLDeHG9Jc","bibbaseid":"mikeev-neuhuer-spieler-wolf-ontheflyverificationandoptimizationofdtapropertiesforlargemarkovchains-2013","downloads":0,"creationDate":"2017-01-02T15:13:03.897Z","title":"On-the-fly verification and optimization of DTA-properties for large Markov chains","author_short":["Mikeev, L.","Neuhäußer, M.","Spieler, D.","Wolf, V."],"year":2013,"bibtype":"article","biburl":"https://bibbase.org/service/mendeley/bbb99b2d-2278-3254-820f-2de6d915ce63","bibdata":{"title":"On-the-fly verification and optimization of DTA-properties for large Markov chains","type":"article","year":"2013","keywords":"[Continuous-time Markov chains, Deterministic time","volume":"43","id":"85c6c212-8683-3ff8-9a2e-0f1162032fde","created":"2017-01-02T09:34:03.000Z","file_attached":false,"profile_id":"bbb99b2d-2278-3254-820f-2de6d915ce63","last_modified":"2017-03-22T13:51:34.979Z","read":false,"starred":false,"authored":"true","confirmed":false,"hidden":false,"private_publication":false,"abstract":"We consider continuous-time Markov chains (CTMC) with very large or infinite state spaces which are, for instance, used to model biological processes or to evaluate the performance of computer and communication networks. We propose a numerical integration algorithm to approximate the probability that a process conforms to a specification that belongs to a subclass of deterministic timed automata (DTAs). We combat the state space explosion problem by using a dynamic state space that contains only the most relevant states. In this way we avoid an explicit construction of the state-transition graph of the composition of the DTA and the CTMC. We also show how to maximize the probability of acceptance of the DTA for parametric CTMCs and substantiate the usefulness of our approach with experimental results from biological case studies. © 2012 Springer Science+Business Media, LLC.","bibtype":"article","author":"Mikeev, L. and Neuhäußer, M.R. and Spieler, D. and Wolf, V.","doi":"10.1007/s10703-012-0165-1","journal":"Formal Methods in System Design","number":"2","bibtex":"@article{\n title = {On-the-fly verification and optimization of DTA-properties for large Markov chains},\n type = {article},\n year = {2013},\n keywords = {[Continuous-time Markov chains, Deterministic time},\n volume = {43},\n id = {85c6c212-8683-3ff8-9a2e-0f1162032fde},\n created = {2017-01-02T09:34:03.000Z},\n file_attached = {false},\n profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},\n last_modified = {2017-03-22T13:51:34.979Z},\n read = {false},\n starred = {false},\n authored = {true},\n confirmed = {false},\n hidden = {false},\n private_publication = {false},\n abstract = {We consider continuous-time Markov chains (CTMC) with very large or infinite state spaces which are, for instance, used to model biological processes or to evaluate the performance of computer and communication networks. We propose a numerical integration algorithm to approximate the probability that a process conforms to a specification that belongs to a subclass of deterministic timed automata (DTAs). We combat the state space explosion problem by using a dynamic state space that contains only the most relevant states. In this way we avoid an explicit construction of the state-transition graph of the composition of the DTA and the CTMC. We also show how to maximize the probability of acceptance of the DTA for parametric CTMCs and substantiate the usefulness of our approach with experimental results from biological case studies. © 2012 Springer Science+Business Media, LLC.},\n bibtype = {article},\n author = {Mikeev, L. and Neuhäußer, M.R. and Spieler, D. and Wolf, V.},\n doi = {10.1007/s10703-012-0165-1},\n journal = {Formal Methods in System Design},\n number = {2}\n}","author_short":["Mikeev, L.","Neuhäußer, M.","Spieler, D.","Wolf, V."],"biburl":"https://bibbase.org/service/mendeley/bbb99b2d-2278-3254-820f-2de6d915ce63","bibbaseid":"mikeev-neuhuer-spieler-wolf-ontheflyverificationandoptimizationofdtapropertiesforlargemarkovchains-2013","role":"author","urls":{},"keyword":["[Continuous-time Markov chains","Deterministic time"],"metadata":{"authorlinks":{"wolf, v":"https://bibbase.org/service/mendeley/bbb99b2d-2278-3254-820f-2de6d915ce63"}},"downloads":0},"search_terms":["fly","verification","optimization","dta","properties","large","markov","chains","mikeev","neuhäußer","spieler","wolf"],"keywords":["[continuous-time markov chains","deterministic time"],"authorIDs":["6TtMsgho6wSDppwNh"],"dataSources":["me3WD7pwWySxCKW8s","ya2CyA73rpZseyrZ8"]}