{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,1]],"date-time":"2025-06-01T04:08:58Z","timestamp":1748750938442,"version":"3.41.0"},"reference-count":24,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2015,10,29]],"date-time":"2015-10-29T00:00:00Z","timestamp":1446076800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Stud Logica"],"published-print":{"date-parts":[[2016,8]]},"DOI":"10.1007\/s11225-015-9637-9","type":"journal-article","created":{"date-parts":[[2015,10,29]],"date-time":"2015-10-29T09:59:42Z","timestamp":1446112782000},"page":"641-678","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Checking EMTLK Properties of Timed Interpreted Systems Via Bounded Model Checking"],"prefix":"10.1007","volume":"104","author":[{"given":"Bo\u017cena","family":"Wo\u017ana-Szcze\u015bniak","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrzej","family":"Zbrzezny","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,10,29]]},"reference":[{"key":"9637_CR1","first-page":"390","volume":"104","author":"R. Alur","year":"1993","unstructured":"Alur R., Henzinger T. A.: Real-time logics: complexity and expressiveness. Information and Computation 104, 390\u2013401 (1993)","journal-title":"Information and Computation"},{"issue":"1","key":"9637_CR2","doi-asserted-by":"crossref","first-page":"116","DOI":"10.1145\/227595.227602","volume":"43","author":"R. Alur","year":"1996","unstructured":"Alur R., Feder T., Henzinger T.: The benefits of relaxing punctuality. Journal of the ACM 43(1), 116\u2013146 (1996)","journal-title":"Journal of the ACM"},{"key":"9637_CR3","doi-asserted-by":"crossref","first-page":"75","DOI":"10.3233\/SAT190039","volume":"4","author":"A. Biere","year":"2008","unstructured":"Biere A.: Picosat essentials. Journal on Satisfiability, Boolean Modeling and Computation (JSAT) 4, 75\u201397 (2008)","journal-title":"Journal on Satisfiability, Boolean Modeling and Computation (JSAT)"},{"key":"9637_CR4","doi-asserted-by":"crossref","unstructured":"Biere, A., K. Heljanko, T. Junttila, T. Latvala, and V. Schuppan, Linear encodings of bounded ltl model checking, Logical Methods in Computer Science 2(5:5):1\u201364, 2006.","DOI":"10.2168\/LMCS-2(5:5)2006"},{"key":"9637_CR5","doi-asserted-by":"crossref","unstructured":"Blackburn, P., M. de Rijke, and Y. Venema, Modal Logic, vol. 53 of Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, Cambridge, 2001.","DOI":"10.1017\/CBO9781107050884"},{"key":"9637_CR6","doi-asserted-by":"crossref","unstructured":"Cabodi, G., P. Camurati, and S. Quer, Can BDDs compete with SAT solvers on bounded model checking?, in Proceedings of the 39th Annual Design Automation Conference (DAC\u20192002), ACM, New York, 2002, pp. 117\u2013122.","DOI":"10.1109\/DAC.2002.1012605"},{"issue":"1","key":"9637_CR7","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1023\/A:1011276507260","volume":"19","author":"E. Clarke","year":"2001","unstructured":"Clarke E., Biere A., Raimi R., Zhu Y.: Bounded model checking using satisfiability solving. Formal Methods in System Design 19(1), 7\u201334 (2001)","journal-title":"Formal Methods in System Design"},{"key":"9637_CR8","doi-asserted-by":"crossref","unstructured":"Emerson, E. A., Temporal and modal logic, in J. van Leeuwen, (ed.), Handbook of Theoretical Computer Science, vol. B, Chap. 16, Elsevier Science Publishers, 1990, pp. 996\u20131071.","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"key":"9637_CR9","doi-asserted-by":"crossref","unstructured":"Fagin, R., J. Y. Halpern, Y. Moses, and M. Y. Vardi, Reasoning about Knowledge, MIT Press, Cambridge, 1995.","DOI":"10.7551\/mitpress\/5803.001.0001"},{"key":"9637_CR10","doi-asserted-by":"crossref","unstructured":"Furia, C. A., and P. Spoletini, Tomorrow and all our yesterdays: MTL satisfiability over the integers, in Proceedings of the Theoretical Aspects of Computing (ICTAC\u20192008), vol. 5160 of LNCS. Springer-Verlag, New York, 2008, pp. 253\u2013264.","DOI":"10.1007\/978-3-540-85762-4_9"},{"key":"9637_CR11","doi-asserted-by":"crossref","unstructured":"Gammie, P., and R. van der Meyden, MCK: Model checking the logic of knowledge, in Proceedings of 16th International Conference on Computer Aided Verification (CAV\u201904), vol. 3114 of LNCS, Springer-Verlag, New York, 2004, pp. 479\u2013483.","DOI":"10.1007\/978-3-540-27813-9_41"},{"key":"9637_CR12","doi-asserted-by":"crossref","unstructured":"Huang, X., and R. van der Meyden, The complexity of epistemic model checking: Clock semantics and branching time, in Proceedings of the 2010 Conference on ECAI 2010: 19th European Conference on Artificial Intelligence, IOS Press, Amsterdam, 2010, pp. 549\u2013554.","DOI":"10.3233\/978-1-60750-606-5-549"},{"key":"9637_CR13","unstructured":"Levesque, H., A logic of implicit and explicit belief, in Proceedings of the 6th National Conference of the AAAI, Morgan Kaufman, Palo Alto, 1984, pp. 198\u2013202."},{"issue":"1","key":"9637_CR14","doi-asserted-by":"crossref","first-page":"63","DOI":"10.1023\/A:1026176900459","volume":"75","author":"A. Lomuscio","year":"2003","unstructured":"Lomuscio A., Sergot M.: Deontic interpreted systems. Studia Logica 75(1), 63\u201392 (2003)","journal-title":"Studia Logica"},{"key":"9637_CR15","doi-asserted-by":"crossref","unstructured":"Lomuscio, A., W. Penczek, and B. Wo\u017ana, Bounded model checking for knowledge and real time, Artificial Intelligence 171:1011\u20131038, 2007.","DOI":"10.1016\/j.artint.2007.05.005"},{"key":"9637_CR16","doi-asserted-by":"crossref","unstructured":"Lomuscio, A., H. Qu, and F. Raimondi, Mcmas: A model checker for the verification of multi-agent systems, in Proceedings of the 21st International Conference on Computer Aided Verification (CAV 2009), vol. 5643 of LNCS, Springer-Verlag, New York, 2009, pp. 682\u2013688.","DOI":"10.1007\/978-3-642-02658-4_55"},{"key":"9637_CR17","doi-asserted-by":"crossref","unstructured":"M\u0229ski, A., W. Penczek, M. Szreter, B. Wo\u017ana-Szcze\u015bniak, and A. Zbrzezny, BDD- versus SAT-based bounded model checking for the existential fragment of linear temporal logic with knowledge: algorithms and their performance, Autonomous Agents and Multi-Agent Systems 28(4):558\u2013604, 2014.","DOI":"10.1007\/s10458-013-9232-2"},{"key":"9637_CR18","doi-asserted-by":"crossref","unstructured":"Peled, D., All from one, one for all: On model checking using representatives, in Proceedings of the 5th International Conference on Computer Aided Verification (CAV\u201993), vol. 697 of LNCS, Springer-Verlag, New York, 1993, pp. 409\u2013423.","DOI":"10.1007\/3-540-56922-7_34"},{"key":"9637_CR19","doi-asserted-by":"crossref","unstructured":"Penczek, W., and A. Lomuscio, Verifying epistemic properties of multi-agent systems via bounded model checking, Fundamenta Informaticae 55(2):167\u2013185, 2003.","DOI":"10.1145\/860575.860609"},{"key":"9637_CR20","unstructured":"Tripakis, S., Minimization of timed systems. http:\/\/verimag.imag.fr\/~tripakis\/dea.ps.gz , 1998."},{"key":"9637_CR21","volume-title":"An introduction to multi-agent systems","author":"M. Wooldridge","year":"2002","unstructured":"Wooldridge M.: An introduction to multi-agent systems. Wiley, Chichester (2002)"},{"key":"9637_CR22","doi-asserted-by":"crossref","unstructured":"Wo\u017ana-Szcze\u015bniak, B., and A. Zbrzezny, A translation of the existential model checking problem from MITL to HLTL, Fundamenta Informaticae 122(4):401\u2013420, 2013.","DOI":"10.3233\/FI-2013-795"},{"key":"9637_CR23","doi-asserted-by":"crossref","unstructured":"Wo\u017ana-Szcze\u015bniak, B., and A. Zbrzezny, Checking MTL properties of discrete timed automata via bounded model checking, Fundamenta Informaticae 135(4):553\u2013568, 2014.","DOI":"10.1007\/s11225-015-9637-9"},{"issue":"3\u20134","key":"9637_CR24","first-page":"377","volume":"120","author":"A. Zbrzezny","year":"2012","unstructured":"Zbrzezny A.: A new translation from ECTL* to SAT. Fundamenta Informaticae 120(3\u20134), 377\u2013397 (2012)","journal-title":"Fundamenta Informaticae"}],"container-title":["Studia Logica"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11225-015-9637-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11225-015-9637-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11225-015-9637-9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,31]],"date-time":"2025-05-31T06:38:57Z","timestamp":1748673537000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11225-015-9637-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,10,29]]},"references-count":24,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2016,8]]}},"alternative-id":["9637"],"URL":"https:\/\/doi.org\/10.1007\/s11225-015-9637-9","relation":{},"ISSN":["0039-3215","1572-8730"],"issn-type":[{"type":"print","value":"0039-3215"},{"type":"electronic","value":"1572-8730"}],"subject":[],"published":{"date-parts":[[2015,10,29]]}}}