{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,6]],"date-time":"2025-08-06T13:18:06Z","timestamp":1754486286831},"publisher-location":"Berlin\/Heidelberg","reference-count":20,"publisher":"Springer-Verlag","isbn-type":[{"type":"print","value":"354058241X"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0013988","type":"book-chapter","created":{"date-parts":[[2005,11,23]],"date-time":"2005-11-23T07:34:32Z","timestamp":1132731272000},"page":"180-194","source":"Crossref","is-referenced-by-count":3,"title":["How linear can branching-time be?"],"prefix":"10.1007","author":[{"given":"Orna","family":"Grumberg","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Robert P.","family":"Kurshan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"12_CR1","doi-asserted-by":"crossref","unstructured":"M. C. Browne, E. M. Clarke, and O. Grumberg. Characterizing finite Kripke structures in propositional temporal logic. Theoretical Computer Science, 59(1\u20132), July 1988.","DOI":"10.1016\/0304-3975(88)90098-9"},{"key":"12_CR2","doi-asserted-by":"crossref","unstructured":"E. M. Clarke and I. A. Draghicescu. Expressibility results for linear time and branching time logics. In Linear Time, Branching Time, and Partial Order in Logics and Models for Concurrency, volume 354, pages 428\u2013437. Springer-Verlag: Lecture Notes in Computer Science, 1988.","DOI":"10.1007\/BFb0013029"},{"key":"12_CR3","unstructured":"E. M. Clarke and E. A. Emerson. Synthesis of synchronization skeletons for branching time temporal logic. In Logic of Programs: Workshop, Yorktown Heights, NY, May 1981, volume 131 of Lecture Notes in Computer Science. Springer-Verlag, 1981."},{"key":"12_CR4","doi-asserted-by":"crossref","unstructured":"E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic verification of finitestate concurrent systems using temporal logic specifications. In Proceedings of the Tenth Annual A CM Symposium on Principles of Programming Languages, January 1983.","DOI":"10.1145\/567067.567080"},{"key":"12_CR5","doi-asserted-by":"crossref","unstructured":"E. M. Clarke, O. Grumberg, and D. E. Long. Model checking and abstraction. In Proceedings of the Nineteenth Annual ACM Symposium on Principles of Programming Languages, January 1992.","DOI":"10.1145\/143165.143235"},{"key":"12_CR6","doi-asserted-by":"crossref","unstructured":"D. Dams, O. Grumberg, and R. Gerth. Generation of reduced models for checking fragments of CTL. In C. Courcoubetis, editor, Proceedings of the Fifth Workshop on Computer-Aided Verification, volume 697 of Lecture Notes in Computer Science. Springer-Verlag, July 1993.","DOI":"10.1007\/3-540-56922-7_39"},{"key":"12_CR7","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1145\/4904.4999","volume":"33","author":"E. A. Emerson","year":"1986","unstructured":"E. A. Emerson and J. Y. Halpern. \u201cSometimes\u201d and \u201cNot Never\u201d revisited: On branching time versus linear time. Journal of the ACM, 33:151\u2013178, 1986.","journal-title":"Journal of the ACM"},{"key":"12_CR8","unstructured":"E. A. Emerson and C.-L. Lei. Modalities for model checking: Branching time strikes back. In POPL85 [17]."},{"key":"12_CR9","unstructured":"O. Grumberg and D. E. Long. Model checking and modular verification. To appear in ACM Transactions on Programming Languages and Systems."},{"key":"12_CR10","unstructured":"Z. Har'El and R. P. Kurshan. The COSPAN user's guide. Technical Report 11211-871009-21TM, AT & T Bell Laboratories, 1987."},{"issue":"1","key":"12_CR11","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1002\/j.1538-7305.1990.tb00102.x","volume":"69","author":"Z. Har'El","year":"1990","unstructured":"Z. Har'El and R. P. Kurshan. Software for analytical development of communications protocols. AT & T Technical Journal, 69(1):45\u201359, Jan.\u2013Feb. 1990.","journal-title":"AT & T Technical Journal"},{"key":"12_CR12","unstructured":"R. P. Kurshan. Analysis of discrete event coordination. In J. W. de Bakker, W.-P. de Roever, and G. Rozenberg, editors, Proceedings of the REX Workshop on Stepwise Refinement of Distributed Systems, Models, Formalisms, Correctness, volume 430 of Lecture Notes in Computer Science. Springer-Verlag, May 1989."},{"key":"12_CR13","doi-asserted-by":"crossref","unstructured":"O. Lichtenstein and A. Pnueli. Checking that finite state concurrent programs satisfy their linear specification. In POPL85 [17].","DOI":"10.1145\/318593.318622"},{"key":"12_CR14","unstructured":"R. Milner. An algebraic definition of simulation between programs. In Proceedings of the Second International Joint Conference on Artificial Intelligence, September 1971."},{"key":"12_CR15","doi-asserted-by":"crossref","unstructured":"R. Milner. A Calculus of Communicating Systems, volume 92 of Lecture Notes in Computer Science. Springer-Verlag, 1980.","DOI":"10.1007\/3-540-10235-3"},{"key":"12_CR16","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1016\/0304-3975(81)90110-9","volume":"13","author":"A. Pnueli","year":"1981","unstructured":"A. Pnueli. A temporal logic of concurrent programs. Theoretical Computer Science, 13:45\u201360, 1981.","journal-title":"Theoretical Computer Science"},{"key":"12_CR17","unstructured":"Proceedings of the Twelfth Annual ACM Symposium on Principles of Programming Languages, January 1985."},{"key":"12_CR18","doi-asserted-by":"crossref","unstructured":"J.P. Quielle and J. Sifakis. Specification and verification of concurrent systems in CESAR. In Proceedings of the Fifth International Symposium in Programming, 1981.","DOI":"10.1007\/3-540-11494-7_22"},{"key":"12_CR19","unstructured":"G. Shurek and O. Grumberg. The modular framework of computer-aided verification: Motivation, solutions and evaluation criteria. In R. P. Kurshan and E. M. Clarke, editors, Proceedings of the 1990 Workshop on Computer-Aided Verification, June 1990."},{"key":"12_CR20","unstructured":"M. Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In Proceedings of the First Annual Symposium on Logic in Computer Science. IEEE Computer Society Press, June 1986."}],"container-title":["Lecture Notes in Computer Science","Temporal Logic"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/www.springerlink.com\/index\/pdf\/10.1007\/BFb0013988","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,11]],"date-time":"2020-04-11T04:35:26Z","timestamp":1586579726000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0013988"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["354058241X"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/bfb0013988","relation":{},"subject":[]}}