{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T17:08:40Z","timestamp":1760202520546,"version":"3.41.0"},"reference-count":52,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2005,4,1]],"date-time":"2005-04-01T00:00:00Z","timestamp":1112313600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2005,4]]},"abstract":"<jats:p>Model checking is a method for the verification of systems with respect to their specifications. Symbolic model-checking, which enables the verification of large systems, proceeds by calculating fixed-point expressions over the system's set of states. The \u03bc-calculus is a branching-time temporal logic with fixed-point operators. As such, it is a convenient logic for symbolic model-checking tools. In particular, the alternation-free fragment of \u03bc-calculus has a restricted syntax, making the symbolic evaluation of its formulas computationally easy. Formally, it takes time that is linear in the size of the system. On the other hand, specifiers find the \u03bc-calculus inconvenient. In addition, specifiers often prefer to use linear-time formalisms. Such formalisms, however, cannot in general be translated to the alternation-free \u03bc-calculus, and their symbolic evaluation involves nesting of fixed-points, resulting in time complexity that is quadratic in the size of the system. In this article, we characterize linear-time properties that can be specified in the alternation-free \u03bc-calculus. We show that a linear-time property can be specified in the alternation-free \u03bc-calculus iff it can be recognized by a deterministic B\u00fcchi automaton. We study the problem of deciding whether a linear-time property, specified by either an automaton or an LTL formula, can be translated to an alternation-free \u03bc-calculus formula, and describe the translation, when possible.<\/jats:p>","DOI":"10.1145\/1055686.1055689","type":"journal-article","created":{"date-parts":[[2005,8,3]],"date-time":"2005-08-03T08:30:55Z","timestamp":1123057855000},"page":"273-294","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":28,"title":["From linear time to branching time"],"prefix":"10.1145","volume":"6","author":[{"given":"Orna","family":"Kupferman","sequence":"first","affiliation":[{"name":"Hebrew University, Jerusalem, Israel"}]},{"given":"Moshe Y.","family":"Vardi","sequence":"additional","affiliation":[{"name":"Rice University, Houston, TX"}]}],"member":"320","published-online":{"date-parts":[[2005,4]]},"reference":[{"key":"e_1_2_1_1_1","unstructured":"Arnold A. and Niwi\u0144ski D. 1992. Fixed point characterization of weak monadic logic definable sets of trees. In Tree Automata and Languages M. Nivat and A. Podelski Eds. Elsevier Amsterdam The Netherlands 159--188.]]  Arnold A. and Niwi\u0144ski D. 1992. Fixed point characterization of weak monadic logic definable sets of trees. In Tree Automata and Languages M. Nivat and A. Podelski Eds. Elsevier Amsterdam The Netherlands 159--188.]]"},{"volume-title":"Proceedings of the 11th IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press, Los Alamitos, Calif., 304--312","author":"Bhat G.","key":"e_1_2_1_2_1"},{"volume":"1633","volume-title":"Proceedings of the 11th International Conference. Lecture Notes in Computer Science","author":"Bloem R.","key":"e_1_2_1_3_1"},{"volume":"1102","volume-title":"Proceedings of the 8th International Conference. Lecture Notes in Computer Science","author":"Brayton R.","key":"e_1_2_1_4_1"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1986.1676819"},{"volume-title":"Proceedings of the International Congress on Logic, Method, and Philosophy of Science","year":"1962","author":"B\u00fcchi J.","key":"e_1_2_1_6_1"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(92)90017-A"},{"key":"e_1_2_1_8_1","unstructured":"Cadence. SMV. http:\/\/www.cadence.com\/company\/cadence_labs_research.html.]]  Cadence. SMV. http:\/\/www.cadence.com\/company\/cadence_labs_research.html.]]"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/322234.322243"},{"volume":"354","volume-title":"Proceedings of the Workshop on Linear Time, Branching Time, and Partial Order in Logics and Models for Concurrency, J. de Bakker, W. de Roever, and G. Rozenberg, Eds. Lecture Notes in Computer Science","author":"Clarke E.","key":"e_1_2_1_10_1"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/5397.5399"},{"key":"e_1_2_1_12_1","unstructured":"Clarke E. Grumberg O. and Peled D. 1999. Model Checking. MIT Press.]]   Clarke E. Grumberg O. and Peled D. 1999. Model Checking. MIT Press.]]"},{"volume":"575","volume-title":"Proceedings of the 3rd International Conference on Computer-Aided Verification. Lecture Notes in Computer Science","author":"Cleaveland R.","key":"e_1_2_1_13_1"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/4904.4999"},{"volume-title":"Proceedings of the 18th Hawaii International Conference on System Sciences. Western Periodicals Company, North Hollywood, Calif.]]","author":"Emerson E.","key":"e_1_2_1_15_1"},{"volume-title":"Proceedings of the 1st Symposium on Logic in Computer Science","author":"Emerson E.","key":"e_1_2_1_16_1"},{"volume":"267","volume-title":"Proceedings of the 14th International Colloquium on Automata, Languages, and Programming. Lecture Notes in Computer Science","author":"Hafer T.","key":"e_1_2_1_17_1"},{"volume":"1102","volume-title":"Proceedings of the 8th International Conference. Lecture Notes in Computer Science","author":"Hardin R.","key":"e_1_2_1_18_1"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008727508722"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.588521"},{"volume-title":"Proceedings of the 20th International Symposium on Mathematical Foundations of Computer Science. Lecture Notes in Computer Science. Springer-Verlag","author":"Janin D.","key":"e_1_2_1_21_1"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-0000(75)80050-X"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(82)90125-6"},{"volume":"834","volume-title":"Algorithms and Computations. Lecture Notes in Computer Science","author":"Krishnan S.","key":"e_1_2_1_24_1"},{"volume":"900","volume-title":"Symposium on Theoretical Aspects of Computer Science. Lecture Notes in Computer Science","author":"Krishnan S.","key":"e_1_2_1_25_1"},{"volume-title":"Proceedings of the 7th International Conference (Liege). 253--266","author":"Krishnan S.","key":"e_1_2_1_26_1"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/6.4.523"},{"volume-title":"Proceedings of the 11th IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press, Los Alamitos, Calif., 322--333","author":"Kupferman O.","key":"e_1_2_1_28_1"},{"volume-title":"Proceedings of the IFIP Working Conference on Programming Concepts and Methods. Chapman & Hall","author":"Kupferman O.","key":"e_1_2_1_29_1"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/377978.377993"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/333979.333987"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(87)90036-5"},{"key":"e_1_2_1_33_1","doi-asserted-by":"crossref","unstructured":"Kurshan R. 1994. Computer Aided Verification of Coordinating Processes. Princeton University Press Princeton N.J.]]   Kurshan R. 1994. Computer Aided Verification of Coordinating Processes. Princeton University Press Princeton N.J.]]","DOI":"10.1515\/9781400864041"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01691063"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/318593.318622"},{"volume-title":"Proceedings of the 41th Annual Symposium on Foundations of Computer Science. IEEE Computer Society Press, Los Alamitos, Calif., 643--652","year":"2000","author":"Maidl M.","key":"e_1_2_1_36_1"},{"key":"e_1_2_1_37_1","doi-asserted-by":"crossref","unstructured":"McMillan K. 1993. Symbolic Model Checking. Kluwer Academic Publishers.]]   McMillan K. 1993. Symbolic Model Checking. Kluwer Academic Publishers.]]","DOI":"10.1007\/978-1-4615-3190-6"},{"volume-title":"Proceedings of the 13th IEEE Symposium on Switching and Automata Theory. IEEE Computer Society Press, Los Alamitos, Calif., 125--129","author":"Meyer A.","key":"e_1_2_1_38_1"},{"volume":"226","volume-title":"Proceedings of the 13th International Colloquium on Automata, Languages and Programming. Lecture Notes in Computer Science","author":"Muller D.","key":"e_1_2_1_39_1"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90133-2"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(81)90110-9"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)71929-3"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1147\/rd.32.0114"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1988.21948"},{"key":"e_1_2_1_45_1","unstructured":"Safra S. 1989. Complexity of automata on infinite objects. Ph.D. dissertation Weizmann Institute of Science Rehovot Israel.]]  Safra S. 1989. Complexity of automata on infinite objects. Ph.D. dissertation Weizmann Institute of Science Rehovot Israel.]]"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/129712.129739"},{"volume-title":"Proceedings of IFIP Conference on Computer Hardware Description Languages and Applications","year":"1997","author":"Schneider K.","key":"e_1_2_1_47_1"},{"key":"e_1_2_1_48_1","doi-asserted-by":"crossref","unstructured":"Thomas W. 1990. Automata on infinite objects. Hand. Theoret. Comput. Sci. 165--191.]]   Thomas W. 1990. Automata on infinite objects. Hand. Theoret. Comput. Sci. 165--191.]]","DOI":"10.1016\/B978-0-444-88074-1.50009-3"},{"volume-title":"Proceedings of the 1st Symposium on Logic in Computer Science","author":"Vardi M.","key":"e_1_2_1_49_1"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1092"},{"key":"e_1_2_1_51_1","volume-title":"Proceedings of the 19th Conference on Foundations of Software Technology and Theoretical Computer Science, C. P. Ragan, V. Raman, and R. Ramanujam, Eds. Lecture Notes in Computer Science","volume":"1738","author":"Wilke T.","year":"1999"},{"key":"e_1_2_1_52_1","unstructured":"Wolper P. 1982. Synthesis of communicating processes from temporal logic specifications. Ph.D. dissertation Stanford University Stanford Calif.]]   Wolper P. 1982. Synthesis of communicating processes from temporal logic specifications. Ph.D. dissertation Stanford University Stanford Calif.]]"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1055686.1055689","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1055686.1055689","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T16:31:28Z","timestamp":1750264288000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1055686.1055689"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,4]]},"references-count":52,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2005,4]]}},"alternative-id":["10.1145\/1055686.1055689"],"URL":"https:\/\/doi.org\/10.1145\/1055686.1055689","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2005,4]]},"assertion":[{"value":"2005-04-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}