{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T17:11:49Z","timestamp":1760202709971},"publisher-location":"Cham","reference-count":28,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319402284"},{"type":"electronic","value":"9783319402291"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-40229-1_27","type":"book-chapter","created":{"date-parts":[[2016,6,11]],"date-time":"2016-06-11T12:54:04Z","timestamp":1465649644000},"page":"389-405","source":"Crossref","is-referenced-by-count":6,"title":["Interval Temporal Logic Model Checking: The Border Between Good and Bad HS Fragments"],"prefix":"10.1007","author":[{"given":"Laura","family":"Bozzelli","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alberto","family":"Molinari","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Angelo","family":"Montanari","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Adriano","family":"Peron","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pietro","family":"Sala","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,6,12]]},"reference":[{"issue":"11","key":"27_CR1","doi-asserted-by":"crossref","first-page":"832","DOI":"10.1145\/182.358434","volume":"26","author":"JF Allen","year":"1983","unstructured":"Allen, J.F.: Maintaining knowledge about temporal intervals. Commun. ACM 26(11), 832\u2013843 (1983)","journal-title":"Commun. ACM"},{"unstructured":"Bozzelli, L., Molinari, A., Montanari, A., Peron, A., Sala, P.: Interval Temporal Logic Model Checking: the Border Between Good and Bad HS Fragments (2016). https:\/\/www.dimi.uniud.it\/la-ricerca\/pubblicazioni\/preprints\/1.2016","key":"27_CR2"},{"issue":"1\u20133","key":"27_CR3","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1007\/s10472-013-9376-4","volume":"71","author":"D Bresolin","year":"2014","unstructured":"Bresolin, D., Della Monica, D., Goranko, V., Montanari, A., Sciavicco, G.: The dark side of interval temporal logic: marking the undecidability border. Ann. Math. Artif. Intell. 71(1\u20133), 41\u201383 (2014)","journal-title":"Ann. Math. Artif. Intell."},{"issue":"1","key":"27_CR4","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1093\/logcom\/exn063","volume":"20","author":"D Bresolin","year":"2010","unstructured":"Bresolin, D., Goranko, V., Montanari, A., Sala, P.: Tableau-based decision procedures for the logics of subinterval structures over dense orderings. J. Logic Comput. 20(1), 133\u2013166 (2010)","journal-title":"J. Logic Comput."},{"issue":"3","key":"27_CR5","doi-asserted-by":"crossref","first-page":"289","DOI":"10.1016\/j.apal.2009.07.003","volume":"161","author":"D Bresolin","year":"2009","unstructured":"Bresolin, D., Goranko, V., Montanari, A., Sciavicco, G.: Propositional interval neighborhood logics: expressiveness, decidability, and undecidable extensions. Ann. Pure Appl. Logic 161(3), 289\u2013304 (2009)","journal-title":"Ann. Pure Appl. Logic"},{"key":"27_CR6","volume-title":"Model Checking","author":"EM Clarke","year":"2002","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (2002)"},{"issue":"1","key":"27_CR7","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1145\/4904.4999","volume":"33","author":"EA Emerson","year":"1986","unstructured":"Emerson, E.A., Halpern, J.Y.: \u201cSometimes\u201d and \u201cnot never\u201d revisited: on branching versus linear time temporal logic. J. ACM 33(1), 151\u2013178 (1986)","journal-title":"J. ACM"},{"key":"27_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/10720246_1","volume-title":"Recent Advances in AI Planning","author":"F Giunchiglia","year":"2000","unstructured":"Giunchiglia, F., Traverso, P.: Planning as model checking. In: Biundo, S., Fox, M. (eds.) ECP 1999. LNCS, vol. 1809, pp. 1\u201320. Springer, Heidelberg (2000)"},{"issue":"2","key":"27_CR9","doi-asserted-by":"crossref","first-page":"421","DOI":"10.1145\/201019.201031","volume":"42","author":"G Gottlob","year":"1995","unstructured":"Gottlob, G.: NP trees and Carnap\u2019s modal logic. J. ACM 42(2), 421\u2013457 (1995)","journal-title":"J. ACM"},{"issue":"4","key":"27_CR10","doi-asserted-by":"crossref","first-page":"935","DOI":"10.1145\/115234.115351","volume":"38","author":"JY Halpern","year":"1991","unstructured":"Halpern, J.Y., Shoham, Y.: A propositional modal logic of time intervals. J. ACM 38(4), 935\u2013962 (1991)","journal-title":"J. ACM"},{"key":"27_CR11","volume-title":"Algorithmics: The Spirit of Computing","author":"D Harel","year":"1992","unstructured":"Harel, D.: Algorithmics: The Spirit of Computing. Wesley, Reading (1992)"},{"key":"27_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"290","DOI":"10.1007\/3-540-44464-5_21","volume-title":"Advances in Computing Science - ASIAN 2000","author":"K Lodaya","year":"2000","unstructured":"Lodaya, K.: Sharpening the undecidability of interval temporal logic. In: Kleinberg, R.D., Sato, M. (eds.) ASIAN 2000. LNCS, vol. 1961, pp. 290\u2013298. Springer, Heidelberg (2000)"},{"unstructured":"Lomuscio, A., Michaliszyn, J.: An epistemic Halpern-Shoham logic. In: IJCAI, pp. 1010\u20131016 (2013)","key":"27_CR13"},{"unstructured":"Lomuscio, A., Michaliszyn, J.: Decidability of model checking multi-agent systems against a class of EHS specifications. In: ECAI, pp. 543\u2013548 (2014)","key":"27_CR14"},{"unstructured":"Lomuscio, A., Michaliszyn, J.: Model checking epistemic Halpern-Shoham logic extended with regular expressions. CoRR abs\/1509.00608 (2015)","key":"27_CR15"},{"key":"27_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"450","DOI":"10.1007\/11691372_31","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Lomuscio","year":"2006","unstructured":"Lomuscio, A., Raimondi, F.: mcmas: a model checker for multi-agent systems. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 450\u2013454. Springer, Heidelberg (2006)"},{"issue":"2","key":"27_CR17","doi-asserted-by":"crossref","first-page":"217","DOI":"10.3233\/FI-2014-1011","volume":"131","author":"J Marcinkowski","year":"2014","unstructured":"Marcinkowski, J., Michaliszyn, J.: The undecidability of the logic of subintervals. Fundamenta Informaticae 131(2), 217\u2013240 (2014)","journal-title":"Fundamenta Informaticae"},{"doi-asserted-by":"crossref","unstructured":"Molinari, A., Montanari, A., Murano, A., Perelli, G., Peron, A.: Checking interval properties of computations. Acta Informatica (2015, accepted for publication)","key":"27_CR18","DOI":"10.1007\/s00236-015-0250-1"},{"doi-asserted-by":"crossref","unstructured":"Molinari, A., Montanari, A., Peron, A.: Complexity of ITL model checking: some well-behaved fragments of the interval logic HS. In: TIME, pp. 90\u2013100 (2015)","key":"27_CR19","DOI":"10.1109\/TIME.2015.12"},{"unstructured":"Molinari, A., Montanari, A., Peron, A.: A model checking procedure for interval temporal logics based on track representatives. In: CSL, pp. 193\u2013210 (2015)","key":"27_CR20"},{"unstructured":"Molinari, A., Montanari, A., Peron, A., Sala, P.: Model checking well-behaved fragments of HS: the (almost) final picture. In: KR (2016)","key":"27_CR21"},{"unstructured":"Moszkowski, B.: Reasoning about digital circuits. Ph.D. thesis, Dept. of Computer Science, Stanford University, Stanford, CA (1983)","key":"27_CR22"},{"doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: FOCS, pp. 46\u201357. IEEE (1977)","key":"27_CR23","DOI":"10.1109\/SFCS.1977.32"},{"issue":"1\u20132","key":"27_CR24","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/j.artint.2005.04.003","volume":"166","author":"I Pratt-Hartmann","year":"2005","unstructured":"Pratt-Hartmann, I.: Temporal prepositions and their logic. Artif. Intell. 166(1\u20132), 1\u201336 (2005)","journal-title":"Artif. Intell."},{"key":"27_CR25","first-page":"451","volume":"9","author":"P Roeper","year":"1980","unstructured":"Roeper, P.: Intervals and tenses. J. Philos. Logic 9, 451\u2013469 (1980)","journal-title":"J. Philos. Logic"},{"key":"27_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"790","DOI":"10.1007\/3-540-45061-0_62","volume-title":"Automata, Languages and Programming","author":"P Schnoebelen","year":"2003","unstructured":"Schnoebelen, P.: Oracle circuits for branching-time model checking. In: Baeten, J.C.M., Lenstra, J.K., Parrow, J., Woeginger, G.J. (eds.) ICALP 2003. LNCS, vol. 2719, pp. 790\u2013801. Springer, Heidelberg (2003)"},{"issue":"3","key":"27_CR27","doi-asserted-by":"crossref","first-page":"733","DOI":"10.1145\/3828.3837","volume":"32","author":"AP Sistla","year":"1985","unstructured":"Sistla, A.P., Clarke, E.M.: The complexity of propositional linear temporal logics. J. ACM 32(3), 733\u2013749 (1985)","journal-title":"J. ACM"},{"issue":"4","key":"27_CR28","doi-asserted-by":"crossref","first-page":"529","DOI":"10.1305\/ndjfl\/1093635589","volume":"31","author":"Y Venema","year":"1990","unstructured":"Venema, Y.: Expressiveness and completeness of an interval tense logic. Notre Dame J. Formal Logic 31(4), 529\u2013547 (1990)","journal-title":"Notre Dame J. Formal Logic"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-40229-1_27","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,9,22]],"date-time":"2020-09-22T04:09:50Z","timestamp":1600747790000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-40229-1_27"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319402284","9783319402291"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-40229-1_27","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}