{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:24:59Z","timestamp":1761611099456},"reference-count":36,"publisher":"Elsevier BV","issue":"1","license":[{"start":{"date-parts":[[2003,1,1]],"date-time":"2003-01-01T00:00:00Z","timestamp":1041379200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,17]],"date-time":"2013-07-17T00:00:00Z","timestamp":1374019200000},"content-version":"vor","delay-in-days":3850,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theoretical Computer Science"],"published-print":{"date-parts":[[2003,1]]},"DOI":"10.1016\/s0304-3975(01)00090-1","type":"journal-article","created":{"date-parts":[[2002,10,28]],"date-time":"2002-10-28T17:15:47Z","timestamp":1035825347000},"page":"117-160","source":"Crossref","is-referenced-by-count":41,"title":["Performance measure sensitive congruences for Markovian process algebras"],"prefix":"10.1016","volume":"290","author":[{"given":"Marco","family":"Bernardo","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mario","family":"Bravetti","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/S0304-3975(01)00090-1_BIB1","series-title":"Modelling with Generalized Stochastic Petri Nets","author":"Ajmone Marsan","year":"1995"},{"key":"10.1016\/S0304-3975(01)00090-1_BIB2","doi-asserted-by":"crossref","unstructured":"C. Baier, B. Haverkort, H. Hermanns, J.-P. Katoen, On the logical characterisation of performability properties, Proc. 27th Internat. Colloq. on Automata, Languages and Programming (ICALP \u201900), Lecture Notes in Computer Science, Vol. 1853, Geneve, Switzerland, 2000, pp. 780\u2013792.","DOI":"10.1007\/3-540-45022-X_65"},{"key":"10.1016\/S0304-3975(01)00090-1_BIB3","unstructured":"C. Baier, J.-P. Katoen, H. Hermanns, Approximate symbolic model checking of continuous time Markov chains, Proc. 10th Internat. Conf. on Concurrency Theory (CONCUR \u201900), Lecture Notes in Computer Science, Vol. 1664, Eindhoven, The Netherlands, 1999, pp. 146\u2013162."},{"key":"10.1016\/S0304-3975(01)00090-1_BIB4","doi-asserted-by":"crossref","unstructured":"M. Bernardo, An algebra-based method to associate rewards with EMPA terms, Proc. 24th Internat. Colloq. on Automata, Languages and Programming (ICALP \u201997), Lecture Notes in Computer Science, Vol. 1256, Bologna, Italy, 1997, pp. 358\u2013368.","DOI":"10.1007\/3-540-63165-8_192"},{"key":"10.1016\/S0304-3975(01)00090-1_BIB5","unstructured":"M. Bernardo, Theory and application of extended Markovian process algebra, Ph.D. Thesis, University of Bologna, Italy, 1999 (http:\/\/www.di.unito.it\/\u223cbernardo\/)."},{"key":"10.1016\/S0304-3975(01)00090-1_BIB6","doi-asserted-by":"crossref","unstructured":"M. Bernardo, W.R. Cleaveland, S.T. Sims, W.J. Stewart, TwoTowers: a tool integrating functional and performance analysis of concurrent systems, Proc. IFIP Joint Internat. Conf. on Formal Description Techniques for Distributed Systems and Communication Protocols and Protocol Specification, Testing and Verification (FORTE\/PSTV \u201998), Kluwer, Paris, France, 1998, pp. 457\u2013467.","DOI":"10.1007\/978-0-387-35394-4_28"},{"key":"10.1016\/S0304-3975(01)00090-1_BIB7","unstructured":"M. Bravetti, A. Aldini, An asynchronous calculus for generative\u2013reactive probabilistic systems, Tech. Report UBLCS-2000-03, University of Bologna (Italy), 2000 (extended abstract in Proc. 8th Internat. Workshop on Process Algebra and Performance Modelling (PAPM \u201900), Carleton Scientific, Geneva, Switzerland, 2000, pp. 591\u2013605)."},{"key":"10.1016\/S0304-3975(01)00090-1_BIB8","doi-asserted-by":"crossref","unstructured":"M. Bravetti, M. Bernardo, Compositional asymmetric cooperations for process algebras with probabilities, priorities, and time, Tech. Report UBLCS-2000-01, University of Bologna, Italy, 2000 (extended abstract Proc. 1st Internat. Workshop on Models for Time Critical Systems (MTCS \u201900), Electronic Notes in Theoretical Computer Science, Vol. 39(3), State College, PA, 2000).","DOI":"10.1016\/S1571-0661(05)80749-2"},{"key":"10.1016\/S0304-3975(01)00090-1_BIB9","doi-asserted-by":"crossref","first-page":"237","DOI":"10.1016\/0166-5316(91)90003-L","article-title":"On the solution of GSPN reward models","volume":"12","author":"Ciardo","year":"1991","journal-title":"Performance Evaluation"},{"key":"10.1016\/S0304-3975(01)00090-1_BIB10","unstructured":"G. Clark, Formalising the specification of rewards with PEPA, Proc. 4th Workshop on Process Algebras and Performance Modelling (PAPM \u201996), CLUT, Torino, Italy, 1996, pp. 139\u2013160."},{"key":"10.1016\/S0304-3975(01)00090-1_BIB11","doi-asserted-by":"crossref","unstructured":"G. Clark, S. Gilmore, J. Hillston, Specifying performance measures for PEPA, Proc. 5th AMAST Internat. Workshop on Formal Methods for Real Time and Probabilistic Systems (ARTS \u201999), Lecture Notes in Computer Science, Vol. 1601, Bamberg, Germany, 1999, pp. 211\u2013227.","DOI":"10.1007\/3-540-48778-6_13"},{"key":"10.1016\/S0304-3975(01)00090-1_BIB12","series-title":"Model Checking","author":"Clarke","year":"1999"},{"key":"10.1016\/S0304-3975(01)00090-1_BIB13","doi-asserted-by":"crossref","unstructured":"W.R. Cleaveland, G. L\u00fcttgen, V. Natarajan, Priority in Process Algebras, Handbook of Process Algebra, Elsevier, 2001.","DOI":"10.1016\/B978-044482830-9\/50030-8"},{"key":"10.1016\/S0304-3975(01)00090-1_BIB14","doi-asserted-by":"crossref","unstructured":"W.R. Cleaveland, S. Sims, The NCSU concurrency workbench, Proc. 8th Internat. Conf. on Computer Aided Verification (CAV \u201996), Lecture Notes in Computer Science, Vol. 1102, New Brunswick, NJ, 1996, pp. 394\u2013397.","DOI":"10.1007\/3-540-61474-5_87"},{"key":"10.1016\/S0304-3975(01)00090-1_BIB15","series-title":"Decomposability: Queueing and Computer System Applications","author":"Courtois","year":"1977"},{"key":"10.1016\/S0304-3975(01)00090-1_BIB16","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1016\/0304-3975(84)90113-0","article-title":"Testing equivalences for processes","volume":"34","author":"De Nicola","year":"1983","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/S0304-3975(01)00090-1_BIB17","doi-asserted-by":"crossref","first-page":"59","DOI":"10.1006\/inco.1995.1123","article-title":"Reactive, generative and stratified models of probabilistic processes","volume":"121","author":"van Glabbeek","year":"1995","journal-title":"Inform. Comput."},{"key":"10.1016\/S0304-3975(01)00090-1_BIB18","doi-asserted-by":"crossref","first-page":"219","DOI":"10.1007\/BF01439850","article-title":"Specification techniques for Markov reward models","volume":"3","author":"Haverkort","year":"1993","journal-title":"Discrete Event Dyn. Systems: Theory Appl."},{"key":"10.1016\/S0304-3975(01)00090-1_BIB19","unstructured":"H. Hermanns, Leistungsvorhersage von Verhaltensbeschreibungen mittels Temporale Logik, contribution to the GI\/ITG Fachgespraech \u201995: Formale Beschreibungstechniken fuer Verteilte Systeme, 1995."},{"key":"10.1016\/S0304-3975(01)00090-1_BIB20","unstructured":"H. Hermanns, Interactive Markov chains, Ph.D. Thesis, University of Erlangen-N\u00fcrnberg, Germany, 1998."},{"key":"10.1016\/S0304-3975(01)00090-1_BIB21","series-title":"A Compositional Approach to Performance Modelling","author":"Hillston","year":"1996"},{"key":"10.1016\/S0304-3975(01)00090-1_BIB22","series-title":"Communicating Sequential Processes","author":"Hoare","year":"1985"},{"key":"10.1016\/S0304-3975(01)00090-1_BIB23","series-title":"Dynamic Probabilistic Systems","author":"Howard","year":"1971"},{"key":"10.1016\/S0304-3975(01)00090-1_BIB24","series-title":"Queueing Systems","author":"Kleinrock","year":"1975"},{"key":"10.1016\/S0304-3975(01)00090-1_BIB25","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0890-5401(91)90030-6","article-title":"Bisimulation through probabilistic testing","volume":"94","author":"Larsen","year":"1991","journal-title":"Inform. Comput."},{"key":"10.1016\/S0304-3975(01)00090-1_BIB26","series-title":"Distributed Algorithms","author":"Lynch","year":"1996"},{"key":"10.1016\/S0304-3975(01)00090-1_BIB27","doi-asserted-by":"crossref","first-page":"139","DOI":"10.1016\/0166-5316(92)90002-X","article-title":"Performability","volume":"14","author":"Meyer","year":"1992","journal-title":"Performance Evaluation"},{"key":"10.1016\/S0304-3975(01)00090-1_BIB28","series-title":"Communication and Concurrency","author":"Milner","year":"1989"},{"key":"10.1016\/S0304-3975(01)00090-1_BIB29","doi-asserted-by":"crossref","first-page":"413","DOI":"10.1016\/0166-5316(94)90061-2","article-title":"Reward model solution methods with impulse and rate rewards","volume":"20","author":"Qureshi","year":"1994","journal-title":"Performance Evaluation"},{"key":"10.1016\/S0304-3975(01)00090-1_BIB30","doi-asserted-by":"crossref","first-page":"215","DOI":"10.1007\/978-3-7091-9123-1_10","article-title":"A unified approach for specifying measures of performance, dependability, and performability","volume":"4","author":"Sanders","year":"1991","journal-title":"Dependable Comput. Fault Tolerant Systems"},{"key":"10.1016\/S0304-3975(01)00090-1_BIB31","unstructured":"R. Segala, Modeling and verification of randomized distributed real-time systems, Ph.D. Thesis, MIT, Boston, MA, 1995."},{"key":"10.1016\/S0304-3975(01)00090-1_BIB32","series-title":"Introduction to the Numerical Solution of Markov Chains","author":"Stewart","year":"1994"},{"key":"10.1016\/S0304-3975(01)00090-1_BIB33","doi-asserted-by":"crossref","first-page":"536","DOI":"10.1007\/BF01211867","article-title":"Processes with probabilities, priority and time","volume":"6","author":"Tofts","year":"1994","journal-title":"Formal Aspects Comput."},{"key":"10.1016\/S0304-3975(01)00090-1_BIB34","doi-asserted-by":"crossref","first-page":"197","DOI":"10.1016\/0166-5316(92)90004-Z","article-title":"Composite performance and dependability analysis","volume":"14","author":"Trivedi","year":"1992","journal-title":"Performance Evaluation"},{"key":"10.1016\/S0304-3975(01)00090-1_BIB35","doi-asserted-by":"crossref","first-page":"179","DOI":"10.1016\/0304-3975(90)90111-T","article-title":"Specification styles in distributed systems design and verification","volume":"89","author":"Vissers","year":"1991","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/S0304-3975(01)00090-1_BIB36","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/S0304-3975(97)00056-X","article-title":"Composition and behaviors of probabilistic I\/O automata","volume":"176","author":"Wu","year":"1997","journal-title":"Theoret. Comput. Sci."}],"container-title":["Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397501000901?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397501000901?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2020,3,11]],"date-time":"2020-03-11T00:51:35Z","timestamp":1583887895000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0304397501000901"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,1]]},"references-count":36,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2003,1]]}},"alternative-id":["S0304397501000901"],"URL":"https:\/\/doi.org\/10.1016\/s0304-3975(01)00090-1","relation":{},"ISSN":["0304-3975"],"issn-type":[{"value":"0304-3975","type":"print"}],"subject":[],"published":{"date-parts":[[2003,1]]}}}