{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,29]],"date-time":"2026-03-29T16:30:35Z","timestamp":1774801835746,"version":"3.50.1"},"reference-count":26,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[1999,7,1]],"date-time":"1999-07-01T00:00:00Z","timestamp":930787200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[1999,7,1]],"date-time":"1999-07-01T00:00:00Z","timestamp":930787200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Formal Methods in System Design"],"published-print":{"date-parts":[[1999,7]]},"DOI":"10.1023\/a:1008739929481","type":"journal-article","created":{"date-parts":[[2002,12,22]],"date-time":"2002-12-22T11:37:32Z","timestamp":1040557052000},"page":"7-48","source":"Crossref","is-referenced-by-count":341,"title":["Reactive Modules"],"prefix":"10.1007","volume":"15","author":[{"given":"Rajeev","family":"Alur","sequence":"first","affiliation":[]},{"given":"Thomas A.","family":"Henzinger","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"207107_CR1","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1016\/0304-3975(91)90224-P","volume":"82","author":"M. Abadi","year":"1991","unstructured":"M. Abadi and L. Lamport, \u201cThe existence of refinement mappings,\u201d Theoretical Computer Science, Vol. 82, pp. 253\u2013284, 1991.","journal-title":"Theoretical Computer Science"},{"key":"207107_CR2","doi-asserted-by":"crossref","first-page":"507","DOI":"10.1145\/203095.201069","volume":"17","author":"M. Abadi","year":"1995","unstructured":"M. Abadi and L. Lamport, \u201cConjoining specifications,\u201d ACM Transactions on Programming Languages and Systems, Vol. 17, pp. 507\u2013534, 1995.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"207107_CR3","doi-asserted-by":"crossref","first-page":"177","DOI":"10.1016\/0020-0190(86)90132-8","volume":"23","author":"B. Alpern","year":"1986","unstructured":"B. Alpern, A.J. Demers, and F.B. Schneider, \u201cSafety without stuttering,\u201d Information Processing Letters, Vol. 23, pp. 177\u2013180, 1986.","journal-title":"Information Processing Letters"},{"key":"207107_CR4","doi-asserted-by":"crossref","unstructured":"R. Alur and T.A. Henzinger, \u201cLocal liveness for compositional modeling of fair reactive systems,\u201d in CAV 95: Computer-aided Verification, Lecture Notes in Computer Science 939, Springer-Verlag, pp. 166\u2013179, 1995.","DOI":"10.1007\/3-540-60045-0_49"},{"key":"207107_CR5","doi-asserted-by":"crossref","unstructured":"R. Alur, T.A. Henzinger, and S.K. Rajamani, \u201cSymbolic exploration of transition hierarchies,\u201d in TACAS 98: Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science 1384, Springer-Verlag, pp. 330\u2013344, 1998.","DOI":"10.1007\/BFb0054181"},{"key":"207107_CR6","doi-asserted-by":"crossref","unstructured":"R. Alur, T.A. Henzinger, F.Y.C. Mang, S. Qadeer, S.K. Rajamani, and S. Tasiran, \u201cMocha: Modularity in model checking,\u201d in CAV 98: Computer-aided Verification, Lecture Notes in Computer Science 1427, Springer-Verlag, pp. 521\u2013525, 1998.","DOI":"10.1007\/BFb0028774"},{"key":"207107_CR7","doi-asserted-by":"crossref","first-page":"103","DOI":"10.1016\/0167-6423(91)90001-E","volume":"16","author":"A. Benveniste","year":"1991","unstructured":"A. Benveniste, P. le Guernic, and C. Jacquemot, \u201cSynchronous programming with events and relations: The Signal language and its semantics,\u201d Science of Computer Programming, Vol. 16, pp. 103\u2013149, 1991.","journal-title":"Science of Computer Programming"},{"key":"207107_CR8","unstructured":"G. Berry and G. Gonthier, \u201cThe synchronous programming language Esterel: Design, semantics, implementation,\u201d Technical Report 842, INRIA, 1988."},{"key":"207107_CR9","doi-asserted-by":"crossref","unstructured":"G. Berry, S. Ramesh, and R.K. Shyamasundar, \u201cCommunicating reactive processes,\u201d in Proceedings of the 20th Annual Symposium on Principles of Programming Languages, ACM Press, pp. 85\u201398, 1993.","DOI":"10.1145\/158511.158526"},{"key":"207107_CR10","unstructured":"K.M. Chandy and J. Misra, Parallel Program Design: A Foundation, Addison-Wesley Publishing Company, 1988."},{"key":"207107_CR11","doi-asserted-by":"crossref","unstructured":"D.L. Dill, Trace Theory for Automatic Hierarchical Verification of Speed-independent Circuits, The MIT Press, 1989.","DOI":"10.7551\/mitpress\/6874.001.0001"},{"key":"207107_CR12","doi-asserted-by":"crossref","unstructured":"D.L. Dill, \u201cThe MUR\u00d8 verification system,\u201d in CAV 96: Computer-aided Verification, Lecture Notes in Computer Science 1102, Springer-Verlag, pp. 390\u2013393, 1996.","DOI":"10.1007\/3-540-61474-5_86"},{"key":"207107_CR13","doi-asserted-by":"crossref","first-page":"843","DOI":"10.1145\/177492.177725","volume":"16","author":"O. Grumberg","year":"1994","unstructured":"O. Grumberg and D.E. Long, \u201cModel checking and modular verification,\u201d ACM Transactions on Programming Languages and Systems, Vol. 16, pp. 843\u2013871, 1994.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"207107_CR14","doi-asserted-by":"crossref","unstructured":"N. Halbwachs, Synchronous Programming of Reactive Systems, Kluwer Academic Publishers, 1993.","DOI":"10.1007\/978-1-4757-2231-4"},{"key":"207107_CR15","doi-asserted-by":"crossref","unstructured":"T.A. Henzinger, S. Qadeer, and S.K. Rajamani, \u201cYou assume, we guarantee: Methodology and case studies,\u201d in CAV 98: Computer-aided Verification, Lecture Notes in Computer Science 1427, Springer-Verlag, pp. 440\u2013445, 1998.","DOI":"10.1007\/BFb0028765"},{"key":"207107_CR16","doi-asserted-by":"crossref","unstructured":"C.A.R. Hoare, Communicating Sequential Processes, Prentice-Hall, 1985.","DOI":"10.1007\/978-3-642-82921-5_4"},{"key":"207107_CR17","unstructured":"G.J. Holzmann, Design and Validation of Computer Protocols, Prentice-Hall, 1991."},{"key":"207107_CR18","doi-asserted-by":"crossref","unstructured":"R.P. Kurshan, Computer-aided Verification of Coordinating Processes, Princeton University Press, 1994.","DOI":"10.1515\/9781400864041"},{"key":"207107_CR19","doi-asserted-by":"crossref","unstructured":"R.P. Kurshan, M. Merritt, A. Orda, and S.R. Sachs, \u201cModeling asynchrony with a synchronous model,\u201d in CAV 95: Computer-aided Verification, Lecture Notes in Computer Science 939, Springer-Verlag, pp. 339\u2013352, 1995.","DOI":"10.1007\/3-540-60045-0_61"},{"key":"207107_CR20","doi-asserted-by":"crossref","first-page":"190","DOI":"10.1145\/69624.357207","volume":"5","author":"L. Lamport","year":"1983","unstructured":"L. Lamport, \u201cSpecifying concurrent program modules,\u201d ACM Transactions on Programming Languages and Systems, Vol. 5, pp. 190\u2013222, 1983.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"207107_CR21","unstructured":"N.A. Lynch, Distributed Algorithms, Morgan-Kaufmann, 1996."},{"key":"207107_CR22","doi-asserted-by":"crossref","unstructured":"Z. Manna and A. Pnueli, The Temporal Logic of Reactive and Concurrent Systems: Specification, Springer-Verlag, 1992.","DOI":"10.1007\/978-1-4612-0931-7"},{"key":"207107_CR23","doi-asserted-by":"crossref","unstructured":"K.L. McMillan, Symbolic Model Checking: An Approach to the State-explosion Problem, Kluwer Academic Publishers, 1993.","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"207107_CR24","unstructured":"R. Milner, Communication and Concurrency, Prentice-Hall, 1989."},{"key":"207107_CR25","doi-asserted-by":"crossref","unstructured":"E.W. Stark, \u201cA proof technique for rely-guarantee properties,\u201d in FST & TCS 85: Foundations of Software Technology and Theoretical Computer Science, Lecture Notes in Computer Science 206, Springer-Verlag, pp. 369\u2013391, 1985.","DOI":"10.1007\/3-540-16042-6_21"},{"key":"207107_CR26","unstructured":"R.J. van Glabbeek, \u201cComparative concurrency semantics and refinement of actions,\u201d Ph.D. Thesis, Vrije Universiteit te Amsterdam, 1990."}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1008739929481.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1008739929481\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1008739929481.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,5]],"date-time":"2025-08-05T04:23:27Z","timestamp":1754367807000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1008739929481"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999,7]]},"references-count":26,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1999,7]]}},"alternative-id":["207107"],"URL":"https:\/\/doi.org\/10.1023\/a:1008739929481","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[1999,7]]}}}