{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,1]],"date-time":"2026-02-01T20:23:29Z","timestamp":1769977409508,"version":"3.49.0"},"publisher-location":"Cham","reference-count":21,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319671123","type":"print"},{"value":"9783319671130","type":"electronic"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"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":[[2017]]},"DOI":"10.1007\/978-3-319-67113-0_3","type":"book-chapter","created":{"date-parts":[[2017,8,24]],"date-time":"2017-08-24T00:21:24Z","timestamp":1503534084000},"page":"34-48","source":"Crossref","is-referenced-by-count":2,"title":["Query Checking for Linear Temporal Logic"],"prefix":"10.1007","author":[{"given":"Samuel","family":"Huang","sequence":"first","affiliation":[]},{"given":"Rance","family":"Cleaveland","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,8,25]]},"reference":[{"key":"3_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-16612-9_1","volume-title":"Runtime Verification","author":"C Ackermann","year":"2010","unstructured":"Ackermann, C., Cleaveland, R., Huang, S., Ray, A., Shelton, C., Latronico, E.: Automatic requirement extraction from test cases. In: Barringer, H., et al. (eds.) RV 2010. LNCS, vol. 6418, pp. 1\u201315. Springer, Heidelberg (2010). doi:\n10.1007\/978-3-642-16612-9_1"},{"key":"3_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"296","DOI":"10.1007\/3-540-46002-0_21","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R Armoni","year":"2002","unstructured":"Armoni, R., et al.: The ForSpec temporal logic: a new temporal property-specification language. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 296\u2013311. Springer, Heidelberg (2002). doi:\n10.1007\/3-540-46002-0_21"},{"key":"3_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1007\/978-3-642-28756-5_8","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T Babiak","year":"2012","unstructured":"Babiak, T., K\u0159et\u00ednsk\u00fd, M., \u0158eh\u00e1k, V., Strej\u010dek, J.: LTL to B\u00fcchi automata translation: fast and more deterministic. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 95\u2013109. Springer, Heidelberg (2012). doi:\n10.1007\/978-3-642-28756-5_8"},{"key":"3_CR4","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"3_CR5","doi-asserted-by":"crossref","unstructured":"Bruns, G., Godefroid, P.: Temporal logic query checking. In: 16th Annual IEEE Symposium on Logic in Computer Science, pp. 409\u2013417. IEEE, June 2001","DOI":"10.1109\/LICS.2001.932516"},{"key":"3_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"450","DOI":"10.1007\/10722167_34","volume-title":"Computer Aided Verification","author":"W Chan","year":"2000","unstructured":"Chan, W.: Temporal-logic queries. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 450\u2013463. Springer, Heidelberg (2000). doi:\n10.1007\/10722167_34"},{"key":"3_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1007\/978-3-642-19583-9_11","volume-title":"Hardware and Software: Verification and Testing","author":"H Chockler","year":"2011","unstructured":"Chockler, H., Gurfinkel, A., Strichman, O.: Variants of LTL Query Checking. In: Barner, S., Harris, I., Kroening, D., Raz, O. (eds.) HVC 2010. LNCS, vol. 6504, pp. 76\u201392. Springer, Heidelberg (2011). doi:\n10.1007\/978-3-642-19583-9_11"},{"key":"3_CR8","volume-title":"Model Checking","author":"EM Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"3_CR9","doi-asserted-by":"crossref","unstructured":"Emerson, E.A.: Temporal and modal logic. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, vol. B, pp. 995\u20131072. MIT Press (1990)","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"issue":"1","key":"3_CR10","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. JACM 33(1), 151\u2013178 (1986)","journal-title":"JACM"},{"issue":"1\u20133","key":"3_CR11","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1016\/j.scico.2007.01.015","volume":"69","author":"MD Ernst","year":"2007","unstructured":"Ernst, M.D., Perkins, J.H., Guo, P.J., McCamant, S., Pacheco, C., Tschantz, M.S., Xiao, C.: The Daikon system for dynamic detection of likely invariants. Sci. Comput. Program. 69(1\u20133), 35\u201345 (2007)","journal-title":"Sci. Comput. Program."},{"key":"3_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1007\/3-540-44618-4_13","volume-title":"CONCUR 2000 \u2014 Concurrency Theory","author":"K Etessami","year":"2000","unstructured":"Etessami, K., Holzmann, G.J.: Optimizing B\u00fcchi automata. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 153\u2013168. Springer, Heidelberg (2000). doi:\n10.1007\/3-540-44618-4_13"},{"key":"3_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/3-540-44585-4_6","volume-title":"Computer Aided Verification","author":"P Gastin","year":"2001","unstructured":"Gastin, P., Oddoux, D.: Fast LTL to B\u00fcchi automata translation. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 53\u201365. Springer, Heidelberg (2001). doi:\n10.1007\/3-540-44585-4_6"},{"key":"3_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"308","DOI":"10.1007\/3-540-36135-9_20","volume-title":"Formal Techniques for Networked and Distributed Sytems \u2014 FORTE 2002","author":"D Giannakopoulou","year":"2002","unstructured":"Giannakopoulou, D., Lerda, F.: From states to transitions: improving translation of LTL formulae to B\u00fcchi automata. In: Peled, D.A., Vardi, M.Y. (eds.) FORTE 2002. LNCS, vol. 2529, pp. 308\u2013326. Springer, Heidelberg (2002). doi:\n10.1007\/3-540-36135-9_20"},{"issue":"10","key":"3_CR15","doi-asserted-by":"crossref","first-page":"898","DOI":"10.1109\/TSE.2003.1237171","volume":"29","author":"A Gurfinkel","year":"2003","unstructured":"Gurfinkel, A., Chechik, M., Devereux, B.: Temporal logic query checking: a tool for model exploration. IEEE Trans. Soft. Eng. 29(10), 898\u2013914 (2003)","journal-title":"IEEE Trans. Soft. Eng."},{"key":"3_CR16","doi-asserted-by":"crossref","unstructured":"Lemieux, C., Park, D., Beschastnikh, I.: General LTL specification mining. In: 30th IEEE\/ACM International Conference on Automated Software Engineering, pp. 81\u201392. IEEE, Lincoln, November 2015","DOI":"10.1109\/ASE.2015.71"},{"key":"3_CR17","doi-asserted-by":"crossref","unstructured":"Li, W., Forin, A., Seshia, S.A.: Scalable specification mining for verification and diagnosis. In: 47th Design Automation Conference, pp. 755\u2013760. ACM, Anaheim, June 2010","DOI":"10.1145\/1837274.1837466"},{"issue":"5","key":"3_CR18","doi-asserted-by":"crossref","first-page":"651","DOI":"10.1109\/TSE.2008.63","volume":"34","author":"S Shoham","year":"2008","unstructured":"Shoham, S., Yahav, E., Fink, S.J., Pistoia, M.: Static specification mining using automata-based abstractions. IEEE Trans. Soft. Eng. 34(5), 651\u2013666 (2008)","journal-title":"IEEE Trans. Soft. Eng."},{"key":"3_CR19","unstructured":"Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: First Symposium on Logic in Computer Science, pp. 322\u2013331. IEEE Computer Society, Boston, June 1986"},{"issue":"5","key":"3_CR20","first-page":"689","volume":"3","author":"K Winter","year":"1997","unstructured":"Winter, K.: Model checking for abstract state machines. J. Univ. Comput. Sci. 3(5), 689\u2013701 (1997)","journal-title":"J. Univ. Comput. Sci."},{"key":"3_CR21","doi-asserted-by":"crossref","unstructured":"Zhang, D., Cleaveland, R.: Efficient temporal-logic query checking for Presburger systems. In: 20th IEEE\/ACM International Conference on Automated Software Engineering, pp. 24\u201333. ACM, Long Beach, November 2005","DOI":"10.1145\/1101908.1101915"}],"container-title":["Lecture Notes in Computer Science","Critical Systems: Formal Methods and Automated Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-67113-0_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,10,19]],"date-time":"2017-10-19T02:35:01Z","timestamp":1508380501000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-67113-0_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319671123","9783319671130"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-67113-0_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]}}}