{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:02:58Z","timestamp":1725663778340},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540525592"},{"type":"electronic","value":"9783540470359"}],"license":[{"start":{"date-parts":[[1990,1,1]],"date-time":"1990-01-01T00:00:00Z","timestamp":631152000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1990]]},"DOI":"10.1007\/3-540-52559-9_65","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T16:37:46Z","timestamp":1330187866000},"page":"180-207","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Modular verification of Petri Nets"],"prefix":"10.1007","author":[{"given":"Werner","family":"Damm","sequence":"first","affiliation":[]},{"given":"Gert","family":"D\u00f6hmen","sequence":"additional","affiliation":[]},{"given":"Volker","family":"Gerstner","sequence":"additional","affiliation":[]},{"given":"Bernhard","family":"Josko","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,4]]},"reference":[{"key":"7_CR1","unstructured":"H.Barringer, R.Kuiper: A Temporal Logic Specification Method Supporting Hierarchical Development, University of Manchester, 1983"},{"key":"7_CR2","doi-asserted-by":"crossref","unstructured":"H.Barringer, R.Kuiper, A.Pnueli: Now You May Compose Temporal Logic Specifications, Proc. 16th ACM Symposium on Theory of Computing, 1984, 51\u201363","DOI":"10.1145\/800057.808665"},{"key":"7_CR3","doi-asserted-by":"crossref","unstructured":"E.M. Clarke, E.A. Emerson, A.P. Sistla: Automatic verification of finite-state concurrent systems using temporal logic specifications: a practical approach. Tenth ACM Symposium on principles of Programming Languages (1983)","DOI":"10.1145\/567067.567080"},{"key":"7_CR4","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1016\/0167-8191(89)90128-2","volume":"9","author":"W. Damm","year":"1988","unstructured":"W. Damm, G. D\u00f6hmen: Specifying Distributed Computer Architectures in AADL, Parallel Computing, Vol 9, 1988, 193\u2013211","journal-title":"Parallel Computing"},{"key":"7_CR5","unstructured":"W.Damm, G.D\u00f6hmen: AADL: a Net-Based Specification Method for Computer Architecture Design, in: Languages for Parallel Architectures: Design, Semantics, and Implementation Models\", edt. J.de Bakker, Wiley & Sons, 1989"},{"key":"7_CR6","unstructured":"W.Damm, G.D\u00f6hmen, V.Gerstner, J.Helbig, B.Josko, F.Korf, T.Peikenkamp: AADL Language Document, University of Oldenburg, FRG, 1989"},{"key":"7_CR7","doi-asserted-by":"crossref","unstructured":"P.Degano, R.Gorrieri, S.Machetti: An excercise in concurrency: a CSP process as a Condition\/Event system, Advances on Petri-Nets 1988, edt G.Rozenberg, Lecture Notes in Computer science 340, Springer Verlag, 1988, 83\u2013105","DOI":"10.1007\/3-540-50580-6_25"},{"key":"7_CR8","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1016\/0167-6423(83)90017-5","volume":"2","author":"E.A. Emerson","year":"1982","unstructured":"E.A. Emerson, E.M. Clarke: Using branching time temporal logic to synthesisze synchronization skeletons, Science of Computer Programming, Vol 2, 1982, 241\u2013266","journal-title":"Science of Computer Programming"},{"key":"7_CR9","doi-asserted-by":"crossref","unstructured":"E.A. Emerson, J.Y. Halpern: Sometimes and not never revisited: On branching time versus linear time. 10th ACM Symposium on Principles of programming Languages. 1983","DOI":"10.1145\/567067.567081"},{"key":"7_CR10","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0022-0000(85)90001-7","volume":"30","author":"E.A. Emerson","year":"1985","unstructured":"E.A. Emerson, J.Y. Halpern: Decision procedures and expressiveness in the temporal logic of branching time. Journal of Computer and System Science 30 (1985), pp. 1\u201324","journal-title":"Journal of Computer and System Science"},{"key":"7_CR11","doi-asserted-by":"crossref","first-page":"56","DOI":"10.1109\/TCOM.1983.1095720","volume":"COM-31","author":"B. Hailpern","year":"1983","unstructured":"B. Hailpern, S. Owicki: Modular Verification of Computer Communication Protocols, IEEE Trans. on Communication, Vol COM-31, 1983,56\u201368","journal-title":"IEEE Trans. on Communication"},{"key":"7_CR12","doi-asserted-by":"crossref","unstructured":"D.Harel, A.Pnueli: On the Development of Reactive Systems, Nato ASI Series, Vol. F13, Logics and Models of Concurrent Systems, edt. K.Apt, Springer Verlag, 1985","DOI":"10.1007\/978-3-642-82453-1_17"},{"key":"7_CR13","unstructured":"M.Jazayeri, C.Ghezzi, D.Hoffman,. D.Middleton, M.Smotherman: Design and Implementation of a Language for Communicating Sequential Processes, IEEE Proc. 9th Int.Conf. on Parallel Processes, Harbor Spring, Michigan, USA, 1980"},{"key":"7_CR14","doi-asserted-by":"crossref","first-page":"280","DOI":"10.1007\/3-540-18088-5_23","volume":"267","author":"B. Josko","year":"1987","unstructured":"B. Josko: Modelchecking of CTL formulae under liveness assumptions. Proceedings ICALP 87. Lecture Notes in Computer Science 267 (1987), 280\u2013289","journal-title":"Lecture Notes in Computer Science"},{"key":"7_CR15","unstructured":"B. Josko: Verifying the correctness of AADL-modules using model checking. Proceedings REX-Workshop on Stepwise refinement of Distributed systems: models, formalisms, correctness"},{"key":"7_CR16","unstructured":"F. Korf: M-CSP \u2014 eine modulare Sprache mit Proze\u00dfkommunikation und ihre Implemntierung, Master Thesis, RWTH Aachen, 1987"},{"key":"7_CR17","doi-asserted-by":"crossref","first-page":"417","DOI":"10.1109\/TSE.1981.230844","volume":"7","author":"J. Misra","year":"1981","unstructured":"J. Misra, K.M. Chandy: Proofs of Networks of Processes, IEEE Trans. Software Enginering. 7, 1981, 417\u2013426","journal-title":"IEEE Trans. Software Enginering."},{"key":"7_CR18","doi-asserted-by":"crossref","first-page":"68","DOI":"10.1145\/357233.357237","volume":"6","author":"Z. Manna","year":"1984","unstructured":"Z. Manna,P. Wolper: Synthesis of Communicating Processes from Temporal Logic Specifications, ACM Toplas 6, 1984, 68\u201393","journal-title":"ACM Toplas"},{"key":"7_CR19","doi-asserted-by":"crossref","unstructured":"V.Nguyen, D.Gries, S.Owicki: A Model and Temporal Proof System for Network of Proceses, 12 POPL, 1985, 121\u2013131","DOI":"10.1145\/318593.318624"},{"key":"7_CR20","unstructured":"OCCAM Programming Manual, INMOS Ltd, Whitefriars, Lewins Mead, Bristol, England"},{"key":"7_CR21","doi-asserted-by":"crossref","unstructured":"A.Pnueli: In transition from Global to Modular Temporal Reasoning about Programs, in: Logics and Models of Concurrent Systems, edt. K.R.Apt, Springer Verlag, 1985, 123\u2013144","DOI":"10.1007\/978-3-642-82453-1_5"},{"key":"7_CR22","doi-asserted-by":"crossref","first-page":"510","DOI":"10.1007\/BFb0027047","volume":"224","author":"A. Pnueli","year":"1986","unstructured":"A. Pnueli, Applications of Temporal Logic to the Specification and Verification of Reactive Systems: a Survey of Current Trends, in: Current Trends in Concurrency, edts. J.W.de Bakker, W.-P. de Roever, G.Rozenberg, Lecture Notes in Computer Science 224, Springer Verlag, 1986, 510\u2013584","journal-title":"Lecture Notes in Computer Science"},{"key":"7_CR23","doi-asserted-by":"crossref","first-page":"403","DOI":"10.1007\/3-540-13345-3_37","volume":"172","author":"W. Reisig","year":"1984","unstructured":"W. Reisig: Partial Order Semantics versus Interleaving Semantics of CSP-like languages and its Impact on Fairness, Lecture Notes in Computer Science 172, Springer Verlag, 1984, 403\u2013413","journal-title":"Lecture Notes in Computer Science"},{"key":"7_CR24","first-page":"20","volume":"82","author":"S.P. Wolper","year":"1982","unstructured":"S.P. Wolper: Specification and Synthesis of Communicating Processes using an extended Temporal Logic, POPL 82, 1982, 20\u201333","journal-title":"POPL"},{"key":"7_CR25","doi-asserted-by":"crossref","unstructured":"P.Wolper: Expressing INteresting Properties of Programs in Propositional Temporal Logic, 13th POPL, 1986, 184\u2013193","DOI":"10.1145\/512644.512661"}],"container-title":["Lecture Notes in Computer Science","Stepwise Refinement of Distributed Systems Models, Formalisms, Correctness"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-52559-9_65","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,1,8]],"date-time":"2020-01-08T19:14:40Z","timestamp":1578510880000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-52559-9_65"}},"subtitle":["The temporal logic approach"],"short-title":[],"issued":{"date-parts":[[1990]]},"ISBN":["9783540525592","9783540470359"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/3-540-52559-9_65","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1990]]},"assertion":[{"value":"4 June 2005","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}