{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T23:34:21Z","timestamp":1725492861718},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540672609"},{"type":"electronic","value":"9783540464297"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-46429-8_18","type":"book-chapter","created":{"date-parts":[[2007,10,20]],"date-time":"2007-10-20T14:52:33Z","timestamp":1192891953000},"page":"247-261","source":"Crossref","is-referenced-by-count":10,"title":["Exploiting Modal Logic to Express Performance Measures"],"prefix":"10.1007","author":[{"given":"Graham","family":"Clark","sequence":"first","affiliation":[]},{"given":"Stephen","family":"Gilmore","sequence":"additional","affiliation":[]},{"given":"Jane","family":"Hillston","sequence":"additional","affiliation":[]},{"given":"Marina","family":"Ribaudo","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,12,20]]},"reference":[{"key":"18_CR1","unstructured":"P. G. Harrison and N. M. Patel. Performance Modelling of Communication Networks and Computer Architectures. International Computer Science Series. Addison-Wesley, 1993."},{"key":"18_CR2","unstructured":"M. Ajmone Marsan, G. Balbo, G. Conte, S. Donatelli, and G. Franceschinis. Modelling with Generalized Stochastic Petri Nets. John Wiley, 1995."},{"key":"18_CR3","unstructured":"J.F. Meyer, A. Movaghar, and W.H. Sanders. Stochastic activity networks: Structure, behavior and application. In Proc of Int. Workshop on Timed Petri Nets, pages 106\u2013115, Torino, Italy, 1985. IEEE Computer Society Press."},{"key":"18_CR4","doi-asserted-by":"crossref","unstructured":"J. Hillston. A Compositional Approach to Performance Modelling. Cambridge University Press, 1996.","DOI":"10.1017\/CBO9780511569951"},{"key":"18_CR5","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\u201993, 1993."},{"key":"18_CR6","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/S0304-3975(97)00127-8","volume":"201","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. Theoretical Computer Science, 201:1\u201354, July 1998.","journal-title":"Theoretical Computer Science"},{"key":"18_CR7","series-title":"Semi-Markov and Decision Processes","first-page":"851","volume-title":"Dynamic Probabilistic Systems","author":"R. A. Howard","year":"1971","unstructured":"R. A. Howard. Dynamic Probabilistic Systems, volume II: Semi-Markov and Decision Processes, chapter 13, pages 851\u2013915. John Wiley & Sons, New York, 1971."},{"key":"18_CR8","unstructured":"J. Bryans, H. Bowman, and J. Derrick. Analysis of a Multimedia Stream using Stochastic Process Algebra. In C. Priami, editor, Proc. of 6th Int. Workshop on Process Algebras and Performance Modelling, pages 51\u201369, Nice, France, September 1998."},{"issue":"5","key":"18_CR9","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. Formal Aspects of Computing, 6(5):512\u2013535, 1994.","journal-title":"Formal Aspects of Computing"},{"key":"18_CR10","doi-asserted-by":"crossref","unstructured":"M. Huth and M. Kwiatkowska. Quantitative analysis and model checking. In Proceedings, Twelth Annual IEEE Symposium on Logic in Computer Science, pages 111\u2013122, Warsaw, Poland, 29 June\u20132 July 1997. IEEE Computer Society Press.","DOI":"10.1109\/LICS.1997.614940"},{"key":"18_CR11","doi-asserted-by":"crossref","unstructured":"V. Hartonas-Garmhausen. Probabilistic Symbolic Model Checking with Engineering Models and Applications. PhD thesis, Carnegie Mellon University, 1998.","DOI":"10.1007\/3-540-48778-6_6"},{"key":"18_CR12","unstructured":"L. de Alfaro. How to specify and verify the long-run average behavior of probabilistic systems. In LICS: IEEE Symposium on Logic in Computer Science, 1998."},{"key":"18_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"353","DOI":"10.1007\/3-540-58021-2_20","volume-title":"Proc. of 7th Conf. on Mod. Techniques and Tools for Computer Perf. Eval.","author":"S. Gilmore","year":"1994","unstructured":"S. Gilmore and J. Hillston. The PEPA Workbench: A Tool to Support a Process Algebra-based Approach to Performance Modelling. In G. Haring and G. Kotsis, editors, Proc. of 7th Conf. on Mod. Techniques and Tools for Computer Perf. Eval., volume 794 of LNCS, pages 353\u2013368, 1994."},{"key":"18_CR14","unstructured":"G. Clark. Formalising the Specification of Rewards with PEPA. In Proc. of 4th Process Algebras and Performance Modelling Workshop, pages 139\u2013160, July 1996."},{"key":"18_CR15","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"211","DOI":"10.1007\/3-540-48778-6_13","volume-title":"Proc. of 5th Int. AMAST Workshop on Real-Time and Probabilistic Systems","author":"G. Clark","year":"1999","unstructured":"G. Clark, S. Gilmore, and J. Hillston. Specifying performance measures for PEPA. In J.P. Katoen, editor, Proc. of 5th Int. AMAST Workshop on Real-Time and Probabilistic Systems, volume 1601 of LNCS, pages 211\u2013227, Bamberg, Germany, 1999. Springer-Verlag."},{"key":"18_CR16","doi-asserted-by":"crossref","unstructured":"S. Gilmore, J. Hillston, and M. Ribaudo. An efficient algorithm for aggregating PEPA models. To appear in IEEE Transactions on Software Engineering, 2000.","DOI":"10.1109\/32.922715"},{"issue":"1","key":"18_CR17","doi-asserted-by":"crossref","first-page":"11","DOI":"10.1049\/ip-sen:19990149","volume":"146","author":"G. Clark","year":"1999","unstructured":"G. Clark, S. Gilmore, J. Hillston, and N. Thomas. Experiences with the PEPA Performance Modelling Tools. IEE Proceedings\u2014Software, 146(1):11\u201319, February 1999. Special issue of papers from 14th UK Performance Engineering Workshop.","journal-title":"IEE Proceedings\u2014Software"},{"issue":"1","key":"18_CR18","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0890-5401(91)90030-6","volume":"94","author":"K. G. Larsen","year":"1991","unstructured":"K. G. Larsen and A. Skou. Bisimulation through probabilistic testing. Information and Computation, 94(1):1\u201328, September 1991.","journal-title":"Information and Computation"},{"issue":"1","key":"18_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. Journal of the ACM, 32(1):137\u2013161, January 1985.","journal-title":"Journal of the ACM"},{"key":"18_CR20","unstructured":"G. Clark. Techniques for the Construction and Analysis of Algebraic Performance Models. PhD thesis, The University of Edinburgh, 2000."},{"key":"18_CR21","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"358","DOI":"10.1007\/3-540-63165-8_192","volume-title":"24th Int. Colloquium on Automata, Languages and Programming","author":"M. Bernardo","year":"1997","unstructured":"M. Bernardo. An Algebra-Based Method to Associate Rewards with EMPA Terms. In P. Degano, R. Gorrieri, and A. Marchetti Spaccamela, editors, 24th Int. Colloquium on Automata, Languages and Programming, volume 1256 of LNCS, pages 358\u2013368, Bologna, Italy, July 1997. Springer-Verlag."},{"key":"18_CR22","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"146","DOI":"10.1007\/3-540-48320-9_12","volume-title":"Proceedings of CONCUR\u201999","author":"C. Baier","year":"1999","unstructured":"C. Baier, J.-P. Katoen, and H. Hermanns. Approximate symbolic model checking of continuous time Markov chains. In Proceedings of CONCUR\u201999, volume 1664 of LNCS, pages 146\u2013162, 1999."}],"container-title":["Lecture Notes in Computer Science","Computer Performance Evaluation.Modelling Techniques and Tools"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-46429-8_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,3]],"date-time":"2019-05-03T22:04:31Z","timestamp":1556921071000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-46429-8_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540672609","9783540464297"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/3-540-46429-8_18","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2000]]}}}