{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,1]],"date-time":"2022-04-01T07:42:26Z","timestamp":1648798946067},"reference-count":14,"publisher":"International Academy Publishing (IAP)","issue":"4","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["JSW"],"DOI":"10.4304\/jsw.9.4.970-976","type":"journal-article","created":{"date-parts":[[2014,4,23]],"date-time":"2014-04-23T16:46:06Z","timestamp":1398271566000},"source":"Crossref","is-referenced-by-count":1,"title":["Conversion Algorithm of Linear-Time Temporal Logic to Buchi Automata"],"prefix":"10.17706","volume":"9","author":[{"given":"Laixiang","family":"Shan","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zheng","family":"Qin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Shengnan","family":"Li","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Renwei","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xiao","family":"Yang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"7163","published-online":{"date-parts":[[2014,4,1]]},"reference":[{"key":"ref1","volume-title":"Model checking","author":"Clarke","year":"1999","unstructured":"[1]E. M. Clarke, O. Grumberg, and D. A. Peled, Model checking. MIT press, 1999."},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14162-1_7"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1109\/32.588521"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1016\/S1007-0214(09)70010-0"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.4304\/jcp.7.10.2503-2510"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_7"},{"key":"ref7","first-page":"98","volume-title":"\"Symbolic algorithm for generation buchi automata from ltl formulas \" in Parallel Computing Technologies","author":"Shoshmina","year":"2011","unstructured":"[12] I. V. Shoshmina and A. B. Belyaev, \"Symbolic algorithm for generation buchi automata from ltl formulas,\" in Parallel Computing Technologies. Springer, 2011, pp. 98\u2013109."},{"key":"ref8","first-page":"249","volume-title":"\"Improved automata generation for linear temporal logic \" in Computer Aided Verification","author":"Daniele","year":"1999","unstructured":"[13] M. Daniele, F. Giunchiglia, and M. Y. Vardi, \"Improved automata generation for linear temporal logic,\" in Computer Aided Verification. Springer, 1999, pp. 249\u2013260."},{"key":"ref9","first-page":"308","volume-title":"\"From states to transitions","author":"Giannakopoulou","year":"2002","unstructured":"[14] D. Giannakopoulou and F. Lerda, \"From states to transitions: Improving translation of ltl formulae to b\u00a8uchi automata,\" in Formal Techniques for Networked and Distributed SytemsFORTE 2002. Springer, 2002, pp. 308\u2013326."},{"key":"ref10","doi-asserted-by":"crossref","first-page":"248","DOI":"10.1007\/10722167_21","volume-title":"\"Efficient buchi automata from ltl formulae \" in Computer Aided Verification","author":"Somenzi","year":"2000","unstructured":"[15] F. Somenzi and R. Bloem, \"Efficient buchi automata from ltl formulae,\" in Computer Aided Verification. Springer, 2000, pp. 248\u2013263."},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.4304\/jcp.7.2.362-370"},{"key":"ref12","first-page":"126","volume-title":"\"more deterministic vs smaller buchi automata for efficient ltl model checking \" in Correct Hardware Design and Verification Methods","author":"Sebastiani","year":"2003","unstructured":"[17] R. Sebastiani and S. Tonetta, \"more deterministic vs.smaller buchi automata for efficient ltl model checking,\" in Correct Hardware Design and Verification Methods. Springer, 2003, pp. 126\u2013140."},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44585-4_6"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1007\/11591191_50"}],"container-title":["Journal of Software"],"original-title":[],"deposited":{"date-parts":[[2019,8,9]],"date-time":"2019-08-09T20:52:58Z","timestamp":1565383978000},"score":1,"resource":{"primary":{"URL":"http:\/\/ojs.academypublisher.com\/index.php\/jsw\/article\/view\/10816"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,4,1]]},"references-count":14,"journal-issue":{"issue":"4","published-online":{"date-parts":[[2014,4,1]]}},"URL":"https:\/\/doi.org\/10.4304\/jsw.9.4.970-976","relation":{},"ISSN":["1796-217X"],"issn-type":[{"value":"1796-217X","type":"print"}],"subject":[],"published":{"date-parts":[[2014,4,1]]}}}