{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,16]],"date-time":"2026-03-16T10:11:21Z","timestamp":1773655881074,"version":"3.50.1"},"reference-count":27,"publisher":"Elsevier BV","issue":"1","license":[{"start":{"date-parts":[[2003,6,1]],"date-time":"2003-06-01T00:00:00Z","timestamp":1054425600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,8,22]],"date-time":"2013-08-22T00:00:00Z","timestamp":1377129600000},"content-version":"vor","delay-in-days":3735,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theoretical Computer Science"],"published-print":{"date-parts":[[2003,6]]},"DOI":"10.1016\/s0304-3975(02)00445-0","type":"journal-article","created":{"date-parts":[[2003,1,17]],"date-time":"2003-01-17T19:53:32Z","timestamp":1042833212000},"page":"63-81","source":"Crossref","is-referenced-by-count":6,"title":["On feasible cases of checking multi-agent systems behavior"],"prefix":"10.1016","volume":"303","author":[{"given":"Michael","family":"Dekhtyar","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alexander","family":"Dikovsky","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mars","family":"Valiev","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/S0304-3975(02)00445-0_BIB1","doi-asserted-by":"crossref","unstructured":"K.R. Apt, Logic programming. in: J. van Leeuwen (Ed.), Handbook of Theoretical Computer Science. Vol. B. Formal Models and Semantics, Chap. 10, Elsevier, Amsterdam, 1990, pp. 493\u2013574.","DOI":"10.1016\/B978-0-444-88074-1.50015-9"},{"key":"10.1016\/S0304-3975(02)00445-0_BIB2","doi-asserted-by":"crossref","unstructured":"T. Araragi, P. Attie, I. Keidar, K. Kogure, V. Luchangco, N. Lynch, K. Mano, On formal modeling of agent computations, in: NASA Workshop on Formal Approaches to Agent-Based Systems, Greenbelt, MD, April 2000.","DOI":"10.1007\/3-540-45484-5_4"},{"key":"10.1016\/S0304-3975(02)00445-0_BIB3","doi-asserted-by":"crossref","first-page":"533","DOI":"10.1007\/BF01211631","article-title":"METATEM","volume":"7","author":"Barringer","year":"1995","journal-title":"Formal Aspects Comput."},{"key":"10.1016\/S0304-3975(02)00445-0_BIB4","doi-asserted-by":"crossref","unstructured":"M. Benerecetti, F. Guinchiglia, L. Serafini, Model checking multiagent systems, Technical Report # 9708-07, Instituto Trentino di Cultura, 1998.","DOI":"10.1093\/logcom\/8.3.401"},{"key":"10.1016\/S0304-3975(02)00445-0_BIB5","series-title":"Proc. Internat. Workshop on the Computer aided verification, Stanford, Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-58179-0_50","article-title":"An automata-theoretic approach to branching time model checking","author":"Bernholz","year":"1994"},{"key":"10.1016\/S0304-3975(02)00445-0_BIB6","series-title":"Proc. Workshop on Logics of Programs","first-page":"52","article-title":"Design and synthesis of synchronization skeletons using branching time temporal logic","volume":"Vol. 181","author":"Clarke","year":"1981"},{"key":"10.1016\/S0304-3975(02)00445-0_BIB7","series-title":"Model Checking","author":"Clarke","year":"2000"},{"key":"10.1016\/S0304-3975(02)00445-0_BIB8","series-title":"Proc. 2nd Internat. A.P. Ershov Memorial Conf. on Perspective of Systems Informatics","first-page":"420","article-title":"On homeostatic behavior of dynamic deductive data bases","volume":"Vol. 1181","author":"Dekhtyar","year":"1996"},{"key":"10.1016\/S0304-3975(02)00445-0_BIB9","series-title":"Applying temporal logic to analysis of behavior of cooperating logic programs","first-page":"228","volume":"Vol. 1755","year":"2000"},{"key":"10.1016\/S0304-3975(02)00445-0_BIB10","unstructured":"M. Dekhtyar, A. Dikovsky, M. Valiev, On behavior of interacting agents, Research Report No. 02.01, IRIN, Universit\u00e9 de Nantes, March 2002, 33pp., http:\/\/www.sciences.univ-nantes.fr\/irin\/Vie\/RR\/."},{"key":"10.1016\/S0304-3975(02)00445-0_BIB11","series-title":"Handbook of Theoretical Computer Science","article-title":"Temporal and modal logic","author":"Emerson","year":"1990"},{"key":"10.1016\/S0304-3975(02)00445-0_BIB12","doi-asserted-by":"crossref","unstructured":"E.A. Emerson, Model checking and the mu-calculus, in: N. Immerman, P.H. Kolaitis (Eds.), Descriptive Complexity and Finite Models, Proc. DIMACS Workshop, 1996, pp. 185\u2013214.","DOI":"10.1090\/dimacs\/031\/06"},{"issue":"1","key":"10.1016\/S0304-3975(02)00445-0_BIB13","doi-asserted-by":"crossref","first-page":"12","DOI":"10.1145\/371282.371311","article-title":"Clausal temporal resolution","volume":"2","author":"Fisher","year":"2001","journal-title":"ACM Trans. Comput. Logic"},{"key":"10.1016\/S0304-3975(02)00445-0_BIB14","series-title":"Progress in Artificial Intelligence\u20146th Portuguese Conf. on Artificial Intelligence","first-page":"13","article-title":"Specifying and verifying distributed intelligent systems","volume":"Vol. 727","author":"Fisher","year":"1993"},{"issue":"1","key":"10.1016\/S0304-3975(02)00445-0_BIB15","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1023\/A:1010090405266","article-title":"A roadmap of agent research and development","volume":"1","author":"Jennings","year":"1998","journal-title":"Autonomous Agents Multi-Agent Systems"},{"key":"10.1016\/S0304-3975(02)00445-0_BIB16","doi-asserted-by":"crossref","unstructured":"O. Lichtenstein, A. Pnueli, Checking that finite state concurrent programs satisfy their linear specification, in: Proc. 12th ACM Symp. on Principles of Programming Languages, New Orleans, LA, 1985, pp. 97\u2013107.","DOI":"10.1145\/318593.318622"},{"key":"10.1016\/S0304-3975(02)00445-0_BIB17","series-title":"The Temporal Logic of Reactive and Concurrent Systems: Specification","author":"Manna","year":"1991"},{"issue":"4","key":"10.1016\/S0304-3975(02)00445-0_BIB18","doi-asserted-by":"crossref","first-page":"353","DOI":"10.1017\/S0269888998004020","article-title":"Architectures and applications of intelligent agents","volume":"13","author":"M\u00fcller","year":"1998","journal-title":"Knowledge Eng. Rev."},{"key":"10.1016\/S0304-3975(02)00445-0_BIB19","series-title":"Proc. 5th Internat. Symp. on Programming","first-page":"195","article-title":"Specification and verification of concurrent programs in CESAR","volume":"Vol. 137","author":"Queille","year":"1982"},{"key":"10.1016\/S0304-3975(02)00445-0_BIB20","unstructured":"A.S. Rao, M.P. Georgeff, A model-theoretic approach to the verification of situated reasoning systems, in: Proc. 13th Internat. Joint Conf. on Artificial Intelligence (IJCAI-93), Chamb\u00e9ry, France 1993, pp. 318\u2013324."},{"key":"10.1016\/S0304-3975(02)00445-0_BIB21","series-title":"Knowledge in Action: Logical Foundations for Specifying and Implementing Dynamical Systems","author":"Reiter","year":"2001"},{"key":"10.1016\/S0304-3975(02)00445-0_BIB22","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1016\/0004-3702(93)90034-9","article-title":"Agent oriented programming","volume":"60","author":"Shoham","year":"1993","journal-title":"Artificial Intelligence"},{"issue":"3","key":"10.1016\/S0304-3975(02)00445-0_BIB23","doi-asserted-by":"crossref","first-page":"733","DOI":"10.1145\/3828.3837","article-title":"The complexity of propositional linear temporal logic","volume":"32","author":"Sistla","year":"1985","journal-title":"J. ACM"},{"key":"10.1016\/S0304-3975(02)00445-0_BIB24","series-title":"Heterogeneous Agent Systems","author":"Subrahmanian","year":"2000"},{"key":"10.1016\/S0304-3975(02)00445-0_BIB25","unstructured":"M. Vardi, P. Wolper, An automata-theoretic approach to automatic program verification, in: Proc. IEEE Symp. on Logic in Computer Science, Cambridge, MA, 1986, pp. 332\u2013344."},{"key":"10.1016\/S0304-3975(02)00445-0_BIB26","doi-asserted-by":"crossref","unstructured":"M. Wooldridge, The computational complexity of agent design problem, in: E. Durfee (Ed.) Proc. 4th Internat. Conf. on Multi-Agent Systems (ICMAS 2000), IEEE Press, New York, 2000.","DOI":"10.1109\/ICMAS.2000.858472"},{"issue":"2","key":"10.1016\/S0304-3975(02)00445-0_BIB27","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1017\/S0269888900008122","article-title":"Intelligent agents","volume":"10","author":"Wooldridge","year":"1995","journal-title":"Knowledge Eng. Rev."}],"container-title":["Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397502004450?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397502004450?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2020,3,12]],"date-time":"2020-03-12T05:24:29Z","timestamp":1583990669000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0304397502004450"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,6]]},"references-count":27,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2003,6]]}},"alternative-id":["S0304397502004450"],"URL":"https:\/\/doi.org\/10.1016\/s0304-3975(02)00445-0","relation":{},"ISSN":["0304-3975"],"issn-type":[{"value":"0304-3975","type":"print"}],"subject":[],"published":{"date-parts":[[2003,6]]}}}