{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T20:33:13Z","timestamp":1761597193673,"version":"3.37.3"},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540008989"},{"type":"electronic","value":"9783540365778"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/3-540-36577-x_29","type":"book-chapter","created":{"date-parts":[[2010,3,29]],"date-time":"2010-03-29T21:12:04Z","timestamp":1269897124000},"page":"409-424","source":"Crossref","is-referenced-by-count":6,"title":["Modeling and Analysis of Power-Aware Systems"],"prefix":"10.1007","author":[{"given":"Oleg","family":"Sokolsky","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Anna","family":"Philippou","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Insup","family":"Lee","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kyriakos","family":"Christou","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2003,2,28]]},"reference":[{"key":"29_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"780","DOI":"10.1007\/3-540-45022-X_65","volume-title":"On the logical characterisation of performability properties","author":"C. Baier","year":"2000","unstructured":"C. Baier, B.R. Haverkort, H. Hermanns, and J.-P. Katoen. On the logical characterisation of performability properties. In Proceedings of ICALP 00, volume 1853 of LNCS, pages 780\u2013792, 2000."},{"key":"29_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"358","DOI":"10.1007\/3-540-63165-8_192","volume-title":"An algebra-based method to associate rewards with empa terms","author":"M. Bernardo","year":"1997","unstructured":"M. Bernardo. An algebra-based method to associate rewards with empa terms. In Proceedings of ICALP 97, volume 1256 of LNCS, pages 358\u2013368, July 1997."},{"key":"29_CR3","doi-asserted-by":"crossref","unstructured":"T. D. Burd and R. W. Brodersen. Energy efficient CMOS microprocessor design. In Proceedings of IEEE Hawaii International Conference on System Sciences. Volume 1: Architecture, pages 288\u2013297, 1995.","DOI":"10.1109\/HICSS.1995.375385"},{"key":"29_CR4","doi-asserted-by":"crossref","unstructured":"J-Y. Choi, I. Lee, and H.-L. Xie. The specification and schedulability analysis of real-time systems using ACSR. In Proceedings of Real-Time Systems Symposium, December 1995.","DOI":"10.1109\/REAL.1995.495216"},{"key":"29_CR5","doi-asserted-by":"crossref","unstructured":"E. Clarke, E. Emerson, and A. Prasad Sistla. Automatic verification of finite state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems, 8(2), 1986.","DOI":"10.1145\/5397.5399"},{"key":"29_CR6","doi-asserted-by":"crossref","unstructured":"L. de Alfaro. How to specify and verify the long-run average behavior of probabilistic systems. In Proceedings of IEEE Symposium on Logic in Computer Science, pages 454\u2013465, 1998.","DOI":"10.1109\/LICS.1998.705679"},{"key":"29_CR7","doi-asserted-by":"crossref","unstructured":"R. De Nicola and F. W. Vaandrager. Three logics for branching bisimulation. In Proceedings of LICS\u2019 90, 1990.","DOI":"10.1109\/LICS.1990.113739"},{"key":"29_CR8","unstructured":"H. Hansson. Time and probability in formal design of distributed systems. In Real-Time Safety Critical Systems, volume 1. Elsevier, 1994."},{"key":"29_CR9","doi-asserted-by":"crossref","unstructured":"H. Karlo. Linear Programming. Progress in Theoretical Computer Science. Birkhauser, 1991.","DOI":"10.1007\/978-0-8176-4844-2"},{"key":"29_CR10","doi-asserted-by":"crossref","unstructured":"I. Lee, P. Br\u00e9mond-Gr\u00e9goire, and R. Gerber. A process algebraic approach to the specification and analysis of resource-bound real-time systems. Proceedings of the IEEE, pages 158\u2013171, Jan 1994.","DOI":"10.1109\/5.259433"},{"key":"29_CR11","unstructured":"I. Lee, A. Philippou, and O. Sokolsky. Formal modeling and analysis of power-aware real-time systems. Technical Report MIS-CIS-02-12, Department of Computer and Information Science, University of Pennsylvania, 2002."},{"key":"29_CR12","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1145\/321738.321743","volume":"1","author":"C. L. Liu","year":"1973","unstructured":"C. L. Liu and J. W. Layland. Scheduling algorithms for multiprogramming in a hard real-time environment. Journal of the ACM 20, 1:46\u201361, 1973.","journal-title":"Journal of the ACM 20"},{"key":"29_CR13","doi-asserted-by":"crossref","unstructured":"A. Philippou, O. Sokolsky, R. Cleaveland, I. Lee, and S. Smolka. Probabilistic resource failure in real-time process algebra. In Proceedings of CONCUR 98, pages 389\u2013404, 1998.","DOI":"10.1007\/BFb0055637"},{"key":"29_CR14","doi-asserted-by":"crossref","unstructured":"P. Pillai and K. G. Shin. Real-time dynamic voltage scaling for low-power embedded operating systems. In Proceedings of ACM Symposium on Operating Systems Principles, 2001.","DOI":"10.1145\/502034.502044"},{"key":"29_CR15","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"481","DOI":"10.1007\/978-3-540-48654-1_35","volume-title":"Probabilistic simulations for probabilistic processes","author":"R. Segala","year":"1994","unstructured":"R. Segala and N. Lynch. Probabilistic simulations for probabilistic processes. In Proceedings CONCUR 94, Uppsala, Sweden, volume 836 of LNCS, pages 481\u2013496, 1994."},{"key":"29_CR16","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1023\/A:1018938205540","volume":"7","author":"O. Sokolsky","year":"1999","unstructured":"O. Sokolsky, I. Lee, and H. Ben-Abdallah. Specification and analysis of real-time systems with PARAGON. Annals of Software Engineering, 7:211\u2013234, 1999.","journal-title":"Annals of Software Engineering"},{"key":"29_CR17","doi-asserted-by":"crossref","unstructured":"M. Vardi. Automatic verification of probabilistic concurrent finite-state programs. In Proceedings of the Symposium on Foundations of Computer Science, pages 327\u2013338, 1985.","DOI":"10.1109\/SFCS.1985.12"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-36577-X_29","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,19]],"date-time":"2025-02-19T19:12:03Z","timestamp":1739992323000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-36577-X_29"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540008989","9783540365778"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/3-540-36577-x_29","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2003]]}}}