{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T13:35:20Z","timestamp":1770298520971,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540434191","type":"print"},{"value":"9783540460022","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-46002-0_21","type":"book-chapter","created":{"date-parts":[[2007,10,28]],"date-time":"2007-10-28T02:29:59Z","timestamp":1193538599000},"page":"296-311","source":"Crossref","is-referenced-by-count":99,"title":["The ForSpec Temporal Logic: A New Temporal Property-Specification Language"],"prefix":"10.1007","author":[{"given":"Roy","family":"Armoni","sequence":"first","affiliation":[]},{"given":"Limor","family":"Fix","sequence":"additional","affiliation":[]},{"given":"Alon","family":"Flaisher","sequence":"additional","affiliation":[]},{"given":"Rob","family":"Gerth","sequence":"additional","affiliation":[]},{"given":"Boris","family":"Ginsburg","sequence":"additional","affiliation":[]},{"given":"Tomer","family":"Kanza","sequence":"additional","affiliation":[]},{"given":"Avner","family":"Landver","sequence":"additional","affiliation":[]},{"given":"Sela","family":"Mador-Haim","sequence":"additional","affiliation":[]},{"given":"Eli","family":"Singerman","sequence":"additional","affiliation":[]},{"given":"Andreas","family":"Tiemeyer","sequence":"additional","affiliation":[]},{"given":"MosheY.","family":"Vardi","sequence":"additional","affiliation":[]},{"given":"Yael","family":"Zbar","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,3,14]]},"reference":[{"key":"21_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"74","DOI":"10.1007\/BFb0031988","volume-title":"Real Time: Theory in Practice","author":"R. Alur","year":"1992","unstructured":"R. Alur and T.A. Henzinger. Logics and models of real time: a survey. In J.W.de Bakker, K. Huizing, W.-P. de Roever, and G. Rozenberg, editors, Real Time: Theory in Practice, Lecture Notes in Computer Science 600, pages 74\u2013106. Springer-Verlag, 1992."},{"key":"21_CR2","series-title":"Lect Notes Comput Sci","first-page":"62","volume-title":"Temporal Logic in Specification","author":"B. Banieqbal","year":"1987","unstructured":"B. Banieqbal and H. Barringer. Temporal logic with fixed points. In B. Banieqbal, H. Barringer, and A. Pnueli, editors, Temporal Logic in Specification, volume 398 of Lecture Notes in Computer Science, pages 62\u201374. Springer-Verlag, 1987."},{"key":"21_CR3","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 (CAV\u201900), volume 2102 of Lecture Notes in Computer Science, pages 363\u2013367. Springer-Verlag, 2001."},{"key":"21_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"184","DOI":"10.1007\/BFb0028744","volume-title":"On-the-fly model checking of RCTL formulas","author":"I. Beer","year":"1998","unstructured":"I. Beer, S. Ben-David, and A. Landver. On-the-fly model checking of RCTL formulas. In Computer Aided Verification, Proc. 10th International Conference, volume 1427 of Lecture Notes in Computer Science, pages 184\u2013194. Springer-Verlag, 1998."},{"issue":"4","key":"21_CR5","doi-asserted-by":"publisher","first-page":"410","DOI":"10.1007\/s100090050046","volume":"2","author":"A. Cimatti","year":"2000","unstructured":"A. Cimatti, E.M. Clarke, F. Giunchiglia, and M. Roveri. Nusmv: a new symbolic model checker. It\u2019l J. on Software Tools for Technology Transfer, 2(4):410\u2013425, 2000.","journal-title":"It\u2019l J. on Software Tools for Technology Transfer"},{"key":"21_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"166","DOI":"10.1007\/3-540-63141-0_12","volume-title":"An algebraic theory of multiple clocks","author":"R. Cleaveland","year":"1997","unstructured":"R. Cleaveland, G. Luttgen, and M. Mendler. An algebraic theory of multiple clocks. In Proc. 8th Int\u2019l Conf. on Concurrency Theory (CONCUR\u201997), volume 1243 of Lecture Notes in Computer Science, pages 166\u2013180. Springer-Verlag, 1998."},{"key":"21_CR7","first-page":"997","volume-title":"Handbook of Theoretical Computer Science","author":"E.A. Emerson","year":"1990","unstructured":"E.A. Emerson. Temporal and modal logic. In J. Van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, chapter 16, pages 997\u20131072. Elsevier, MIT press, 1990."},{"key":"21_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1007\/BFb0030596","volume-title":"Generalized quantitative temporal reasoning: An automata theoretic","author":"E.A. Emerson","year":"1997","unstructured":"E.A. Emerson and R.J. Trefler. Generalized quantitative temporal reasoning: An automata theoretic. In Proc. Theory and Practice of Software Development (TAPSOFT), volume 1214 of Lecture Notes in Computer Science, pages 189\u2013200. Springer-Verlag, 1997."},{"key":"21_CR9","series-title":"Lect Notes Comput Sci","volume-title":"Tools and algorithms for the construction and analysis of systems","author":"B. Finkbeiner","year":"2001","unstructured":"B. Finkbeiner. Symbolic refinement checking with nondeterministic BDDs. In Tools and algorithms for the construction and analysis of systems, Lecture Notes in Computer Science. Springer-Verlag, 2001."},{"key":"21_CR10","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1016\/0022-0000(79)90046-1","volume":"18","author":"M.J. Fischer","year":"1979","unstructured":"M.J. Fischer and R.E. Ladner. Propositional dynamic logic of regular programs. Journal of Computer and Systems Sciences, 18:194\u2013211, 1979.","journal-title":"Journal of Computer and Systems Sciences"},{"issue":"1","key":"21_CR11","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1016\/S0168-0072(98)00039-6","volume":"96","author":"J.G. Henriksen","year":"1999","unstructured":"J.G. Henriksen and P.S. Thiagarajan. Dynamic linear time temporal logic. Annals of Pure and Applied Logic, 96(1\u20133):187\u2013207, 1999.","journal-title":"Annals of Pure and Applied Logic"},{"key":"21_CR12","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","volume":"27","author":"D. Kozen","year":"1983","unstructured":"D. Kozen. Results on the propositional \u03bc-calculus. Theoretical Computer Science, 27:333\u2013354, 1983.","journal-title":"Theoretical Computer Science"},{"key":"21_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"519","DOI":"10.1007\/3-540-44685-0_35","volume-title":"Extended temporal logic revisited","author":"O. Kupferman","year":"2001","unstructured":"O. Kupferman, N. Piterman, and M.Y. Vardi. Extended temporal logic revisited. In Proc. 12th International Conference on Concurrency Theory, volume 2154 of Lecture Notes in Computer Science, pages 519\u2013535, August 2001."},{"key":"21_CR14","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":"21_CR15","unstructured":"R.P. Kurshan. FormalCheck User\u2019s Manual. Cadence Design, Inc., 1998."},{"issue":"3","key":"21_CR16","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":"21_CR17","doi-asserted-by":"publisher","first-page":"377","DOI":"10.1016\/S0304-3975(99)00008-0","volume":"220","author":"C. Liu","year":"1999","unstructured":"C. Liu and M.A. Orgun. Verification of reactive systems using temporal logics with clocks. Theoretical Computer Science, 220:377\u2013408, 1999.","journal-title":"Theoretical Computer Science"},{"key":"21_CR18","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"196","DOI":"10.1007\/3-540-15648-8_16","volume-title":"Logics of Programs","author":"O. Lichtenstein","year":"1985","unstructured":"O. Lichtenstein, A. Pnueli, and L. Zuck. The glory of the past. In Logics of Programs, volume 193 of Lecture Notes in Computer Science, pages 196\u2013218, Brooklyn, June 1985. Springer-Verlag."},{"key":"21_CR19","unstructured":"M.J. Morley. Semantics of temporal e. In T. F. Melham and F.G. Moller, editors, Banff\u201999 Higher OrderWorkshop (Formal Methods in Computation). University of Glasgow, Department of Computing Science Technical Report, 1999."},{"key":"21_CR20","doi-asserted-by":"crossref","unstructured":"A. Pnueli. In transition from global to modular temporal reasoning about programs. In K. Apt, editor, Logics and Models of Concurrent Systems, volume F-13 of NATO Advanced Summer Institutes, pages 123\u2013144. Springer-Verlag, 1985.","DOI":"10.1007\/978-3-642-82453-1_5"},{"key":"21_CR21","doi-asserted-by":"crossref","unstructured":"T. Schlipf, T. Buechner, R. Fritz, M. Helms, and J. Koehl. Formal verification made easy. IBM Journal of Research and Development, 41(4:5), 1997.","DOI":"10.1147\/rd.414.0567"},{"key":"21_CR22","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1016\/0304-3975(87)90008-9","volume":"49","author":"A.P. Sistla","year":"1987","unstructured":"A.P. Sistla, M.Y. Vardi, and P. Wolper. The complementation problem for B\u00fcchi automata with applications to temporal logic. Theoretical Computer Science, 49:217\u2013237, 1987.","journal-title":"Theoretical Computer Science"},{"key":"21_CR23","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 F. Moller and G. Birtwistle, editors, Logics for Concurrency: Structure versus Automata, volume 1043 of Lecture Notes in Computer Science, pages 238\u2013266. Springer-Verlag, Berlin, 1996."},{"key":"21_CR24","series-title":"Lect Notes Comput Sci","first-page":"1","volume-title":"Branching vs. linear time: Final showdown","author":"M.Y. Vardi","year":"2001","unstructured":"M.Y. Vardi. Branching vs. linear time: Final showdown. In Proc. Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 2031 of Lecture Notes in Computer Science, pages 1\u201322. Springer-Verlag, 2001."},{"issue":"1","key":"21_CR25","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":"21_CR26","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1016\/S0019-9958(83)80051-5","volume":"56","author":"P. Wolper","year":"1983","unstructured":"P. Wolper. Temporal logic can be more expressive. Information and Control, 56(1\u20132):72\u201399, 1983.","journal-title":"Information and Control"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-46002-0_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,3]],"date-time":"2019-05-03T22:28:44Z","timestamp":1556922524000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-46002-0_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540434191","9783540460022"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/3-540-46002-0_21","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2002]]}}}