{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T10:07:48Z","timestamp":1767262068803,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":35,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540411963"},{"type":"electronic","value":"9783540409113"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-40911-4_24","type":"book-chapter","created":{"date-parts":[[2007,10,19]],"date-time":"2007-10-19T09:23:29Z","timestamp":1192785809000},"page":"420-439","source":"Crossref","is-referenced-by-count":24,"title":["Towards Model Checking Stochastic Process Algebra"],"prefix":"10.1007","author":[{"given":"Holger","family":"Hermanns","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Joost-Pieter","family":"Katoen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Joachim","family":"Meyer-Kayser","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Markus","family":"Siegle","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2001,6,1]]},"reference":[{"issue":"2","key":"24_CR1","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1145\/190.191","volume":"2","author":"M. Marsan Ajmone","year":"1984","unstructured":"M. Ajmone Marsan, G. Conte, and G. Balbo. A class of generalised stochastic Petri nets for the performance evaluation of multiprocessor systems. ACM Tr. on Comp. Sys., 2(2): 93\u2013122, 1984.","journal-title":"ACM Tr. on Comp. Sys"},{"key":"24_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"269","DOI":"10.1007\/3-540-61474-5_75","volume-title":"CAV","author":"A. Aziz","year":"1996","unstructured":"A. Aziz, K. Sanwal, V. Singhal and R. Brayton. Verifying continuous time Markov chains. In CAV, LNCS 1102: 269\u2013276, 1996."},{"key":"24_CR3","series-title":"Lect Notes Comput Sci","volume-title":"CAV","author":"C. Baier","year":"2000","unstructured":"C. Baier, B.R. Haverkort, H. Hermanns and J.-P. Katoen. Model checking continuous-time Markov chains by transient analysis. In CAV, LNCS 1855, 2000."},{"key":"24_CR4","series-title":"Lect Notes Comput Sci","volume-title":"ICALP","author":"C. Baier","year":"2000","unstructured":"C. Baier, B.R. Haverkort, H. Hermanns and J.-P. Katoen. On the logical characterization of performability properties. In ICALP, LNCS 1853, 2000."},{"key":"24_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"146","DOI":"10.1007\/3-540-48320-9_12","volume-title":"CONCUR","author":"C. Baier","year":"1999","unstructured":"C. Baier, J.-P. Katoen and H. Hermanns. Approximate symbolic model checking of continuous-time Markov chains. In CONCUR, LNCS 1664: 146\u2013162, 1999."},{"issue":"2","key":"24_CR6","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1016\/S0020-0190(98)00038-6","volume":"66","author":"C. Baier","year":"1998","unstructured":"C. Baier and M. Kwiatkowska. On the verification of qualitative properties of probabilistic processes under fairness constraints. Inf. Proc. Letters, 66(2): 71\u201379, 1998.","journal-title":"Inf. Proc. Letters"},{"key":"24_CR7","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/S0304-3975(97)00127-8","volume":"202","author":"M. Bernardo","year":"1998","unstructured":"M. Bernardo and R. Gorrieri. A tutorial on EMPA: a theory of concurrent processes with nondeterminism, priorities, probabilities and time. Th. Comp. Sc., 202: 1\u201354, 1998.","journal-title":"Th. Comp. Sc."},{"key":"24_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"211","DOI":"10.1007\/3-540-48778-6_13","volume-title":"ARTS","author":"G. Clark","year":"1999","unstructured":"G. Clark, S. Gilmore, and J. Hillston. Specifying performance measures for PEPA. In ARTS, LNCS 1601: 211\u2013227, 1999."},{"issue":"6","key":"24_CR9","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1109\/6.499951","volume":"33","author":"E.M. Clarke","year":"1996","unstructured":"E.M. Clarke and R.P. Kurshan. Computer-aided verification. IEEE Spectrum, 33(6): 61\u201367, 1996.","journal-title":"IEEE Spectrum"},{"key":"24_CR10","unstructured":"E.M. Clarke, O. Grumberg and D. Peled. Model Checking. MIT Press, 1999."},{"key":"24_CR11","doi-asserted-by":"crossref","unstructured":"P.R. D\u2019Argenio, J.-P. Katoen, and E. Brinksma. Specification and analysis of soft real-time systems: Quantity and quality. In Proc. IEEE Real-Time Systems Symp., pp. 104\u2013114, IEEE CS Press, 1999.","DOI":"10.1109\/REAL.1999.818832"},{"key":"24_CR12","doi-asserted-by":"crossref","unstructured":"M. Diefenbruch, J. Hintelmann, B. M\u00fcller-Clostermann. The QUEST-approach for the performance evemluation of SDL-systems. In Proc. Form. Descritpion Techn. IX, pp. 229\u2013244, Chapman & Hall, 1996.","DOI":"10.1007\/978-0-387-35079-0_14"},{"key":"24_CR13","unstructured":"E.A. Emerson and C.-L. Lei. Temporal model checking under generalized fairness constraints. In Proc. Hawaii Int. Conf. on System Sc., pp. 277\u2013288, 1985."},{"key":"24_CR14","doi-asserted-by":"crossref","first-page":"187","DOI":"10.1007\/BF01384084","volume":"4","author":"A. Fantechi","year":"1994","unstructured":"A. Fantechi, S. Gnesi and G. Ristori. Model checking for action-based logics. Form. Meth. in Sys. Design, 4: 187\u2013203, 1994.","journal-title":"Form. Meth. in Sys. Design"},{"issue":"6","key":"24_CR15","doi-asserted-by":"crossref","first-page":"678","DOI":"10.1109\/TSE.1986.6312965","volume":"SE-12","author":"D. Ferrari","year":"1986","unstructured":"D. Ferrari. Considerations on the insularity of performance evaluation. IEEE Tr. on Softw. Eng., SE-12(6): 678\u2013683, 1986.","journal-title":"IEEE Tr. on Softw. Eng."},{"key":"24_CR16","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"121","DOI":"10.1007\/BFb0013851","volume-title":"Performance","author":"N. G\u00f6tz","year":"1993","unstructured":"N. G\u00f6tz, U. Herzog and M. Rettelbach. Multiprocessor and distributed system design: The integration of functional specification and performance analysis using stochastic process algebras. In Performance, LNCS 729: 121\u2013146, 1993."},{"issue":"5","key":"24_CR17","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1007\/BF01211866","volume":"6","author":"H. Hansson","year":"1994","unstructured":"H. Hansson and B. Jonsson. A logic for reasoning about time and reliability. Form. Asp. of Comp., 6(5): 512\u2013535, 1994.","journal-title":"Form. Asp. of Comp."},{"key":"24_CR18","first-page":"142","volume":"4","author":"C. Harvey","year":"1986","unstructured":"C. Harvey. Performance engineering as integral part of system design. Br. Telecom Techn. J., 4:142\u2013147, 1986.","journal-title":"Br. Telecom Techn. J."},{"issue":"1","key":"24_CR19","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1145\/2455.2460","volume":"32","author":"M. Hennessy","year":"1985","unstructured":"M. Hennessy and R. Milner. Algebraic laws for nondeterminism and concurrency. J. of the ACM, 32(1): 137\u2013161, 1985.","journal-title":"J. of the ACM"},{"key":"24_CR20","unstructured":"H. Hermanns. Interactive Markov Chains. PhD thesis, University of Erlangen-N\u00fcrnberg, 1998."},{"key":"24_CR21","unstructured":"H. Hermanns, U. Herzog and J.-P. Katoen. Process algebra for performance evaluation. Th. Comp. Sci., 2001 (to appear)."},{"issue":"1-4","key":"24_CR22","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1016\/S0166-5316(99)00056-5","volume":"39","author":"H. Hermanns","year":"2000","unstructured":"H. Hermanns, U. Herzog, U. Klehmet, V. Mertsiotakis and M. Siegle. Compositional performance modelling with the TIPPtool. Performance Evaluation, 39(1-4): 5\u201335, 2000.","journal-title":"Performance Evaluation"},{"key":"24_CR23","doi-asserted-by":"crossref","unstructured":"H. Hermanns, U. Herzog, and V. Mertsiotakis. Stochastic process algebras as a tool for performance and dependability modelling. In Proc. IEEE Int. Comp. Perf. and Dependability Symp., pages 102\u2013111. IEEE CS Press, 1995.","DOI":"10.1109\/IPDS.1995.395813"},{"key":"24_CR24","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"347","DOI":"10.1007\/3-540-46419-0_24","volume-title":"TACAS","author":"H. Hermanns","year":"2000","unstructured":"H. Hermanns, J.-P. Katoen, J. Meyer-Kayser and M. Siegle. A Markov chain model checker. In TACAS, LNCS 1785:347\u2013362, 2000."},{"key":"24_CR25","doi-asserted-by":"crossref","unstructured":"H. Hermanns, J.-P. Katoen, J. Meyer-Kayser and M. Siegle. Model checking stochastic process algebra. Tech. Rep. IMMD7-2\/00, University of Erlangen-N\u00fcrnberg, 2000.","DOI":"10.1007\/3-540-40911-4_24"},{"key":"24_CR26","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1007\/3-540-48778-6_15","volume-title":"ARTS","author":"H. Hermanns","year":"1999","unstructured":"H. Hermanns and M. Siegle. Bisimulation algorithms for stochastic process algebras and their BDD-based implementation. In ARTS, LNCS 1601:244\u2013265, 1999."},{"key":"24_CR27","unstructured":"U. Herzog and V. Mertsiotakis. Applying stochastic process algebras to failure modelling. In Proc. Workshop on Process Algebra and Performance Modelling, pp. 107\u2013126, Univ. Erlangen-N\u00fcrnberg, 1994."},{"key":"24_CR28","doi-asserted-by":"crossref","unstructured":"U. Herzog. Formal description, time and performance analysis. In Entwurf und Betrieb Verteilter Systeme, IFB 264:172\u2013190, Springer, 1990.","DOI":"10.1007\/978-3-642-76309-0_10"},{"key":"24_CR29","doi-asserted-by":"crossref","unstructured":"J. Hillston. A Compositional Approach to Performance Modelling. Cambridge University Press, 1996.","DOI":"10.1017\/CBO9780511569951"},{"key":"24_CR30","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","volume":"27","author":"D. Kozen","year":"1983","unstructured":"D. Kozen. Results on the propositional mu-calculus. Th. Comp. Sc., 27: 333\u2013354, 1983.","journal-title":"Th. Comp. Sc."},{"issue":"1","key":"24_CR31","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0890-5401(91)90030-6","volume":"94","author":"K.G. Larsen","year":"1992","unstructured":"K.G. Larsen and A. Skou. Bisimulation through probabilistic testing. Inf. and Comp., 94(1): 1\u201328, 1992.","journal-title":"Inf. and Comp."},{"key":"24_CR32","unstructured":"R. Mateescu and M. Sighireanu. Efficient on-the-fly model checking for regular alternation-free mu-calculus. Proc. Workshop on Form. Meth. for Industrial Critical Sys., pp. 65\u201386. GMD\/FOKUS, 2000."},{"key":"24_CR33","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"407","DOI":"10.1007\/3-540-53479-2_17","volume-title":"Semantics of Concurrency","author":"R. Nicola De","year":"1990","unstructured":"R. De Nicola and F.W. Vaandrager. Action versus state based logics for transition systems. In Semantics of Concurrency, LNCS 469: 407\u2013419, 1990."},{"issue":"2","key":"24_CR34","doi-asserted-by":"publisher","first-page":"458","DOI":"10.1145\/201019.201032","volume":"42","author":"R. Nicola De","year":"1995","unstructured":"R. De Nicola and F.W. Vaandrager. Three logics for branching bisimulation. J. of the ACM, 42(2): 458\u2013487, 1995.","journal-title":"J. of the ACM"},{"key":"24_CR35","doi-asserted-by":"crossref","unstructured":"W. Stewart. Introduction to the Numerical Solution of Markov Chains. Princeton Univ. Press, 1994.","DOI":"10.1515\/9780691223384"}],"container-title":["Lecture Notes in Computer Science","Integrated Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-40911-4_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,21]],"date-time":"2025-01-21T19:13:26Z","timestamp":1737486806000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-40911-4_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540411963","9783540409113"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/3-540-40911-4_24","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2000]]}}}