{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,3,30]],"date-time":"2022-03-30T02:33:17Z","timestamp":1648607597787},"reference-count":24,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2006,3,1]],"date-time":"2006-03-01T00:00:00Z","timestamp":1141171200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Ann Math Artif Intell"],"published-print":{"date-parts":[[2006,3]]},"DOI":"10.1007\/s10472-006-9020-7","type":"journal-article","created":{"date-parts":[[2006,3,23]],"date-time":"2006-03-23T08:44:10Z","timestamp":1143103450000},"page":"289-315","source":"Crossref","is-referenced-by-count":6,"title":["Tableau-based automata construction for dynamic linear time temporal logic*"],"prefix":"10.1007","volume":"46","author":[{"given":"Laura","family":"Giordano","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alberto","family":"Martelli","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2006,3,24]]},"reference":[{"key":"9020_CR1","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1023\/A:1018985923441","volume":"22","author":"F. Bacchus","year":"1998","unstructured":"F. Bacchus and F. Kabanza, Planning for temporally extended goals, Annals of Mathematics and Artificial Intelligence 22 (1998) 5\u201327.","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"9020_CR2","unstructured":"D. Calvanese, G. De Giacomo and M.Y. Vardi, Reasoning about actions and planning in LTL action theories, in: Proc. Principles of Knowledge Representation and Reasoning, KR'02, (Morgan Kaufmann, 2002) pp. 593\u2013602."},{"key":"9020_CR3","doi-asserted-by":"crossref","unstructured":"M. Daniele, F. Giunchiglia and M.Y. Vardi, Improved automata generation for linear temporal logic, in: Proc. Computer Aided Verification, 11th International Conference, CAV'99, Lecture Notes in Computer Science, Vol. 1633 (Springer, 1999) pp. 249\u2013260.","DOI":"10.1007\/3-540-48683-6_23"},{"key":"9020_CR4","doi-asserted-by":"crossref","unstructured":"R. Gerth, D. Peled, M.Y. Vardi and P. Wolper, Simple on-the-fly automatic verification of linear temporal logic, in: Proc. 15th International Symposium on Protocol Specification, Testing and Verification XV, PSTV 1995 (IFIP Conference Proceedings 38 Chapman & Hall, 1996) pp. 3\u201318.","DOI":"10.1007\/978-0-387-34892-6_1"},{"issue":"2","key":"9020_CR5","doi-asserted-by":"crossref","first-page":"289","DOI":"10.1093\/jigpal\/9.2.273","volume":"9","author":"L. Giordano","year":"2001","unstructured":"L. Giordano, A. Martelli and C. Schwind, Reasoning about actions in dynamic linear time temporal logic, Logic Journal of the IGPL 9(2) (2001) 289\u2013303.","journal-title":"Logic Journal of the IGPL"},{"key":"9020_CR6","unstructured":"L. Giordano, A. Martelli and C. Schwind, Specifying and verifying systems of communicating agents in a temporal action logic, in: Proc. AI*IA 2003: Advances in Artificial Intelligence, 8th Congress of the Italian Association for Artificial Intelligence, Lecture Notes in Computer Science, Vol. 2829 (Springer, 2003) pp. 262\u2013274."},{"key":"9020_CR7","doi-asserted-by":"crossref","unstructured":"L. Giordano, A. Martelli and C. Schwind, Verifying communicating agents by model checking in a temporal action logic, in: Proc. Logics in Artificial Intelligence, 9th European Conference, JELIA 2004, Lecture Notes in Computer Science, Vol. 3229 (Springer, 2004) pp. 57\u201369.","DOI":"10.1007\/978-3-540-30227-8_8"},{"key":"9020_CR8","doi-asserted-by":"crossref","unstructured":"F. Giunchiglia and P. Traverso, Planning as model checking, in: Proc. The 5th European Conference on Planning, ECP'99, Lecture Notes in Computer Science, Vol. 1809 (Springer, 2000) pp. 1\u201320.","DOI":"10.1007\/10720246_1"},{"key":"9020_CR9","doi-asserted-by":"crossref","unstructured":"J.G. Henriksen and P.S. Thiagarajan, A product version of dynamic linear time temporal logic, in: Proc. CONCUR '97: Concurrency Theory, 8th International Conference, Lecture Notes in Computer Science, Vol. 1243 (Springer, 1997) pp. 45\u201358.","DOI":"10.1007\/3-540-63141-0_4"},{"issue":"1\u20133","key":"9020_CR10","doi-asserted-by":"crossref","first-page":"187","DOI":"10.1016\/S0168-0072(98)00039-6","volume":"96","author":"J.G. Henriksen","year":"1999","unstructured":"J.G. Henriksen and P.S. Thiagarajan, Dynamic linear time temporal logic, Annals of Pure and Applied Logic 96(1\u20133) (1999) 187\u2013207.","journal-title":"Annals of Pure and Applied Logic"},{"issue":"5","key":"9020_CR11","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G.J. Holzmann","year":"1997","unstructured":"G.J. Holzmann, The model checker SPIN, IEEE Transaction on Software Engineering 23(5) (1997) 279\u2013295.","journal-title":"IEEE Transaction on Software Engineering"},{"key":"9020_CR12","doi-asserted-by":"crossref","unstructured":"J. Hromkovic, S. Seibert and T. Wilke, Translating regular expressions into small \u025b-free nondeterministic finite automata, in: Proc. STACS 97, 14th Annual Symposium on Theoretical Aspects of Computer Science, Lecture Notes in Computer Science, Vol. 1200 (Springer, 1997) pp. 55\u201366.","DOI":"10.1007\/BFb0023448"},{"issue":"2","key":"9020_CR13","first-page":"167","volume":"55","author":"W. Penczek","year":"2003","unstructured":"W. Penczek and A. Lomuscio, Verifying epistemic properties of multi-agent systems via bounded model checking, Fundamenta Informaticae 55(2) (2003) 167\u2013185.","journal-title":"Fundamenta Informaticae"},{"key":"9020_CR14","unstructured":"M. Pistore and P. Traverso, Planning as model checking for extended goals in non-deterministic domains, in: Proc. of the Seventeenth International Joint Conference on Artificial Intelligence, IJCAI 2001 (Morgan Kaufmann, 2001) pp.479\u2013484."},{"key":"9020_CR15","doi-asserted-by":"crossref","unstructured":"R. Reiter, The frame problem in the situation calculus: A simple solution (sometimes) and a completeness result for goal regression, Artificial Intelligence and Mathematical Theory of Computation: Papers in Honor of John McCarthy, ed. V. Lifschitz (Academic, 1991) pp. 359\u2013380.","DOI":"10.1016\/B978-0-12-450010-5.50026-8"},{"issue":"12","key":"9020_CR16","doi-asserted-by":"crossref","first-page":"40","DOI":"10.1109\/2.735849","volume":"31","author":"M.P. Singh","year":"1998","unstructured":"M.P. Singh, Agent communication languages: Rethinking the principles, IEEE Computer 31(12) (1998) 40\u201347.","journal-title":"IEEE Computer"},{"key":"9020_CR17","doi-asserted-by":"crossref","first-page":"733","DOI":"10.1145\/3828.3837","volume":"32","author":"A.P. Sistla","year":"1985","unstructured":"A.P. Sistla and E.M. Clarke, The complexity of propositional linear temporal logic, Journal of the ACM 32 (1985) 733\u2013749.","journal-title":"Journal of the ACM"},{"issue":"12","key":"9020_CR18","doi-asserted-by":"crossref","first-page":"1104","DOI":"10.1109\/TC.1980.1675516","volume":"C-29","author":"R.G. Smith","year":"1980","unstructured":"R.G. Smith, The contract net protocol: High level communication and control in a distributed problem solver, IEEE Transactions on Computers C-29(12) (1980) 1104\u20131113.","journal-title":"IEEE Transactions on Computers"},{"key":"9020_CR19","doi-asserted-by":"crossref","unstructured":"F. Somenzi and R. Bloem, Efficient B\u00fcchi automata from LTL formulae, in: Proc. Computer Aided Verification, 12th International Conference, CAV 2000, Lecture Notes in Computer Science, Vol. 1855 (Springer, 2000) pp. 247\u2013263.","DOI":"10.1007\/10722167_21"},{"issue":"1","key":"9020_CR20","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1023\/A:1026185103185","volume":"75","author":"W. Hoek van der","year":"2003","unstructured":"W. van der Hoek and M.J.W. Wooldridge, Cooperation, knowledge, and time: Alternating-time temporal epistemic logic and its applications, Studia Logica 75(1) (2003) 125\u2013157.","journal-title":"Studia Logica"},{"key":"9020_CR21","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1006\/inco.1994.1092","volume":"115","author":"M. Vardi","year":"1994","unstructured":"M. Vardi and P. Wolper, Reasoning about infinite computations, Information and Computation 115 (1994) 1\u201337.","journal-title":"Information and Computation"},{"key":"9020_CR22","doi-asserted-by":"crossref","unstructured":"M. Wooldridge, M. Fisher, M.P. Huget and S. Parsons, Model checking multi-agent systems with MABLE, in: Proc. First International Joint Conference on Autonomous Agents and Multiagent Systems, AAMAS 2002 (ACM, 2002) pp. 952\u2013959.","DOI":"10.1145\/544862.544965"},{"key":"9020_CR23","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1016\/S0019-9958(83)80051-5","volume":"56","author":"P. Wolper","year":"1983","unstructured":"P. Wolper, Temporal logic can be more expressive, Information and Control 56 (1983) 72\u201399.","journal-title":"Information and Control"},{"key":"9020_CR24","doi-asserted-by":"crossref","unstructured":"P. Wolper, Constructing automata from temporal logic formulas: A tutorial, in: Lectures on Formal Methods and Performance Analysis FMPA 2000, Lecture Notes in Computer Science, Vol. 2090 (Springer, 2001) pp. 261\u2013277.","DOI":"10.1007\/3-540-44667-2_7"}],"container-title":["Annals of Mathematics and Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10472-006-9020-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10472-006-9020-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10472-006-9020-7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,29]],"date-time":"2019-05-29T13:51:49Z","timestamp":1559137909000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10472-006-9020-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,3]]},"references-count":24,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2006,3]]}},"alternative-id":["9020"],"URL":"https:\/\/doi.org\/10.1007\/s10472-006-9020-7","relation":{},"ISSN":["1012-2443","1573-7470"],"issn-type":[{"value":"1012-2443","type":"print"},{"value":"1573-7470","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006,3]]}}}