@article{hatefi_improving_2015,
	title = {Improving time bounded reachability computations in interactive {Markov} chains},
	issn = {0167-6423},
	url = {http://www.sciencedirect.com/science/article/pii/S0167642315000994},
	doi = {10.1016/j.scico.2015.05.003},
	abstract = {Interactive Markov Chains (IMCs) are compositional behaviour models extending both Continuous Time Markov Chain (CTMC) and Labelled Transition System (LTS). They are used as semantic models in different engineering contexts ranging from ultramodern satellite designs to industrial system-on-chip manufacturing. Different approximation algorithms have been proposed for model checking of IMCs, with time bounded reachability probabilities playing a pivotal role. This paper addresses the accuracy and efficiency of approximating time bounded reachability probabilities in IMCs, improving over the state-of-the-art in both efficiency of computation and tightness of approximation. Moreover, a stable numerical approach, which provides an effective framework for implementation of the theory, is proposed. Experimental evidence demonstrates the efficiency of the new approach.},
	urldate = {2015-08-05},
	journal = {Science of Computer Programming},
	author = {Hatefi, Hassan and Hermanns, Holger},
	month = jun,
	year = {2015},
	keywords = {Discretisation, Interactive Markov chains, Root finding, Time bounded reachability},
}

{"_id":"H4GxnWMjE8v3jHNMG","bibbaseid":"hatefi-hermanns-improvingtimeboundedreachabilitycomputationsininteractivemarkovchains-2015","downloads":0,"creationDate":"2015-07-05T19:45:41.015Z","title":"Improving time bounded reachability computations in interactive Markov chains","author_short":["Hatefi, H.","Hermanns, H."],"year":2015,"bibtype":"article","biburl":"https://api.zotero.org/users/2539494/collections/QPKDCWZ2/items?key=GQZ7eSblSbBg8hlOjp5OpOAp&format=bibtex&limit=100","bibdata":{"bibtype":"article","type":"article","title":"Improving time bounded reachability computations in interactive Markov chains","issn":"0167-6423","url":"http://www.sciencedirect.com/science/article/pii/S0167642315000994","doi":"10.1016/j.scico.2015.05.003","abstract":"Interactive Markov Chains (IMCs) are compositional behaviour models extending both Continuous Time Markov Chain (CTMC) and Labelled Transition System (LTS). They are used as semantic models in different engineering contexts ranging from ultramodern satellite designs to industrial system-on-chip manufacturing. Different approximation algorithms have been proposed for model checking of IMCs, with time bounded reachability probabilities playing a pivotal role. This paper addresses the accuracy and efficiency of approximating time bounded reachability probabilities in IMCs, improving over the state-of-the-art in both efficiency of computation and tightness of approximation. Moreover, a stable numerical approach, which provides an effective framework for implementation of the theory, is proposed. Experimental evidence demonstrates the efficiency of the new approach.","urldate":"2015-08-05","journal":"Science of Computer Programming","author":[{"propositions":[],"lastnames":["Hatefi"],"firstnames":["Hassan"],"suffixes":[]},{"propositions":[],"lastnames":["Hermanns"],"firstnames":["Holger"],"suffixes":[]}],"month":"June","year":"2015","keywords":"Discretisation, Interactive Markov chains, Root finding, Time bounded reachability","bibtex":"@article{hatefi_improving_2015,\n\ttitle = {Improving time bounded reachability computations in interactive {Markov} chains},\n\tissn = {0167-6423},\n\turl = {http://www.sciencedirect.com/science/article/pii/S0167642315000994},\n\tdoi = {10.1016/j.scico.2015.05.003},\n\tabstract = {Interactive Markov Chains (IMCs) are compositional behaviour models extending both Continuous Time Markov Chain (CTMC) and Labelled Transition System (LTS). They are used as semantic models in different engineering contexts ranging from ultramodern satellite designs to industrial system-on-chip manufacturing. Different approximation algorithms have been proposed for model checking of IMCs, with time bounded reachability probabilities playing a pivotal role. This paper addresses the accuracy and efficiency of approximating time bounded reachability probabilities in IMCs, improving over the state-of-the-art in both efficiency of computation and tightness of approximation. Moreover, a stable numerical approach, which provides an effective framework for implementation of the theory, is proposed. Experimental evidence demonstrates the efficiency of the new approach.},\n\turldate = {2015-08-05},\n\tjournal = {Science of Computer Programming},\n\tauthor = {Hatefi, Hassan and Hermanns, Holger},\n\tmonth = jun,\n\tyear = {2015},\n\tkeywords = {Discretisation, Interactive Markov chains, Root finding, Time bounded reachability},\n}\n\n","author_short":["Hatefi, H.","Hermanns, H."],"key":"hatefi_improving_2015","id":"hatefi_improving_2015","bibbaseid":"hatefi-hermanns-improvingtimeboundedreachabilitycomputationsininteractivemarkovchains-2015","role":"author","urls":{"Paper":"http://www.sciencedirect.com/science/article/pii/S0167642315000994"},"keyword":["Discretisation","Interactive Markov chains","Root finding","Time bounded reachability"],"metadata":{"authorlinks":{}}},"search_terms":["improving","time","bounded","reachability","computations","interactive","markov","chains","hatefi","hermanns"],"keywords":["discretisation","interactive markov chains","root finding","time bounded reachability"],"authorIDs":[],"dataSources":["ypi2bjGvbv5c7j2pz"]}