{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,5]],"date-time":"2022-04-05T11:08:35Z","timestamp":1649156915996},"reference-count":15,"publisher":"Springer Science and Business Media LLC","issue":"6","license":[{"start":{"date-parts":[[2006,11,1]],"date-time":"2006-11-01T00:00:00Z","timestamp":1162339200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Comput Sci Technol"],"published-print":{"date-parts":[[2006,11]]},"DOI":"10.1007\/s11390-006-0944-5","type":"journal-article","created":{"date-parts":[[2006,12,22]],"date-time":"2006-12-22T01:26:24Z","timestamp":1166750784000},"page":"944-949","source":"Crossref","is-referenced-by-count":1,"title":["Direct Model Checking Matrix Algorithm"],"prefix":"10.1007","volume":"21","author":[{"given":"Zhi-Hong","family":"Tao","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hans Kleine","family":"B\u00fcning","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Li-Fu","family":"Wang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"3","key":"944_CR1","doi-asserted-by":"crossref","first-page":"207","DOI":"10.1007\/BF01257083","volume":"20","author":"M Ben-Ari","year":"1983","unstructured":"Ben-Ari M, Manna Z, Pnueli A. The temporal logic of branching time. Acta Information, 1983, 20(3): 207\u2013226.","journal-title":"Acta Information"},{"key":"944_CR2","doi-asserted-by":"crossref","unstructured":"Biere A, Cimatti A, Clarke E M, Fujita M, Zhu Y. Symbolic model checking using SAT procedures instead of BDDs. Annuanl ACM IEEE Design Automation Conference, New Orleans, USA, 1999, pp.317\u2013320.","DOI":"10.21236\/ADA360973"},{"key":"944_CR3","doi-asserted-by":"crossref","unstructured":"Biere A, Cimatti A, Clarek E, Zhu Y. Symbolic model checking without BDDs. In Proc. the Workshop on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201999), LNCS, Springer-Verlag, 1999, 1579: 193\u2013207.","DOI":"10.21236\/ADA360973"},{"issue":"2","key":"944_CR4","doi-asserted-by":"crossref","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"J R Burch","year":"1992","unstructured":"Burch J R, Clarke E M, McMillan K L. Symbolic model checking: 1020 states and beyond. Information and Computation, 1992, 98(2): 142\u2013170.","journal-title":"Information and Computation"},{"key":"944_CR5","doi-asserted-by":"crossref","unstructured":"Clarke E M, Emerson E A. Design and synthesis of synchronization skeletons using branching time temporal logic. Logic of Programs: Workshop, Yorktoen Heights, LNCS, NY: Springer, 1981, 131: 52\u201371.","DOI":"10.1007\/BFb0025774"},{"issue":"2","key":"944_CR6","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E M Clarke","year":"1986","unstructured":"Clarke E M, Emerson E A, Sistla A P. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems, 1986, 8(2): 244\u2013263.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"944_CR7","unstructured":"Aho A V, Hopcroft J E, Ullman J D. The Design and Analysis of Computer Algorithms. Addison Wesley, 1974."},{"key":"944_CR8","doi-asserted-by":"crossref","unstructured":"McMillan K L. Symbolic Model Checking: An Approach to the State Explosion Problem. Kluwer Academic Publishers, 1993.","DOI":"10.1007\/978-1-4615-3190-6"},{"issue":"5","key":"944_CR9","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G Holzmann","year":"May 1999","unstructured":"Holzmann G. The Spin model checker. IEEE Trans. Software Engineering, May 1999, 23(5): 279\u2013295.","journal-title":"IEEE Trans. Software Engineering"},{"issue":"10","key":"944_CR10","first-page":"1672","volume":"14","author":"Jian Liu","year":"2003","unstructured":"Liu Jian, Lin Hui-Min. Consistency between the predicate \u03bc-calculus and modal graphs. Journal of Software, 2003, 14(10): 1672\u20131680.","journal-title":"Journal of Software"},{"issue":"4","key":"944_CR11","first-page":"713","volume":"14","author":"X Y Zhu","year":"2003","unstructured":"Zhu X Y, Tang Z S. A temporal logic-based software architecture description language XYZ\/ADL. Journal of Software, 2003, 14(4): 713\u2013720.","journal-title":"Journal of Software"},{"key":"944_CR12","doi-asserted-by":"crossref","unstructured":"Bjesse P, Leonard T, Mokkedem A. Finding bugs in an alpha microprocessor using satisfiability solvers. In Proc. 13th Int. Conf. Computer Aided Verification (CAV\u201901), Berry G, Comon H, Finkel A (eds.), Lecture Notes in Computer Science, Springer-Verlag, 2001, 2102: 454\u2013464.","DOI":"10.1007\/3-540-44585-4_44"},{"key":"944_CR13","volume-title":"Model Checking","author":"E M Clarke","year":"2000","unstructured":"Clarke E M, Grumberg O, Peled D A. Model Checking. Cambridge, MA: The MIT Press, 2000."},{"issue":"3","key":"944_CR14","doi-asserted-by":"crossref","first-page":"213","DOI":"10.1145\/258077.258078","volume":"6","author":"R Allen","year":"July 1997","unstructured":"Allen R, Garlan D. A formal basis for architectural connection. ACM Trans. Software Engineering and Methodology, July 1997, 6(3): 213\u2013249.","journal-title":"ACM Trans. Software Engineering and Methodology"},{"key":"944_CR15","unstructured":"ITU-T Z 100\u20132000. Specification and description language, Dec 2000."}],"container-title":["Journal of Computer Science and Technology"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11390-006-0944-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11390-006-0944-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11390-006-0944-5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,1]],"date-time":"2019-06-01T10:32:37Z","timestamp":1559385157000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11390-006-0944-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,11]]},"references-count":15,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2006,11]]}},"alternative-id":["944"],"URL":"https:\/\/doi.org\/10.1007\/s11390-006-0944-5","relation":{},"ISSN":["1000-9000","1860-4749"],"issn-type":[{"value":"1000-9000","type":"print"},{"value":"1860-4749","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006,11]]}}}