{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T09:41:14Z","timestamp":1725615674102},"reference-count":22,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010,9]]},"DOI":"10.1109\/time.2010.21","type":"proceedings-article","created":{"date-parts":[[2010,10,19]],"date-time":"2010-10-19T14:58:43Z","timestamp":1287500323000},"page":"43-50","source":"Crossref","is-referenced-by-count":15,"title":["Bounded Reachability for Temporal Logic over Constraint Systems"],"prefix":"10.1109","author":[{"given":"Marcello M.","family":"Bersani","sequence":"first","affiliation":[]},{"given":"Achille","family":"Frigeri","sequence":"additional","affiliation":[]},{"given":"Angelo","family":"Morzenti","sequence":"additional","affiliation":[]},{"given":"Matteo","family":"Pradella","sequence":"additional","affiliation":[]},{"given":"Matteo","family":"Rossi","sequence":"additional","affiliation":[]},{"given":"Pierluigi","family":"San Pietro","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"article-title":"Tense logic and the theory of linear order","year":"1968","author":"kamp","key":"ref10"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24727-2_10"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"key":"ref13","doi-asserted-by":"crossref","first-page":"163","DOI":"10.1145\/567446.567462","article-title":"On the temporal basis of fairness","author":"gabbay","year":"1980","journal-title":"POPL"},{"key":"ref14","first-page":"393","article-title":"The complexity of temporal logic model checking","author":"schnoebelen","year":"2002","journal-title":"Advances in Modal Logic 5"},{"key":"ref15","first-page":"409","article-title":"The declarative past and imperative future: Executable temporal logic for interactive systems","author":"gabbay","year":"1987","journal-title":"Temporal Logic in Specification"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2008.22"},{"key":"ref17","first-page":"193","article-title":"Symbolic model checking without BDDs","author":"biere","year":"1999","journal-title":"Proc of TACAS"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1109\/SEFM.2010.37"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(80)90059-6"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1145\/1287624.1287669"},{"key":"ref3","article-title":"The Effects of Bounding Syntactic Resources on Presburger LTL","author":"demri","year":"2006","journal-title":"LSV Tech Rep LSV-06-5"},{"key":"ref6","first-page":"268","article-title":"Multiple Counters Automata, Safety Analysis and Presburger Arithmetic","author":"comon","year":"1998","journal-title":"CAV"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-05089-3_47"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1007\/11901914_36"},{"article-title":"Symbolic methods for exploring infinite state spaces","year":"1998","author":"boigelot","key":"ref7"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36206-1_12"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44622-2_17"},{"key":"ref9","first-page":"438","article-title":"Lazy theorem proving for bounded model checking over infinite domains","author":"de moura","year":"2002","journal-title":"CADE"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-2(5:5)2006"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1109\/SEFM.2009.16"},{"key":"ref21","article-title":"SMT-LIB standard 1.2","author":"ranise","year":"2006","journal-title":"Tech Rep"}],"event":{"name":"2010 17th International Symposium on Temporal Representation and Reasoning (TIME)","start":{"date-parts":[[2010,9,6]]},"location":"Paris, France","end":{"date-parts":[[2010,9,8]]}},"container-title":["2010 17th International Symposium on Temporal Representation and Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/5600467\/5601852\/05601858.pdf?arnumber=5601858","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,5]],"date-time":"2019-06-05T12:24:32Z","timestamp":1559737472000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/5601858\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,9]]},"references-count":22,"URL":"https:\/\/doi.org\/10.1109\/time.2010.21","relation":{},"subject":[],"published":{"date-parts":[[2010,9]]}}}