{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,26]],"date-time":"2025-02-26T05:34:25Z","timestamp":1740548065288,"version":"3.38.0"},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540229063"},{"type":"electronic","value":"9783540301219"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-30121-9_18","type":"book-chapter","created":{"date-parts":[[2010,9,18]],"date-time":"2010-09-18T05:41:26Z","timestamp":1284788486000},"page":"183-195","source":"Crossref","is-referenced-by-count":0,"title":["Deductive Probabilistic Verification Methods for Embedded and Ubiquitous Computing"],"prefix":"10.1007","author":[{"given":"Satoshi","family":"Yamane","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Takashi","family":"Kanatani","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"18_CR1","doi-asserted-by":"crossref","first-page":"316","DOI":"10.1007\/978-1-4615-4016-8","volume-title":"Foundations of Real-time Computing: Formal Specifications and Methods","author":"A.M. Tilborg","year":"1991","unstructured":"Tilborg, A.M., Koob, G.M.: Foundations of Real-time Computing: Formal Specifications and Methods, p. 316. Kluwer Academic Pub., Dordrecht (1991)"},{"key":"18_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0031984","volume-title":"Real-Time: Theory in Practice","author":"J.W. Bakker de","year":"1992","unstructured":"de Bakker, J.W., Huizing, C., de Roever, W.P., Rozenberg, G.: REX 1991. LNCS, vol.\u00a0600. Springer, Heidelberg (1992)"},{"key":"18_CR3","volume-title":"Real-Time Systems Abstractions, Languages and Design Methodologies","author":"K.M. Kavi","year":"1992","unstructured":"Kavi, K.M.: Real-Time Systems Abstractions, Languages and Design Methodologies. IEEE Computer Society Press, Los Alamitos (1992)"},{"key":"18_CR4","series-title":"NATO ASI Series F: Computer and Systems Sciences, Vol. 170","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-59615-5","volume-title":"Verification of Digital and Hybrid Systems","author":"M.K. Inan","year":"2000","unstructured":"Inan, M.K., Kurshan, R.P.: Verification of Digital and Hybrid Systems. NATO ASI Series F: Computer and Systems Sciences, Vol. 170, vol.\u00a0170. Springer, Heidelberg (2000)"},{"key":"18_CR5","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R. Alur","year":"1994","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science\u00a0126, 183\u2013235 (1994)","journal-title":"Theoretical Computer Science"},{"key":"18_CR6","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1006\/inco.1993.1024","volume":"104","author":"R. Alur","year":"1993","unstructured":"Alur, R., Courcoubetis, C., Dill, D.L.: Model-Checking in Dense Real-Time. Information and Computation\u00a0104, 2\u201334 (1993)","journal-title":"Information and Computation"},{"key":"18_CR7","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1006\/inco.1994.1045","volume":"111","author":"T.A. Henzinger","year":"1994","unstructured":"Henzinger, T.A., Nicollin, X., Sifakis, J., Yovine, S.: Symbolic model checking for real-time systems. Information and Computation\u00a0111, 193\u2013244 (1994)","journal-title":"Information and Computation"},{"key":"18_CR8","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1016\/S0304-3975(01)00046-9","volume":"282","author":"M. Kwiatkowska","year":"2002","unstructured":"Kwiatkowska, M., Norman, G., Segala, R., Sproston, J.: Automatic verification of real-time systems with discrete probability distributions. Theoretical Computer Science\u00a0282, 101\u2013150 (2002)","journal-title":"Theoretical Computer Science"},{"key":"18_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"276","DOI":"10.1007\/978-3-540-40965-6_18","volume-title":"Advances in Computing Science \u2013 ASIAN 2003. Progamming Languages and Distributed Computation Programming Languages and Distributed Computation","author":"S. Yamane","year":"2003","unstructured":"Yamane, S.: Probabilistic Timed Simulation Verification and its application to Stepwise Refinement of Real-Time Systems. In: Saraswat, V.A. (ed.) ASIAN 2003. LNCS, vol.\u00a02896, pp. 276\u2013290. Springer, Heidelberg (2003)"},{"key":"18_CR10","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1145\/2166.357214","volume":"5","author":"S. Hart","year":"1983","unstructured":"Hart, S., Sharir, M., Pnueli, A.: Termination of Probabilistic Concurrent Programs. ACM Transactions on Programming Languages\u00a05, 356\u2013380 (1983)","journal-title":"ACM Transactions on Programming Languages"},{"key":"18_CR11","doi-asserted-by":"crossref","unstructured":"Sharir, M., Hart, S.: Probabilistic temporal logics for finite and bounded models. In: Proc. of the 16th ACM Symposium on Theory of Computing, pp. 1\u201313 (1984)","DOI":"10.1145\/800057.808660"},{"key":"18_CR12","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1016\/S0019-9958(82)91022-1","volume":"53","author":"D. Lehmann","year":"1982","unstructured":"Lehmann, D., Shelah, S.: Reasoning about time and chance. Information and Control\u00a053, 165\u2013198 (1982)","journal-title":"Information and Control"},{"key":"18_CR13","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: On the Extremely Fair Treatment of Probabilistic Algorithms. In: Proc. of the 15th ACM Symposium Theory of Computing, pp. 278\u2013290 (1983)","DOI":"10.1145\/800061.808757"},{"issue":"1","key":"18_CR14","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/BF01843570","volume":"1","author":"A. Pnueli","year":"1986","unstructured":"Pnueli, A., Zuck, L.: Verification of multiprocess probabilistic protocols. Distributed Computing\u00a01(1), 53\u201372 (1986)","journal-title":"Distributed Computing"},{"key":"18_CR15","unstructured":"Hansson, H.A.: Time and Probability in Formal Design of Distributed Systems. PhD thesis, Uppsala University (1991)"},{"key":"18_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1007\/BFb0031986","volume-title":"Real-Time: Theory in Practice","author":"R. Alur","year":"1991","unstructured":"Alur, R., Courcoubetis, C., Dill, D.L.: Verifying automata specifications of probabilistic real-time systems. In: Huizing, C., de Bakker, J.W., Rozenberg, G., de Roever, W.-P. (eds.) REX 1991. LNCS, vol.\u00a0600, pp. 28\u201344. Springer, Heidelberg (1991)"},{"key":"18_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1007\/3-540-54233-7_128","volume-title":"Automata, Languages and Programming","author":"R. Alur","year":"1991","unstructured":"Alur, R., Courcoubetis, C., Dill, D.L.: Model-checking for probabilistic real-time systems. In: Leach Albert, J., Monien, B., Rodr\u00edguez-Artalejo, M. (eds.) ICALP 1991. LNCS, vol.\u00a0510, pp. 115\u2013136. Springer, Heidelberg (1991)"},{"key":"18_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1007\/BFb0032002","volume-title":"Real-Time: Theory in Practice","author":"N.A. Lynch","year":"1992","unstructured":"Lynch, N.A., Vaandrager, F.W.: Forward and Backward Simulations for Timing-Based Systems. In: Huizing, C., de Bakker, J.W., Rozenberg, G., de Roever, W.-P. (eds.) REX 1991. LNCS, vol.\u00a0600, pp. 397\u2013446. Springer, Heidelberg (1992)"},{"key":"18_CR19","unstructured":"Segala, R.: Modeling and Verification of Randomized Distributed Real-Time Systems. PhD thesis, MIT (1995)"},{"key":"18_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1007\/BFb0020933","volume-title":"Hybrid Systems III","author":"Y. Kesten","year":"1996","unstructured":"Kesten, Y., Manna, Z., Pnueli, A.: Verifying Clocked Transition Systems. In: Alur, R., Sontag, E.D., Henzinger, T.A. (eds.) HS 1995. LNCS, vol.\u00a01066, pp. 13\u201340. Springer, Heidelberg (1996)"},{"issue":"3","key":"18_CR21","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1007\/s001650300007","volume":"14","author":"M.Z. Kwiatkowska","year":"2003","unstructured":"Kwiatkowska, M.Z., Norman, G., Sproston, J.: Probabilistic Model Checking of Deadline Properties in the IEEE 1394 FireWire Root Contention Protocol. Formal Aspects of Computing\u00a014(3), 295\u2013318 (2003)","journal-title":"Formal Aspects of Computing"},{"key":"18_CR22","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-4222-2","volume-title":"Temporal Verification of Reactive Systems : Safety","author":"Z. Manna","year":"1995","unstructured":"Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems: Safety. Springer, Heidelberg (1995)"},{"key":"18_CR23","doi-asserted-by":"crossref","unstructured":"Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems: Progress. Unpublished, Stanford University (1996), http:\/\/theory.stanford.edu\/zm\/","DOI":"10.1007\/978-1-4612-4222-2"},{"key":"18_CR24","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M.Z.: Model Checking for Probability and Time: From Theory to Practice. Invited talk at LICS 2003, pp.351\u2013360 (2003)","DOI":"10.1109\/LICS.2003.1210075"},{"key":"18_CR25","doi-asserted-by":"crossref","unstructured":"Vardi, M.Y.: Automatic verification of probabilistic concurrent finite-state systems. In: Proc. 26th IEEE Symp. Found. of Comp. Sci., pp. 327\u2013338 (1985)","DOI":"10.1109\/SFCS.1985.12"},{"issue":"5","key":"18_CR26","doi-asserted-by":"publisher","first-page":"1543","DOI":"10.1145\/186025.186058","volume":"16","author":"M. Abadi","year":"1994","unstructured":"Abadi, M., Lamport, L.: An Old-Fashioned Recipe for Real Time. ACM Transactions on Programming Languages and Systems\u00a016(5), 1543\u20131571 (1994)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"3","key":"18_CR27","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1016\/0167-6423(83)90017-5","volume":"2","author":"E.A. Emerson","year":"1982","unstructured":"Emerson, E.A., Clarke, E.M.: Using Branching Time Temporal Logic to Synthesize Synchronization Skeletons. Science of Computer Programming\u00a02(3), 241\u2013266 (1982)","journal-title":"Science of Computer Programming"}],"container-title":["Lecture Notes in Computer Science","Embedded and Ubiquitous Computing"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-30121-9_18.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,25]],"date-time":"2025-02-25T22:25:04Z","timestamp":1740522304000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-30121-9_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540229063","9783540301219"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-30121-9_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}