{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T13:19:56Z","timestamp":1725455996767},"publisher-location":"Berlin\/Heidelberg","reference-count":25,"publisher":"Springer-Verlag","isbn-type":[{"type":"print","value":"354058241X"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0013999","type":"book-chapter","created":{"date-parts":[[2005,11,23]],"date-time":"2005-11-23T02:34:32Z","timestamp":1132713272000},"page":"365-381","source":"Crossref","is-referenced-by-count":2,"title":["A temporal logic approach to implementation and refinement in timed Petri nets"],"prefix":"10.1007","author":[{"given":"Miguel","family":"Felder","sequence":"first","affiliation":[]},{"given":"Angelo","family":"Morzenti","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"no.4","key":"23_CR1","doi-asserted-by":"publisher","first-page":"431","DOI":"10.1145\/357146.357150","volume":"3","author":"K. Apt","year":"1981","unstructured":"K. Apt, \u201cTen years of Hoare's Logic: A survey \u2014 Part I,\u201d ACM-Transactions on Programming Languages and Systems, vol. 3, no. 4, pp. 431\u2013483, Oct 1981.","journal-title":"ACM-Transactions on Programming Languages and Systems"},{"key":"23_CR2","doi-asserted-by":"crossref","unstructured":"R. Alur and T.A. Henzinger, \u201cReal Time Logics: Complexity and Expressivness\u201d, Tech. Report no. STANCS901307, Appeared in the 5th IEEE LICS'90 (pp. 390\u2013401), 1990.","DOI":"10.21236\/ADA323441"},{"key":"23_CR3","series-title":"Ph.D. Thesis and Tech. Report 89-1040","volume-title":"Designing Distributed Services Using Refinement Mappings","author":"J. I. Aizikowitz","year":"1990","unstructured":"Jacob Itzhack Aizikowitz, \u201cDesigning Distributed Services Using Refinement Mappings\u201d, Ph.D. Thesis and Tech. Report 89-1040, Cornell University, Ithaca, New York, 1990."},{"key":"23_CR4","doi-asserted-by":"crossref","unstructured":"M.Abadi and L. Lamport, \u201cThe existenece of refinement mappings\u201d, Theoretical Computer Science 82 (1991) 253\u2013284, Elsevier Science Publiscers B.V.","DOI":"10.1016\/0304-3975(91)90224-P"},{"key":"23_CR5","doi-asserted-by":"crossref","unstructured":"W. Damm, G. Dohmen, V. Gerstner, and B. Josko, \u201cModular verification of Petri nets, the temporal logic approach,\u201d in Proceedings of Stepwise Refinement of Distributed Systems. Models, Formalisms, Correctnesss, LNCS 430, Springer Verlag, 1990, pp.181\u2013207.","DOI":"10.1007\/3-540-52559-9_65"},{"key":"23_CR6","volume-title":"A Mathematical Introduction to Logic","author":"H.B. Enderton","year":"1972","unstructured":"H.B. Enderton, A Mathematical Introduction to Logic. New York: Academic Press, 1972."},{"key":"23_CR7","doi-asserted-by":"crossref","unstructured":"M. Felder, C. Ghezzi, and M. Pezz\u00e8, \u201cAnalyzing refinements of state based specifications: the case of TB nets,\u201d in Proceedings of ISSTA'93, Cambridge, 1993, pp. 28\u201339.","DOI":"10.1145\/154183.154193"},{"key":"23_CR8","unstructured":"M. Felder, D. Mandrioli, and A. Morzenti, \u201cProving properties of real-time systems through logical specifications and Petri nets models,\u201d Tech. Rep., TR 91-072, Diparimento di Elettronica e Informazione, Politecnico di Milano, December 1991."},{"issue":"no.2","key":"23_CR9","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1109\/32.265634","volume":"20","author":"M. Felder","year":"1994","unstructured":"M. Felder, D. Mandrioli, and A. Morzenti, \u201cProving properties of real-time systems through logical specifications and Petri nets models,\u201d IEEE Transactions on Software Engineering. vol. 20, no. 2, pp. 127\u2013141, February 1994.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"23_CR10","doi-asserted-by":"crossref","unstructured":"M. Felder and A. Morzenti, \u201cValidating real-time systems by executing logic specifications in TRIO,\u201d in Proceedings of 14th International Conference on Software Engineering, ACM\/IEEE, 1992, pp. 199\u2013211.","DOI":"10.1145\/143062.143115"},{"key":"23_CR11","doi-asserted-by":"crossref","unstructured":"R. Glabbeek and U. Goltz, \u201cRefinement of actions in causality based models\u201d, in Proceedings of Stepwise Refinement of Distributed Systems. Models, Formalisms, Correctnesss, LNCS 430, Springer Verlag, 1990, pp. 266\u2013300.","DOI":"10.1007\/3-540-52559-9_68"},{"key":"23_CR12","volume-title":"Fundamentals of Software Engineering","author":"C. Ghezzi","year":"1991","unstructured":"C. Ghezzi, M. Jazayeri, and D. Mandrioli, Fundamentals of Software Engineering. Englewood Cliffs, N.J.: Prentice-Hall International Editors, 1991."},{"issue":"no.2","key":"23_CR13","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1016\/0164-1212(90)90074-V","volume":"12","author":"C. Ghezzi","year":"1990","unstructured":"C. Ghezzi, D. Mandrioli, and A. Morzenti, \u201cTRIO, a logic language for executable specifications of real-time systems,\u201d Journal of Systems and Software, vol. 12, no. 2, pp. 107\u2013123, May 1990.","journal-title":"Journal of Systems and Software"},{"key":"23_CR14","doi-asserted-by":"crossref","unstructured":"T. Henzinger, Z. Manna, and A. Pnueli, \u201cTemporal proof methodologies for real-time systems,\u201d in Proc.of the 18th Annual Symposium on Principles of Programming Languages, ACM-PRESS, 1991, pp. 353\u2013366.","DOI":"10.1145\/99583.99629"},{"key":"23_CR15","doi-asserted-by":"crossref","unstructured":"N.A. Lynch and H. Attiya,\u201cUsing mapping to prove timing properties\u201d Tech. Report MIT\/LCS\/TM-412,b Laboratory for Computer Science, MIT, 1989. Appeared in Proc. PODC'90","DOI":"10.1145\/93385.93428"},{"key":"23_CR16","volume-title":"Introduction to mathematical logic","author":"E. Mendelson","year":"1963","unstructured":"E. Mendelson, \u201cIntroduction to mathematical logic\u201d, Van Nostrand Reinold Company, New York, 1963."},{"issue":"no.9","key":"23_CR17","doi-asserted-by":"publisher","first-page":"1036","DOI":"10.1109\/TCOM.1976.1093424","volume":"24","author":"P.M. Merlin","year":"1976","unstructured":"P.M. Merlin and D.J. Farber, \u201cRecoverability of communication protocols \u2014 Implications of a theoretical study,\u201d IEEE Transactions on Communications, vol 24, no. 9, pp.1036\u20131043, September 1976","journal-title":"IEEE Transactions on Communications"},{"key":"23_CR18","unstructured":"K. M\u00fcller, \u201cConstructable Petri nets\u201d, in Proc. EIK 21. 1985, pp. 171\u2013199."},{"key":"23_CR19","series-title":"Advanced Software Development Series, 1","volume-title":"Temporal Logic For Real-Time Systems","author":"J. Ostroff","year":"1989","unstructured":"J. Ostroff, Temporal Logic For Real-Time Systems, Advanced Software Development Series, 1. Taunton, Somerset, England: Research Studies Press LTD., 1989."},{"key":"23_CR20","doi-asserted-by":"crossref","unstructured":"A. Pnueli, \u201cApplications of temporal logic to the specification and verification of reactive systems: A survey of current trends,\u201d LNCS 224, Springer-Verlag, 1986.","DOI":"10.1007\/BFb0027047"},{"key":"23_CR21","volume-title":"EATCS Monographs on Theoretical Computer Science","author":"W. Reisig","year":"1985","unstructured":"W. Reisig, Petri Nets: an Introduction., EATCS Monographs on Theoretical Computer Science, Springer Verlag, Berlin-New York, 1985."},{"key":"23_CR22","first-page":"35","volume":"no. 18","author":"I. Suzuki","year":"1979","unstructured":"I. Suzuki and T. Murata, \u201cA method of stepwise refinement and abstraction of Petri nets\u201d, Journal of Computer System Sciences, no. 18, 1979, pp. 35\u201346.","journal-title":"Journal of Computer System Sciences"},{"key":"23_CR23","first-page":"82","volume-title":"LNCS 246","author":"W. Vogler","year":"1986","unstructured":"Walter Vogler, \u201cBehaviour preserving refinements in Petri nets\u201d, in Proc. 12th Int. Worksop on Graph Theoretic Concepts in Computer Sciende, M\u00fcnchen, 1986. Springer Verlag, LNCS 246, pp. 82\u201393."},{"key":"23_CR24","doi-asserted-by":"crossref","unstructured":"Walter Vogler, \u201cFailures Semantics based on Interval Semiwords is a Congruence for Refinement\u201d, in Proc. STACS'90, 1990. Springer Verlag, LNCS 415, pp. 285\u2013297.","DOI":"10.1007\/3-540-52282-4_51"},{"key":"23_CR25","first-page":"49","volume-title":"Compostional Reachability analysis using process algebra","author":"W.J. Yeh","year":"1991","unstructured":"W.J. Yeh and M. Young, \u201cCompostional Reachability analysis using process algebra\u201d, in 4th Int. Workshop on Testing and Verifications, Victoria, Canada, 1991, ACM Sigsoft, pp. 49\u201350"}],"container-title":["Lecture Notes in Computer Science","Temporal Logic"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/www.springerlink.com\/index\/pdf\/10.1007\/BFb0013999","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,11]],"date-time":"2020-04-11T00:35:15Z","timestamp":1586565315000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0013999"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["354058241X"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/bfb0013999","relation":{},"subject":[]}}