{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T22:29:34Z","timestamp":1725748174536},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642405365"},{"type":"electronic","value":"9783642405372"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-40537-2_12","type":"book-chapter","created":{"date-parts":[[2013,9,11]],"date-time":"2013-09-11T12:33:51Z","timestamp":1378902831000},"page":"119-133","source":"Crossref","is-referenced-by-count":4,"title":["Model Checking General Linear Temporal Logic"],"prefix":"10.1007","author":[{"given":"Tim","family":"French","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"John","family":"McCabe-Dansted","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mark","family":"Reynolds","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"12_CR1","unstructured":"Alur, R., Courcoubetis, C., Dill, D.L.: Model-checking for real-time systems. In: LICS 1990, pp. 414\u2013425. IEEE Computer Society (1990)"},{"key":"12_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"322","DOI":"10.1007\/BFb0032042","volume-title":"Automata, Languages and Programming","author":"R. Alur","year":"1990","unstructured":"Alur, R., Dill, D.L.: Automata for modeling real-time systems. In: Paterson, M. (ed.) ICALP 1990. LNCS, vol.\u00a0443, pp. 322\u2013335. Springer, Heidelberg (1990)"},{"issue":"2","key":"12_CR3","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1305\/ndjfl\/1093870820","volume":"26","author":"J.P. Burgess","year":"1985","unstructured":"Burgess, J.P., Gurevich, Y.: The decision problem for linear temporal logic. Notre Dame J. Formal Logic\u00a026(2), 115\u2013128 (1985)","journal-title":"Notre Dame J. Formal Logic"},{"key":"12_CR4","unstructured":"French, T., McCabe-Dansted, J.C., Reynolds, M.: Synthesis for temporal logic over the reals. In: Bolander, T., Bra\u00fcner, T., Ghilardi, S., Moss, L.S. (eds.) Advances in Modal Logic 2012, pp. 217\u2013238. College Publications (2012)"},{"key":"12_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/978-3-642-36039-8_6","volume-title":"Logic and Its Applications","author":"T. French","year":"2013","unstructured":"French, T., McCabe-Dansted, J., Reynolds, M.: Indiscrete models: Model building and model checking over linear time. In: Lodaya, K. (ed.) ICLA 2013. LNCS, vol.\u00a07750, pp. 50\u201368. Springer, Heidelberg (2013)"},{"key":"12_CR6","unstructured":"French, T., McCabe-Dansted, J.C., Reynolds, M.: Complexity of model checking general linear time. In: TIME 2013 (accepted, to appear, 2013)"},{"key":"12_CR7","unstructured":"French, T., McCabe-Dansted, J.C., Reynolds, M.: Model checking for compositional models of general linear time: Long version. Tech. rep., CSSE, UWA (Dec 2012), http:\/\/www.csse.uwa.edu.au\/~john\/papers\/ModelCheckZeno_tech.pdf"},{"key":"12_CR8","doi-asserted-by":"crossref","unstructured":"Gabbay, D., Hodkinson, I., Reynolds, M.: Temporal Logic: Mathematical Foundations and Computational Aspects, vol.\u00a01. Oxford University Press (1994)","DOI":"10.1093\/oso\/9780198537694.003.0001"},{"key":"12_CR9","doi-asserted-by":"crossref","unstructured":"Gabbay, D.M., Hodkinson, I.M., Reynolds, M.A.: Temporal expressive completeness in the presence of gaps. In: Oikkonen, J., V\u00e4\u00e4n\u00e4nen, J. (eds.) Logic Colloquium 1990, Proceedings ASL European Meeting 1990, Helsinki. Lecture Notes in Logic, vol.\u00a02, pp. 89\u2013121. Springer (1993)","DOI":"10.1017\/9781316718254.009"},{"key":"12_CR10","doi-asserted-by":"crossref","unstructured":"Gabbay, D.M., Pnueli, A., Shelah, S., Stavi, J.: On the temporal analysis of fairness. In: 7th ACM Symp. on Princ. of Prog. Languages, Las Vegas, pp. 163\u2013173 (1980)","DOI":"10.1145\/567446.567462"},{"key":"12_CR11","volume-title":"Stanford Encyclopedia of Philosophy","author":"N. Hugett","year":"2010","unstructured":"Hugett, N.: Zeno\u2019s paradoxes: 3.2 achilles and the tortoise. In: Zalta, E. (ed.) Stanford Encyclopedia of Philosophy. Chapman and Hall, Boca Raton (2010)"},{"key":"12_CR12","unstructured":"Kamp, H.: Tense logic and the theory of linear order. Ph.D., UCLA (1968)"},{"key":"12_CR13","doi-asserted-by":"crossref","first-page":"109","DOI":"10.4064\/fm-59-1-109-116","volume":"59","author":"H. L\u00e4uchli","year":"1966","unstructured":"L\u00e4uchli, H., Leonard, J.: On the elementary theory of linear order. Fundamenta Mathematicae 59, 109\u2013116 (1966)","journal-title":"Fundamenta Mathematicae"},{"key":"12_CR14","doi-asserted-by":"crossref","unstructured":"Mosterman, P.: 15.6 pathological behaviour classes, hybrid dynamic systems: Modeling and execution. In: Fishwick, P. (ed.) Handbook of Dynamic System Modelling, ch. 15, pp. 15\u201322 to 15\u201323. Chapman and Hall, Boca Raton (2007)","DOI":"10.1201\/9781420010855.ch15"},{"key":"12_CR15","unstructured":"McCabe-Dansted, J.C.: Model checker for general linear time (online applet and data) (2012), http:\/\/www.csse.uwa.edu.au\/~mark\/research\/Online\/mechecker.html"},{"key":"12_CR16","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: Proceedings of the 18th Symposium on Foundations of Computer Science, Providence, RI, pp. 46\u201357 (1977)","DOI":"10.1109\/SFCS.1977.32"},{"issue":"8","key":"12_CR17","doi-asserted-by":"publisher","first-page":"1063","DOI":"10.1016\/j.apal.2010.01.002","volume":"161","author":"M. Reynolds","year":"2010","unstructured":"Reynolds, M.: The complexity of the temporal logic over the reals. Annals of Pure and Applied Logic\u00a0161(8), 1063\u20131096 (2010), doi:10.1016\/j.apal.2010.01.002","journal-title":"Annals of Pure and Applied Logic"},{"key":"12_CR18","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"414","DOI":"10.1007\/3-540-45656-2_36","volume-title":"AI 2001: Advances in Artificial Intelligence","author":"M. Reynolds","year":"2001","unstructured":"Reynolds, M.: Continuous temporal models. In: Stumptner, M., Corbett, D., Brooks, M. (eds.) AI 2001. LNCS (LNAI), vol.\u00a02256, pp. 414\u2013425. Springer, Heidelberg (2001)"},{"key":"12_CR19","doi-asserted-by":"crossref","unstructured":"Reynolds, M.: Dense time reasoning via mosaics. In: TIME 2009: Proceedings of the 2009 16th International Symposium on Temporal Representation and Reasoning, pp. 3\u201310. IEEE Computer Society, Washington, DC (2009)","DOI":"10.1109\/TIME.2009.16"},{"key":"12_CR20","first-page":"19","volume":"3","author":"M. Reynolds","year":"2010","unstructured":"Reynolds, M.: The complexity of temporal logics over linear time. Journal of Studies in Logic\u00a03, 19\u201350 (2010)","journal-title":"Journal of Studies in Logic"},{"key":"12_CR21","doi-asserted-by":"crossref","unstructured":"Reynolds, M.: A tableau for until and since over linear time. In: Combi, C., Leucker, M., Wolter, F. (eds.) TIME, pp. 41\u201348. IEEE (2011)","DOI":"10.1109\/TIME.2011.29"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning with Analytic Tableaux and Related Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-40537-2_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,5,17]],"date-time":"2024-05-17T20:18:50Z","timestamp":1715977130000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-40537-2_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642405365","9783642405372"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-40537-2_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}