{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:28:16Z","timestamp":1761611296848},"publisher-location":"Berlin, Heidelberg","reference-count":35,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540542339"},{"type":"electronic","value":"9783540475163"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1991]]},"DOI":"10.1007\/3-540-54233-7_126","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T22:39:29Z","timestamp":1330209569000},"page":"76-92","source":"Crossref","is-referenced-by-count":39,"title":["Safety for branching time semantics"],"prefix":"10.1007","author":[{"given":"A.","family":"Bouajjani","sequence":"first","affiliation":[]},{"given":"J. C.","family":"Fernandez","sequence":"additional","affiliation":[]},{"given":"S.","family":"Graf","sequence":"additional","affiliation":[]},{"given":"C.","family":"Rodriguez","sequence":"additional","affiliation":[]},{"given":"J.","family":"Sifakis","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,8]]},"reference":[{"key":"6_CR1","unstructured":"M. Abadi and L. Lamport. The existence of refinement mappings. SRC 29, Digital Equipement Corporation, August 1988."},{"key":"6_CR2","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1007\/BF01782772","volume":"2","author":"B. Alpern","year":"1987","unstructured":"B. Alpern and F.B. Schneider. Recognizing safety and liveness. Distributed Computing, 2:117\u2013126, 1987.","journal-title":"Distributed Computing"},{"key":"6_CR3","doi-asserted-by":"crossref","unstructured":"J. A. Bergstra and J.W. Klop. Algebra of communicating processes with abstraction. TCS, 37 (1), 1985.","DOI":"10.1016\/0304-3975(85)90088-X"},{"key":"6_CR4","doi-asserted-by":"crossref","unstructured":"G. Boudol. Notes on algebraic calculi of processes. In Logics and Models for Concurrent Systems, Springer Verlag, 1985. Nato ASI Series F (13).","DOI":"10.1007\/978-3-642-82453-1_9"},{"key":"6_CR5","unstructured":"J.R. B\u00fcchi. On a decision method in restricted second order arithmetic. In Nagel et al., editor, Logic, Methodology and Philosophy of Sciences, Stantford Univ. Press, 1962."},{"key":"6_CR6","doi-asserted-by":"crossref","first-page":"169","DOI":"10.1016\/S0022-0000(77)80004-4","volume":"15","author":"R. Cohen","year":"1977","unstructured":"R. Cohen and A. Gold. Theory of \u03c9-languages. J. Comput. System Sci., 15:169\u2013208, 1977.","journal-title":"J. Comput. System Sci."},{"key":"6_CR7","series-title":"Technical Report","volume-title":"Safety and Liveness of \u03c9-Context-Free Languages","author":"S. Chaudhuri","year":"1989","unstructured":"S. Chaudhuri and R.E. Ladner. Safety and Liveness of \u03c9-Context-Free Languages. Technical Report 88-11-04, Department of Computer Sciences and Engineering, University of Washington, Seatle, Washington, 1989."},{"key":"6_CR8","unstructured":"J. C. Fernandez. Ald\u00e9baran: A tool for verification of communicating processes. Tech. report Spectre C14, LGI-IMAG Grenoble, 1989."},{"key":"6_CR9","unstructured":"J. Fernandez and L. Mounier. Verification bisimulations on the fly. In Proceedings of the Third International Conference on Formal Description Techniques FORTE'90 (Madrid, Spain), pages 91\u2013105, North-Holland, November 1990."},{"key":"6_CR10","volume-title":"An Efficient Algorithm for Branching Bisimulation and Stuttering Equivalence","author":"J. F. Groote","year":"1990","unstructured":"Jan Friso Groote and Frits Vaandrager. An Efficient Algorithm for Branching Bisimulation and Stuttering Equivalence. CS-R 9001, Centrum voor Wiskunde en Informatica, Amsterdam, January 1990."},{"key":"6_CR11","doi-asserted-by":"crossref","unstructured":"R. Hossley and C. Rackoff. The emptiness problem for automata on infinite trees. In Proc. 13th IEEE Symp. on Switching and Automata Theory, 1972.","DOI":"10.1109\/SWAT.1972.28"},{"key":"6_CR12","doi-asserted-by":"crossref","unstructured":"D. Kozen. Results on the propositional \u03bc-calculus. In Theoretical Computer Science, North-Holland, 1983.","DOI":"10.1016\/0304-3975(82)90125-6"},{"issue":"2","key":"6_CR13","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1109\/TSE.1977.229904","volume":"SE-3","author":"L. Lamport","year":"1977","unstructured":"L. Lamport. Proving the correctness of multiprocess programs. IEEE Transactions on Software Engineering, SE-3(2):125\u2013143, 1977.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"6_CR14","unstructured":"L. Lamport. Logical foundation. In M. Paul and H.J. Siegert, editors, Distributed Systems-Methods and Tools for Specification, LNCS 190, Springer Verlag, 1985."},{"key":"6_CR15","doi-asserted-by":"crossref","unstructured":"O. Lichtenstein, A. Pnueli, and L. Zuck. The glory of the past. In Conference on Logics of Programs, LNCS 194, Springer Verlag, 1985.","DOI":"10.1007\/3-540-15648-8_16"},{"key":"6_CR16","unstructured":"R. Milner. An algebraic definition of simulation between programs. In Second Int. Joint Conf. on Artificial Intelligence, BCS, pages 481\u2013489, 1971."},{"key":"6_CR17","doi-asserted-by":"crossref","unstructured":"R. Milner. A calculus of communication systems. In LNCS 92, Springer Verlag, 1980.","DOI":"10.1007\/3-540-10235-3"},{"key":"6_CR18","doi-asserted-by":"crossref","first-page":"227","DOI":"10.1016\/0890-5401(89)90070-9","volume":"81","author":"R. Milner","year":"1989","unstructured":"R. Milner. A complete axiomatization for observational congruence of finite-state behaviours. Information and Computation, 81:227\u2013247, 1989.","journal-title":"Information and Computation"},{"key":"6_CR19","doi-asserted-by":"crossref","unstructured":"Z. Manna and A. Pnueli. Adequate proof principles for invariance and liveness properties of concurrent programs. Science of Computer Programming, 32, 1984.","DOI":"10.1016\/0167-6423(84)90003-0"},{"key":"6_CR20","doi-asserted-by":"crossref","unstructured":"Z. Manna and A. Pnueli. The anchored version of the temporal framework. In J.W. De Bakker, W.P. De Roover, and G. Rozenberg, editors, Linear Time, Branching Time, and Partial Order in Logics and Models for Concurrency, LNCS 354, Springer Verlag, 1989.","DOI":"10.1007\/BFb0013024"},{"key":"6_CR21","doi-asserted-by":"crossref","unstructured":"E.D. Muller. Infinite sequences and finite machines. In 4th IEEE Ann. Symp. on Switching Circuit and Logical Design, pages 3\u201316, 1963.","DOI":"10.1109\/SWCT.1963.8"},{"key":"6_CR22","unstructured":"D. Niwinski. Fixed points vs. infinite generation. In Proc. of Third. Symp. on Logic in Computer Science, Computer Society Press, 1988."},{"key":"6_CR23","doi-asserted-by":"crossref","unstructured":"D. Park. Concurrency and automata on infinite sequences. In 5th GI-Conference on Theorical Computer Science, Springer Verlag, 1981. LNCS 104.","DOI":"10.1007\/BFb0017309"},{"key":"6_CR24","unstructured":"G. D. Plotkin. A structural approach to operational semantics. Lecture Notes, Aarhus University, 1981."},{"key":"6_CR25","doi-asserted-by":"crossref","unstructured":"M.O. Rabin. Decidability of second order theories and automata on infinite trees. Trans. Amer. Math. Soc., 141, 1969.","DOI":"10.2307\/1995086"},{"key":"6_CR26","doi-asserted-by":"crossref","unstructured":"M.O. Rabin. Weakly definable relations and special automata. In Y. Bar Hillel, editor, Proc. Symp. Math. Logic and Foundations of Set Theory, North-Holland, 1970.","DOI":"10.1016\/S0049-237X(08)71929-3"},{"key":"6_CR27","doi-asserted-by":"crossref","unstructured":"M.O. Rabin. Automata on infinite objects and church's problem. In Proc. Regional AMS Conf. Series in Mathematics, 1972.","DOI":"10.1090\/cbms\/013"},{"key":"6_CR28","doi-asserted-by":"crossref","unstructured":"A. Saoudi. Vari\u00e9t\u00e9s d'automates descendants d'arbres infinis. TCS, 43, 1986.","DOI":"10.1016\/0304-3975(86)90183-0"},{"key":"6_CR29","doi-asserted-by":"crossref","unstructured":"A. P. Sistla. On characterization of safety and liveness. In Proc. 4th Symp. Princ. of Dist. Comp., pages 39\u201348, ACM, 1985.","DOI":"10.1145\/323596.323600"},{"key":"6_CR30","doi-asserted-by":"crossref","unstructured":"R.S. Streett. Propositional dynamic logic of looping and converse. Information and Control, 54, 1982.","DOI":"10.1016\/S0019-9958(82)91258-X"},{"key":"6_CR31","doi-asserted-by":"crossref","unstructured":"R.J. van Glabbeek. The Linear Time \u2014 Branching Time Spectrum. Technical Report CS-R9029, Centre for Mathematics and Computer Science, 1990.","DOI":"10.1007\/BFb0039066"},{"key":"6_CR32","volume-title":"Branching time and abstraction in bisimulation semantics (extended abstract)","author":"R.J. Glabbeek van","year":"1989","unstructured":"R.J. van Glabbeek and W.P. Weijland. Branching time and abstraction in bisimulation semantics (extended abstract). CS-R 8911, Centrum voor Wiskunde en Informatica, Amsterdam, 1989."},{"key":"6_CR33","doi-asserted-by":"crossref","unstructured":"M.Y. Vardi and P. Wolper. Automata-theoritic techniques for modal logics of programs. J. Comp. Sys. Sci., 32, 1986.","DOI":"10.1016\/0022-0000(86)90026-7"},{"key":"6_CR34","unstructured":"G. Winskel. Synchronization trees. In J. Diaz, editor, 10th ICALP, LNCS 154, 1983."},{"key":"6_CR35","doi-asserted-by":"crossref","unstructured":"P. Wolper. On the relation of programs and computations to models of temporal logic. In Temporal Logic in Specification, LNCS 398, 1989.","DOI":"10.1007\/3-540-51803-7_23"}],"container-title":["Lecture Notes in Computer Science","Automata, Languages and Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-54233-7_126.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,20]],"date-time":"2023-06-20T18:08:30Z","timestamp":1687284510000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-54233-7_126"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1991]]},"ISBN":["9783540542339","9783540475163"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/3-540-54233-7_126","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1991]]}}}