{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T15:40:54Z","timestamp":1725550854185},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540008989"},{"type":"electronic","value":"9783540365778"}],"license":[{"start":{"date-parts":[[2003,1,1]],"date-time":"2003-01-01T00:00:00Z","timestamp":1041379200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/3-540-36577-x_6","type":"book-chapter","created":{"date-parts":[[2010,3,29]],"date-time":"2010-03-29T17:12:04Z","timestamp":1269882724000},"page":"65-80","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":22,"title":["Resets vs. Aborts in Linear Temporal Logic"],"prefix":"10.1007","author":[{"given":"Roy","family":"Armoni","sequence":"first","affiliation":[]},{"given":"Doron","family":"Bustan","sequence":"additional","affiliation":[]},{"given":"Orna","family":"Kupferman","sequence":"additional","affiliation":[]},{"given":"MosheY.","family":"Vardi","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2003,2,28]]},"reference":[{"key":"6_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"296","DOI":"10.1007\/3-540-46002-0_21","volume-title":"The ForSpec temporal language: A new temporal property-specification language","author":"R. Armoni","year":"2002","unstructured":"R. Armoni, L. Fix, R. Gerth, B. Ginsburg, T. Kanza, A. Landver, S. Mador-Haim, A. Tiemeyer, E. Singerman, M.Y. Vardi, and Y. Zbar. The ForSpec temporal language: A new temporal property-specification language. In Proc. 8th Int\u2019l Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201902), Lecture Notes in Computer Science 2280, pages 296\u2013311. Springer-Verlag, 2002."},{"key":"6_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"363","DOI":"10.1007\/3-540-44585-4_33","volume-title":"The temporal logic sugar","author":"I. Beer","year":"2001","unstructured":"I. Beer, S. Ben-David, C. Eisner, D. Fisman, A. Gringauze, and Y. Rodeh. The temporal logic sugar. In Proc. Conf. on Computer-Aided Verification, LNCS 2102, pages 363\u2013367, 2001."},{"issue":"2","key":"6_CR3","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"J.R. Burch","year":"1992","unstructured":"J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and L.J. Hwang. Symbolic model checking: 1020 states and beyond. Information and Computation, 98(2):142\u2013170, June 1992.","journal-title":"Information and Computation"},{"key":"6_CR4","doi-asserted-by":"crossref","unstructured":"R. Gerth, D. Peled, M.Y. Vardi, and P. Wolper. Simple on-the-fly automatic verification of linear temporal logic. In P. Dembiski and M. Sredniawa, editors, Protocol Specification, Testing, and Verification, pages 3\u201318. Chapman & Hall, August 1995.","DOI":"10.1007\/978-0-387-34892-6_1"},{"key":"6_CR5","doi-asserted-by":"crossref","unstructured":"S.M. Nowick K. van Berkel, M.B. Josephs. Applications of asynchronous circuits. Proceedings of the IEEE, 1999. special issue on asynchronous circuits & systems.","DOI":"10.1109\/5.740016"},{"issue":"3","key":"6_CR6","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1023\/A:1011254632723","volume":"19","author":"O. Kupferman","year":"2001","unstructured":"O. Kupferman and M.Y. Vardi. Model checking of safety properties. Formal methods in System Design, 19(3):291\u2013314, November 2001.","journal-title":"Formal methods in System Design"},{"key":"6_CR7","doi-asserted-by":"crossref","unstructured":"R.P. Kurshan. Formal verification in a commercial setting. In Proc. Conf. on Design Automation (DAC\u201997), volume 34, pages 258\u2013262, 1997.","DOI":"10.1145\/266021.266089"},{"key":"6_CR8","unstructured":"R.P. Kurshan. FormalCheck User\u2019s Manual. Cadence Design, Inc., 1998."},{"key":"6_CR9","first-page":"35","volume":"19","author":"H.R. Lewis","year":"1978","unstructured":"H.R. Lewis. Complexity of solvable cases of the decision problem for the predicate calculus. In Foundations of Computer Science, volume 19, pages 35\u201347, 1978.","journal-title":"Foundations of Computer Science"},{"key":"6_CR10","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1016\/0304-3975(84)90049-5","volume":"32","author":"S. Miyano","year":"1984","unstructured":"S. Miyano and T. Hayashi. Alternating finite automata on \u03c9-words. Theoretical Computer Science, 32:321\u2013330, 1984.","journal-title":"Theoretical Computer Science"},{"key":"6_CR11","unstructured":"M.J. Morley. Semantics of temporal e. In T. F. Melham and F.G. Moller, editors, Banff\u201999 Higher Order Workshop (Formal Methods in Computation). University of Glasgow, Department of Computing Science Technical Report, 1999."},{"key":"6_CR12","series-title":"Lect Notes Comput Sci","volume-title":"Alternating automata, the weak monadic theory of the tree and its complexity","author":"D.E. Muller","year":"1986","unstructured":"D.E. Muller, A. Saoudi, and P.E. Schupp. Alternating automata, the weak monadic theory of the tree and its complexity. In Proc. 13th Int. Colloquium on Automata, Languages and Programming, LNCS 226, 1986."},{"key":"6_CR13","doi-asserted-by":"crossref","unstructured":"A. Pnueli. The temporal logic of programs. In Proc. 18th IEEE Symp. on Foundation of Computer Science, pages 46\u201357, 1977.","DOI":"10.1109\/SFCS.1977.32"},{"key":"6_CR14","doi-asserted-by":"publisher","first-page":"733","DOI":"10.1145\/3828.3837","volume":"32","author":"A.P. Sistla","year":"1985","unstructured":"A.P. Sistla and E.M. Clarke. The complexity of propositional linear temporal logic. Journal ACM, 32:733\u2013749, 1985.","journal-title":"Journal ACM"},{"key":"6_CR15","unstructured":"A comparison of reset control methods: Application note 11. http:\/\/www.summitmicro.com\/tech_support\/notes\/note11.htm , Summit Microelectronics, Inc., 1999."},{"key":"6_CR16","first-page":"261","volume":"48","author":"W. Thomas","year":"1981","unstructured":"W. Thomas. A combinatorial approach to the theory of \u03c9-automata. Information and Computation, 48:261\u2013283, 1981.","journal-title":"Information and Computation"},{"key":"6_CR17","doi-asserted-by":"crossref","unstructured":"P. van Emde Boas. The convenience of tilings. In Complexity, Logic and Recursion Theory, volume 187 of Lecture Notes in Pure and Applied Mathetaics, pages 331\u2013363, 1997.","DOI":"10.1201\/9780429187490-12"},{"key":"6_CR18","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"238","DOI":"10.1007\/3-540-60915-6_6","volume-title":"Logics for Concurrency: Structure versus Automata","author":"M.Y. Vardi","year":"1996","unstructured":"M.Y. Vardi. An automata-theoretic approach to linear temporal logic. In Logics for Concurrency: Structure versus Automata, LNCS 1043, pages 238\u2013266, 1996."},{"key":"6_CR19","unstructured":"M.Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In Proc. 1st Symp. on Logic in Computer Science, pages 332\u2013344, 1986."},{"issue":"2","key":"6_CR20","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1016\/0022-0000(86)90026-7","volume":"32","author":"M.Y. Vardi","year":"1986","unstructured":"M.Y. Vardi and P. Wolper. Automata-theoretic techniques for modal logics of programs. Journal of Computer and System Science, 32(2):182\u2013221, April 1986.","journal-title":"Journal of Computer and System Science"},{"issue":"1","key":"6_CR21","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1994.1092","volume":"115","author":"M.Y. Vardi","year":"1994","unstructured":"M.Y. Vardi and P. Wolper. Reasoning about infinite computations. Information and Computation, 115(1):1\u201337, November 1994.","journal-title":"Information and Computation"},{"key":"6_CR22","unstructured":"H. Wang. Dominoes and the aea case of the decision problem. In Symposium on the Mathematical Theory of Automata, pages 23\u201355, 1962."}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-36577-X_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,6,3]],"date-time":"2020-06-03T06:16:12Z","timestamp":1591164972000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-36577-X_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540008989","9783540365778"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/3-540-36577-x_6","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2003]]},"assertion":[{"value":"28 February 2003","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}