{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,12,31]],"date-time":"2024-12-31T05:05:33Z","timestamp":1735621533753,"version":"3.32.0"},"reference-count":27,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[1995,3,1]],"date-time":"1995-03-01T00:00:00Z","timestamp":794016000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Method Syst Des"],"published-print":{"date-parts":[[1995,3]]},"DOI":"10.1007\/bf01383967","type":"journal-article","created":{"date-parts":[[2005,4,2]],"date-time":"2005-04-02T09:32:59Z","timestamp":1112434379000},"page":"191-216","source":"Crossref","is-referenced-by-count":3,"title":["An environment for formal verification based on symbolic computations"],"prefix":"10.1007","volume":"6","author":[{"given":"Ramin","family":"Hojati","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Robert K.","family":"Brayton","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"8","key":"CR1","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"R.E. Bryant","year":"1986","unstructured":"R.E. Bryant, ?Graph Based Algorithms for Boolean Function Manipulation,?IEEE Trans. on Computers, C-35(8):677?691, August 1986.","journal-title":"IEEE Trans. on Computers, C"},{"key":"CR2","doi-asserted-by":"crossref","unstructured":"J.R. Burch, E.M. Clarke, K.L. McMillan, D. Dill, and L.J. Hwang, ?Symbolic Model Checking: 1020 states and beyond?,Information and Computation, June 1992.","DOI":"10.1016\/0890-5401(92)90017-A"},{"key":"CR3","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1016\/S0022-0000(74)80051-6","volume":"8","author":"Y. Choueka","year":"1974","unstructured":"Y. Choueka, ?Theories of Automata on ?-Tapes: A simplified Approach,?Journal of Computer and System Sciences 8, 117?141, 1974.","journal-title":"Journal of Computer and System Sciences"},{"key":"CR4","doi-asserted-by":"crossref","first-page":"301","DOI":"10.1016\/0020-0190(93)90069-L","volume":"46","author":"E.M. Clarke","year":"1993","unstructured":"E.M. Clarke, I.A. Dragnicescu, and R.P. Kurshan, ?A Unified approach for showing language inclusion and equivalence between various types of automata,?Information Processing Letters 46, 301?308, 1993, Elsevier.","journal-title":"Information Processing Letters"},{"issue":"2","key":"CR5","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E.M. Clarke","year":"1986","unstructured":"E.M. Clarke, E.A. Emerson, and A.P. Sistla, ?Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications,?ACM Transactions on Programming Languages and Systems, 8(2), pp. 244?263, 1986.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"CR6","doi-asserted-by":"crossref","unstructured":"E.A. Emerson, ?Temporal and Modal Logic,?Handbook of Theoretical Computer Science, editor J. van Leeuven, Elsevier Science Publishers B.V., pp. 995?1072, 1990.","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"key":"CR7","doi-asserted-by":"crossref","unstructured":"E.A. Emerson, and C.L. Lei, ?Modalities for Model Checking: Branching Time Logic Strikes Back,?12th Annual Symp. on Principles of Programming Languages, 1985.","DOI":"10.1145\/318593.318620"},{"key":"CR8","unstructured":"E.A. Emerson and C.L. Lei, ?Efficient Model Checking in Fragments of the Propositional Mu-Calculus,?Logic in Computer Science, 1987."},{"key":"CR9","doi-asserted-by":"crossref","unstructured":"Z. Har'El and R.P. Kurshan, ?Software for Analytical Development of Communication Protocols,?AT & T Journal, Jan. 1990, 45?59.","DOI":"10.1002\/j.1538-7305.1990.tb00102.x"},{"key":"CR10","doi-asserted-by":"crossref","unstructured":"Ramin Hojati, Herve Touati, Robert P. Kurshan, and Robert K. Brayton, ?Efficient ?-Regular Language Containment,?Computer-Aided Verification, 1992.","DOI":"10.1007\/3-540-56496-9_31"},{"key":"CR11","doi-asserted-by":"crossref","unstructured":"R. Hojati, T.P. Shiple, R.K. Brayton, and R.P. Kurshan, ?A Unified Approach to Language Containment and Fair CTL Model Checking,?Proceedings of Design Automation Conference, June 1993.","DOI":"10.1145\/157485.164985"},{"key":"CR12","doi-asserted-by":"crossref","unstructured":"R. Hojati, R.K. Brayton, and R.P. Kurshan, ?BDD-Based Debugging of Design Using Language Containment and Fair CTL,?Proceedings of the Conference on Computer-Aided Verification, Elounda, Crete, Greece, To appear, June 1993.","DOI":"10.1007\/3-540-56922-7_5"},{"key":"CR13","doi-asserted-by":"crossref","unstructured":"R. Hojati, R.Mueller-Thuns, and R.K. Brayton, ?Improving Language Containment Using Fairness Graphs,?Computer-Aided Verification, 1994.","DOI":"10.1007\/3-540-58179-0_70"},{"key":"CR14","unstructured":"R. Hojati, V. Singhal, and R.K. Brayton, ?Edge-Streett\/Edge-Rabin Automata Environment for Formal Verification Using Language Containment,? Memorandum No. UCB\/ERL M94\/12, UC Berkeley, 1994."},{"key":"CR15","doi-asserted-by":"crossref","unstructured":"A. Aziz, F. Balarin, S.T. Cheng, R. Hojati, T. Kam, S.C. Krishnan, R.K. Ranjan, T.R. Shiple, V. Singhal, S. Tasiran, H.-Y. Wang, R.K. Brayton and A.L. Sangiovanni-Vincentelli, ?HSIS: A BDD-Based Environment for Formal Varification,?Design Automation Conference, 1994.","DOI":"10.1145\/196244.196467"},{"key":"CR16","series-title":"Memorandum No. UCB\/ERL, M90\/125","volume-title":"Electronics Research Laboratory","author":"T. Kam","year":"1990","unstructured":"T. Kam and R. Brayton, ?Multi-valued Decision Diagrams,?Electronics Research Laboratory, University of California, Berkeley, Memorandum No. UCB\/ERL, M90\/125, 1990."},{"key":"CR17","doi-asserted-by":"crossref","first-page":"59","DOI":"10.1016\/0022-0000(87)90036-5","volume":"35","author":"R.P. Kurshan","year":"1987","unstructured":"R.P. Kurshan, ?Complementing Deterministic Buchi Automata in Polynomial Time,?Journal of Computer and System Sciences, Vol. 35, 1987, 59?71.","journal-title":"Journal of Computer and System Sciences"},{"key":"CR18","doi-asserted-by":"crossref","unstructured":"R.P. Kurshan, ?Reducibility in Analysis of Coordination,? inLNCIS, Vol. 103, pp. 19?39, Springer-Verlag, 1987.","DOI":"10.1007\/BFb0042302"},{"key":"CR19","unstructured":"R.P. Kurshan, ?Automata-Theoretic Verification of Coordinating Processes,?UC Berkeley Notes, 1992."},{"key":"CR20","first-page":"19","volume-title":"Regional Conference Series in Mathematics","author":"M.O. Rabin","year":"1972","unstructured":"M.O. Rabin, ?Automata on Infinite Objects and Church's Problem,?Regional Conference Series in Mathematics, Vol. 13, 1972, American Mathematical Society, Providence, Rhode Island, 19?39."},{"key":"CR21","unstructured":"Shmuel Safra, ?Complexity of Automata on Infinite Objects,?The Weizmann Institute of Science, March 1989."},{"key":"CR22","doi-asserted-by":"crossref","unstructured":"S. Safra, ?Exponential Determinization for ?-Automata with Strong-Fairness Acceptance Condition,?STOC, 1992.","DOI":"10.1145\/129712.129739"},{"key":"CR23","doi-asserted-by":"crossref","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 Buchi Automata with applications to Temporal Logic,?Theoretical Computer Science 49, 1987, pp. 217?237.","journal-title":"Theoretical Computer Science"},{"key":"CR24","doi-asserted-by":"crossref","first-page":"121","DOI":"10.1016\/S0019-9958(82)91258-X","volume":"54","author":"R.S. Streett","year":"1982","unstructured":"R.S. Streett, ?Propositional Dynamic Logic of Looping and Converse is Elementary Decidable,?Information and Control, Vol. 54, 1982, 121?141.","journal-title":"Information and Control"},{"key":"CR25","doi-asserted-by":"crossref","unstructured":"H.J. Touati, H. Savoj, B. Lin, R.K. Brayton, and A.S. Vincentelli, ?Implicit State Enumeration of Finite State Machines Using BDDs,?Proc. of the IEEE International Conference on Computer-Aided Design, pp. 130?133, Nov. 1990.","DOI":"10.1109\/ICCAD.1990.129860"},{"key":"CR26","unstructured":"H. Touati, R. Kurshan, and R. Brayton, ?Testing Language Containment of ?-Automata Using BDDs,?International Workshop on Formal Methods in VLSI Design, 1991."},{"key":"CR27","unstructured":"M.Y. Vardi and P.L. Wolper, ?An Automata-Theoretical Approach to Program Verification,?Logic in Computer Science, 332?334, 1986."}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01383967.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01383967\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01383967","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,12,30]],"date-time":"2024-12-30T06:53:17Z","timestamp":1735541597000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF01383967"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995,3]]},"references-count":27,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1995,3]]}},"alternative-id":["BF01383967"],"URL":"https:\/\/doi.org\/10.1007\/bf01383967","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[1995,3]]}}}