{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,17]],"date-time":"2026-02-17T22:23:06Z","timestamp":1771366986381,"version":"3.50.1"},"reference-count":32,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2002,3,1]],"date-time":"2002-03-01T00:00:00Z","timestamp":1014940800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2002,3,1]],"date-time":"2002-03-01T00:00:00Z","timestamp":1014940800000},"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":["Journal of Logic, Language and Information"],"published-print":{"date-parts":[[2002,3]]},"DOI":"10.1023\/a:1017588004618","type":"journal-article","created":{"date-parts":[[2002,12,29]],"date-time":"2002-12-29T22:59:26Z","timestamp":1041202766000},"page":"195-225","source":"Crossref","is-referenced-by-count":12,"title":["Compositional Verification of Multi-Agent Systems in Temporal Multi-Epistemic Logic"],"prefix":"10.1007","volume":"11","author":[{"given":"Joeri","family":"Engelfriet","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Catholijn M.","family":"Jonker","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jan","family":"Treur","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"334141_CR1","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1145\/151646.151649","volume":"15","author":"M. Abadi","year":"1993","unstructured":"Abadi, M. and Lamport, L., 1993, \u201cComposing specifications,\u201d ACM Transactions on Programming Languages and Systems 15, 73\u2013132.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"334141_CR2","first-page":"40","volume-title":"Proceedings of the 2nd International Conference on Principles of Knowledge Representation and Reasoning, KR'91","author":"H. Barringer","year":"1991","unstructured":"Barringer, H., Fisher, M., Gabbay, D., and Hunter, A., 1991, \u201cMeta-reasoning in executable temporal logic,\u201d pp. 40\u201349 in Proceedings of the 2nd International Conference on Principles of Knowledge Representation and Reasoning, KR'91, J. Allen, R. Fikes, and E. Sandewall, eds., San Francisco, CA: Morgan Kaufmann Publishers."},{"key":"334141_CR3","volume-title":"The Imperative Future: Principles of Executable Temporal Logic","author":"H. Barringer","year":"1996","unstructured":"Barringer, H., Fisher, M., Gabbay, D., Owens, R., and Reynolds, M., 1996, The Imperative Future: Principles of Executable Temporal Logic, Research Studies Press and New York: John Wiley & Sons."},{"key":"334141_CR4","first-page":"163","volume-title":"Lecture Notes in Artificial Intelligence","author":"M. Benerecetti","year":"1999","unstructured":"Benerecetti, M., Giunchiglia, F., and Serafini, L., 1999, \u201cA model-checking algorithm for multiagent systems,\u201d pp. 163\u2013176 in Intelligent Agents V, Proceedings of the International Workshop on Agent Theories, Architectures and Languages, ATAL'98, Lecture Notes in Artificial Intelligence, Vol. 1555, J.P. M\u00fcller, M.P. Singh, and A.S. Rao, eds., Berlin: Springer-Verlag."},{"key":"334141_CR5","first-page":"25","volume-title":"International Journal of Co-operative Information Systems, IJCIS","author":"F.M.T. Brazier","year":"1995","unstructured":"Brazier, F.M.T., Dunin-Keplicz, B.M., Jennings, N.R., and Treur, J., 1995, \u201cFormal specification of multi-agent systems: A real world case,\u201d pp. 25\u201332 in Proceedings of the First International Conference on Multi-Agent Systems, V. Lesser, ed., Cambridge, MA: MIT Press. Extended version in International Journal of Co-operative Information Systems, IJCIS 6, Special Issue on Formal Methods in Co-operative Information Systems: Multi-Agent Systems, M. Huhns and M. Singh, eds., pp. 67-94."},{"key":"334141_CR6","first-page":"49","volume-title":"Proceedings of the Third International Conference on Multi-Agent Systems","author":"F.M.T. Brazier","year":"1998","unstructured":"Brazier, F.M.T., Cornelissen, F., Gustavsson, R., Jonker, C.M., Lindeberg, O., Polak, B., and Treur, J., 1998, \u201cCompositional design and verification of a multi-agent system for one-to-many negotiation,\u201d pp. 49\u201356 in Proceedings of the Third International Conference on Multi-Agent Systems, Y. Demazeau, ed., New York: IEEE Computer Society Press."},{"key":"334141_CR7","doi-asserted-by":"crossref","first-page":"65","DOI":"10.1007\/BFb0026778","volume-title":"Knowledge Acquisition, Modelling and Management","author":"F. Cornelissen","year":"1997","unstructured":"Cornelissen, F., Jonker, C.M., and Treur, J., 1997, \u201cCompositional verification of knowledge-based systems: A case study for diagnostic reasoning,\u201d pp. 65\u201380 in Knowledge Acquisition, Modelling and Management, Proceedings of the 10th EKAW, E. Plaza and R Benjamins, eds., Lecture Notes in Artificial Intelligence, Vol. 1319, Berlin: Springer-Verlag."},{"key":"334141_CR8","unstructured":"Dams, D., Gerth, R., and Kelb, P., 1996, \u201cPractical symbolic model checking of the full \u00b5-calculus using compositional abstractions,\u201d Report, Eindhoven University of Technology, Department of Mathematics and Computer Science."},{"key":"334141_CR9","doi-asserted-by":"crossref","first-page":"233","DOI":"10.1305\/ndjfl\/1040046088","volume":"37","author":"J. Engelfriet","year":"1996","unstructured":"Engelfriet, J., 1996, \u201cMinimal temporal epistemic logic,\u201d Notre Dame Journal of Formal Logic 37, 233\u2013259 (Special issue on Combining Logics). 224 J. ENGELFRIET ET AL.","journal-title":"Notre Dame Journal of Formal Logic"},{"key":"334141_CR10","first-page":"111","volume-title":"Proceedings International Conference on Formal and Applied Practical Reasoning","author":"J. Engelfriet","year":"1996","unstructured":"Engelfriet, J. and Treur, J., 1996a, \u201cSpecification of nonmonotonic reasoning,\u201d pp. 111\u2013125 in Proceedings International Conference on Formal and Applied Practical Reasoning, D.M. Gabbay and H.J. Ohlbach, eds., Lecture Notes in Artificial Intelligence, Vol. 1085, Berlin: Springer-Verlag. Extended version in Journal of Applied Non-Classical Logic 10, 2000, 7-27."},{"key":"334141_CR11","doi-asserted-by":"crossref","first-page":"615","DOI":"10.1006\/jsco.1996.0068","volume":"22","author":"J. Engelfriet","year":"1996","unstructured":"Engelfriet, J. and Treur, J., 1996b, \u201cExecutable temporal logic for nonmonotonic reasoning,\u201d Journal of Symbolic Computation 22, 615\u2013625.","journal-title":"Journal of Symbolic Computation"},{"key":"334141_CR12","doi-asserted-by":"crossref","first-page":"369","DOI":"10.1023\/A:1008243611454","volume":"7","author":"J. Engelfriet","year":"1997","unstructured":"Engelfriet, J. and Treur, J., 1997, \u201cAn interpretation of default logic in temporal epistemic logic,\u201d Journal of Logic, Language and Information 7, 369\u2013388.","journal-title":"Journal of Logic, Language and Information"},{"key":"334141_CR13","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/5803.001.0001","volume-title":"Reasoning about Knowledge","author":"R. Fagin","year":"1995","unstructured":"Fagin, R., Halpern, J.Y., Moses, Y., and Vardi, M.Y., 1995, Reasoning about Knowledge, Cambridge, MA: MIT Press."},{"key":"334141_CR14","first-page":"5\/1","volume-title":"Assumptions in model-based diagnosis","author":"D. Fensel","year":"1996","unstructured":"Fensel D. and Benjamins, R., 1996, \u201cAssumptions in model-based diagnosis,\u201d pp. 5\/1\u20135\/18 in Proceedings of the 10th Banff Knowledge Acquisition for Knowledge-Based Systems Workshop, B.R. Gaines and M.A. Musen, eds., Calgary: SRDG Publications, Department of Computer Science, University of Calgary."},{"key":"334141_CR15","first-page":"4\/1","volume-title":"Specification and verification of knowledge-based systems","author":"D. Fensel","year":"1996","unstructured":"Fensel, D., Schonegge, A., Groenboom, R., and Wielinga, B., 1996, \u201cSpecification and verification of knowledge-based systems,\u201d pp. 4\/1\u20134\/20 in Proceedings of the 10th Banff Knowledge Acquisition for Knowledge-Based Systems Workshop, B.R. Gaines and M.A. Musen, eds., Calgary: SRDG Publications, Department of Computer Science, University of Calgary."},{"key":"334141_CR16","doi-asserted-by":"crossref","first-page":"203","DOI":"10.1007\/BF00156915","volume":"1","author":"M. Finger","year":"1992","unstructured":"Finger, M. and Gabbay, D., 1992, \u201cAdding a temporal dimension to a logic system,\u201d Journal of Logic, Language and Information 1, 203\u2013233.","journal-title":"Journal of Logic, Language and Information"},{"key":"334141_CR17","first-page":"480","volume-title":"Temporal Logic \u2014 Proceedings of the First International Conference","author":"M. Fisher","year":"1994","unstructured":"Fisher, M., 1994, \u201cA survey of Concurrent METATEM\u2014 The language and its applications,\u201d pp. 480\u2013505 in Temporal Logic \u2014 Proceedings of the First International Conference, D.M. Gabbay and H.J. Ohlbach, eds., Lecture Notes in Artificial Intelligence, Vol. 827, Berlin: Springer-Verlag."},{"key":"334141_CR18","doi-asserted-by":"crossref","unstructured":"Fisher, M. and Wooldridge, M., 1997, \u201cOn the formal specification and verification of multi-agent systems,\u201d International Journal of Co-operative Information Systems, IJCIS 6, Special issue on Formal Methods in Co-operative Information Systems: Multi-Agent Systems, M. Huhns and M. Singh, eds., pp. 37\u201365.","DOI":"10.1142\/S0218843097000057"},{"key":"334141_CR19","first-page":"45","volume-title":"Formal Specificiation and Complex Reasoning Systems","author":"E. Giunchiglia","year":"1993","unstructured":"Giunchiglia, E., Traverso, P., and Giunchiglia, F., 1993, \u201cMulti-context systems as a specification framework for complex reasoning systems,\u201d pp. 45\u201372 in Formal Specificiation and Complex Reasoning Systems, J. Treur and T. Wetter, eds., New York: Ellis Horwood."},{"key":"334141_CR20","doi-asserted-by":"crossref","first-page":"29","DOI":"10.1016\/0004-3702(94)90037-X","volume":"65","author":"F. Giunchiglia","year":"1994","unstructured":"Giunchiglia, F. and Serafini, L., 1994, \u201cMultilanguage hierarchical logics (or: How we can do without modal logics),\u201d Artificial Intelligence 65, 29\u201370.","journal-title":"Artificial Intelligence"},{"key":"334141_CR21","first-page":"304","volume":"38","author":"J. Halpern","year":"1986","unstructured":"Halpern, J. and Vardi, M.Y., 1986, \u201cThe complexity of reasoning about knowledge and time,\u201d pp. 304\u2013315 in Proceedings of the 18th\nACM\nSymposium on the Theory of Computing. Journal version in Journal of Computer and System Sciences 38, 1989, 195-237.","journal-title":"Journal of Computer and System Sciences"},{"key":"334141_CR22","unstructured":"Halpern, J., van der Meyden, R., and Vardi, M.Y., 1999, \u201cComplete axiomatizations for reasoning about knowledge and time,\u201d Report."},{"key":"334141_CR23","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1007\/BF01088595","volume":"6","author":"J. Hooman","year":"1994","unstructured":"Hooman, J., 1994, \u201cCompositional verification of a distributed real-time arbitration protocol,\u201d Real-Time Systems 6, 173\u2013206.","journal-title":"Real-Time Systems"},{"key":"334141_CR24","first-page":"350","volume-title":"International Journal of Co-perative Information Systems","author":"C.M. Jonker","year":"1998","unstructured":"Jonker, C.M. and Treur, J., 1998, \u201cCompositional verification of multi-agent Systems: A formal analysis of pro-activeness and reactiveness,\u201d pp. 350\u2013380 in Proceedings of the International Symposium on Compositionality, COMPOS'97, W.P. De Roever, H. Langmaack, and A. Pnueli, eds., Lecture Notes in Computer Science, Vol. 1536, Berlin: Springer-Verlag. Extended version in International Journal of Co-perative Information Systems, to appear."},{"key":"334141_CR25","volume-title":"A Deduction Model of Belief","author":"K. Konolige","year":"1986","unstructured":"Konolige, K., 1986, A Deduction Model of Belief, London: Pitman."},{"key":"334141_CR26","volume-title":"Formal Specification of Complex Reasoning Systems","author":"J. Treur","year":"1993","unstructured":"Treur, J. and Wetter, T., 1993, Formal Specification of Complex Reasoning Systems, New York: Ellis Horwood."},{"key":"334141_CR27","first-page":"745","volume-title":"Proceedings of the Eleventh European Conference on Artificial Intelligence, ECAI'94","author":"J. Treur","year":"1994","unstructured":"Treur, J. and Willems, M., 1994, \u201cA logical foundation for verification,\u201d pp. 745\u2013749 in Proceedings of the Eleventh European Conference on Artificial Intelligence, ECAI'94, A.G. Cohn, ed., New York: John Wiley & Sons. COMPOSITIONAL VERIFICATION OF MULTI-AGENT SYSTEMS 225"},{"key":"334141_CR28","doi-asserted-by":"crossref","DOI":"10.1007\/978-94-010-9868-7","volume-title":"The Logic of Time: A Model-Theoretic Investigation into the Varieties of Temporal Ontology and Temporal Discourse","author":"J.F.A.K. van Benthem","year":"1983","unstructured":"van Benthem, J.F.A.K., 1983, The Logic of Time: A Model-Theoretic Investigation into the Varieties of Temporal Ontology and Temporal Discourse, Dordrecht: Reidel."},{"key":"334141_CR29","first-page":"448","volume-title":"Proceedings IEEE Symposium on Logic in Computer Science, Paris, July","author":"R. van der Meyden","year":"1994","unstructured":"van der Meyden, R., 1994, \u201cAxioms for knowledge and time in distributed systems with perfect recall, pp. 448\u2013457 in Proceedings IEEE Symposium on Logic in Computer Science, Paris, July, New York: IEEE."},{"key":"334141_CR30","first-page":"257","volume-title":"Formal Specification of Complex Reasoning Systems","author":"F. van Harmelen","year":"1993","unstructured":"van Harmelen, F., Malec, J., Lopez de Manataras, R., and Treur, J., 1993, \u201cComparing formal specification languages for complex reasoning systems,\u201d pp. 257\u2013282 in Formal Specification of Complex Reasoning Systems, J. Treur and T. Wetter, eds., New York: Ellis Horwood."},{"key":"334141_CR31","first-page":"272","volume-title":"Proceedings 10th European Conference on Artificial Intelligence, ECAI'92","author":"I.A. van Langevelde","year":"1992","unstructured":"van Langevelde, I.A., Philipsen, A.W., and Treur, J., 1992, \u201cFormal specification of compositional architectures,\u201d pp. 272\u2013276 in Proceedings 10th European Conference on Artificial Intelligence, ECAI'92, B. Neumann, ed., New York: John Wiley and Sons."},{"key":"334141_CR32","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1017\/S0269888900008122","volume":"10","author":"M.J. Wooldridge","year":"1995","unstructured":"Wooldridge, M.J. and Jennings, N.R., 1995, \u201cIntelligent agents: Theory and practice,\u201d Knowledge Engineering Review 10, 115\u2013152.","journal-title":"Knowledge Engineering Review"}],"container-title":["Journal of Logic, Language and Information"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1017588004618.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1017588004618\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1017588004618.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,12]],"date-time":"2025-06-12T10:29:33Z","timestamp":1749724173000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1017588004618"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002,3]]},"references-count":32,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2002,3]]}},"alternative-id":["334141"],"URL":"https:\/\/doi.org\/10.1023\/a:1017588004618","relation":{},"ISSN":["0925-8531","1572-9583"],"issn-type":[{"value":"0925-8531","type":"print"},{"value":"1572-9583","type":"electronic"}],"subject":[],"published":{"date-parts":[[2002,3]]}}}