{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,19]],"date-time":"2025-03-19T12:29:13Z","timestamp":1742387353067},"reference-count":28,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1109\/dsn.2004.1311941","type":"proceedings-article","created":{"date-parts":[[2004,11,13]],"date-time":"2004-11-13T00:14:14Z","timestamp":1100304854000},"page":"701-710","source":"Crossref","is-referenced-by-count":14,"title":["Model checking action- and state-labelled Markov chains"],"prefix":"10.1109","author":[{"given":"C.","family":"Baier","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"L.","family":"Cloth","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"B.","family":"Haverkort","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"M.","family":"Kuntz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"M.","family":"Siegle","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref10","first-page":"58","article-title":"A stochastic extension of the logic PDL","author":"kuntz","year":"2003","journal-title":"Proc 6th Int'l Workshop on Performability Modeling of Computer and Communication Systems"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1016\/S0166-5316(99)00010-3"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(79)90046-1"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1145\/582153.582156"},{"key":"ref14","first-page":"155","article-title":"It usually works: The temporal logic of stochastic systems","author":"aziz","year":"1995","journal-title":"CAV'95 LNCS 939"},{"journal-title":"Introduction to the Numerical Solution of Markov Chains","year":"1994","author":"stewart","key":"ref15"},{"key":"ref16","first-page":"358","article-title":"Model checking continuous-time Markov chains by transient analysis","author":"baier","year":"2000","journal-title":"CAV'00 LNCS 1855"},{"journal-title":"Finite Markov Chains","year":"1976","author":"kemeny","key":"ref17"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.2307\/3215235"},{"article-title":"A Compositional Approach to Performance Modelling","year":"1994","author":"hillston","key":"ref19"},{"key":"ref28","first-page":"12","article-title":"On the efficient sequential and distributed evaluation of very large stochastic Petri nets","author":"haverkort","year":"1999","journal-title":"PNPM 99"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211866"},{"key":"ref27","first-page":"137","article-title":"Perfor-mance evaluation of GSM handover traffic in a GPRS\/GSM network","author":"ventura agustina","year":"2003","journal-title":"Proc 8th IEEE Int'l Symp on Computers and Communications"},{"key":"ref3","first-page":"146","article-title":"Approxi-mate symbolic model checking of continuous-time Markov chains","author":"baier","year":"1999","journal-title":"Proc of CONCUR'99 LNCS 1664"},{"key":"ref6","first-page":"420","article-title":"Towards model checking stochastic process algebra","author":"hermanns","year":"2000","journal-title":"Proc of IFM'00 LNCS 1945"},{"key":"ref5","first-page":"780","article-title":"On the logical characterisation of performability properties","author":"baier","year":"2000","journal-title":"ICALP'00 LNCS 1853"},{"article-title":"Automatische Verifikation Stochasti-scher Systeme","year":"2004","author":"meyer-kayser","key":"ref8"},{"key":"ref7","first-page":"110","article-title":"Implementing a model checker for performability be-haviour","author":"hermanns","year":"2001","journal-title":"Proc 5th Int'l Workshop on Performability Modelling of Computer and Communication Systems"},{"key":"ref2","first-page":"269","article-title":"Verifying continuous time Markov chains","author":"aziz","year":"1996","journal-title":"CAV'96 LNCS 1102"},{"key":"ref9","first-page":"19","article-title":"Model checking pathCSL","author":"baier","year":"2003","journal-title":"Proc 6th Int'l Workshop on Performability Modeling of Computer and Communication Systems"},{"journal-title":"Model checking","year":"1999","author":"clarke","key":"ref1"},{"key":"ref20","first-page":"71","article-title":"Syntax, semantics, equiv-alences, and axioms for MTIPP","author":"hermanns","year":"1994","journal-title":"PAPM'94"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44618-4_23"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1016\/S1567-8326(02)00068-1"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2003.1205180"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1145\/5397.5399"},{"article-title":"Analysis of GSM handover using coloured Petri nets","year":"2003","author":"thomsen","key":"ref26"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1002\/0470841931"}],"event":{"name":"International Conference on Dependable Systems and Networks, 2004","start":{"date-parts":[[2004,7,1]]},"location":"Florence, Italy","end":{"date-parts":[[2004,7,1]]}},"container-title":["International Conference on Dependable Systems and Networks, 2004"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/9172\/29105\/01311941.pdf?arnumber=1311941","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,3,14]],"date-time":"2017-03-14T04:23:22Z","timestamp":1489465402000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/1311941\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"references-count":28,"URL":"https:\/\/doi.org\/10.1109\/dsn.2004.1311941","relation":{},"subject":[],"published":{"date-parts":[[2004]]}}}