{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,1]],"date-time":"2022-04-01T13:36:15Z","timestamp":1648820175153},"reference-count":12,"publisher":"Hindawi Limited","license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/3.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Journal of Applied Mathematics"],"published-print":{"date-parts":[[2015]]},"abstract":"<jats:p>We present on-the-fly degeneralization algorithm used to transform generalized B\u00fcchi automata (GBA) into B\u00fcchi Automata (BA) different from the standard degeneralization algorithm. Contented situation, which is used to record what acceptance conditions are satisfiable during expanding LTL formulae, is attached to the states and transitions in the BA. In order to get the deterministic BA, the Shannon expansion is used recursively when we expand LTL formulae by applying the tableau rules. On-the-fly degeneralization algorithm is carried out in each step of the expansion of LTL formulae. Ordered binary decision diagrams are used to represent the BA and simplify LTL formulae. The temporary automata are stored as syntax directed acyclic graph in order to save storage space. These ideas are implemented in a conversion algorithm used to build a property automaton corresponding to the given LTL formulae. We compare our method to previous work and show that it is more efficient for four sets of random formulae generated by LBTT.<\/jats:p>","DOI":"10.1155\/2015\/516104","type":"journal-article","created":{"date-parts":[[2015,2,10]],"date-time":"2015-02-10T16:06:55Z","timestamp":1423584415000},"page":"1-10","source":"Crossref","is-referenced-by-count":0,"title":["Degeneralization Algorithm for Generation of B\u00fcchi Automata Based on Contented Situation"],"prefix":"10.1155","volume":"2015","author":[{"given":"Laixiang","family":"Shan","sequence":"first","affiliation":[{"name":"School of Software, Tsinghua University, Beijing 100084, China"}]},{"given":"Jun","family":"Qin","sequence":"additional","affiliation":[{"name":"Credit Reference Center, People\u2019s Bank of China, Beijing 100800, China"}]},{"given":"Mingshi","family":"Chen","sequence":"additional","affiliation":[{"name":"Department of Mathematical Sciences, Tsinghua University, Beijing 100084, China"}]},{"given":"Zheng","family":"Qin","sequence":"additional","affiliation":[{"name":"School of Software, Tsinghua University, Beijing 100084, China"}]}],"member":"98","reference":[{"key":"1","year":"1999"},{"key":"2","first-page":"95","volume-title":"LTL to B\u00fcchi automata translation: fast and more deterministic","volume":"7214","year":"2012"},{"key":"3","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44585-4_6"},{"key":"4","first-page":"76","volume-title":"Alternation removal in buchi automata","year":"2010"},{"key":"6","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48119-2_16"},{"key":"8","doi-asserted-by":"publisher","DOI":"10.1109\/32.588521"},{"key":"9","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36135-9_20"},{"key":"10","first-page":"81","volume-title":"Compositional approach to suspension and other improvements to LTL translation","year":"2013"},{"key":"11","first-page":"559","volume-title":"Automata with generalized Rabin pairs for probabilistic model checking and LTL synthesis","year":"2013"},{"key":"12","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-45221-5_44"},{"key":"14","doi-asserted-by":"publisher","DOI":"10.1109\/tc.1986.1676819"},{"key":"15","doi-asserted-by":"publisher","DOI":"10.1007\/s100090200070"}],"container-title":["Journal of Applied Mathematics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/downloads.hindawi.com\/journals\/jam\/2015\/516104.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/downloads.hindawi.com\/journals\/jam\/2015\/516104.xml","content-type":"application\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/downloads.hindawi.com\/journals\/jam\/2015\/516104.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2016,8,18]],"date-time":"2016-08-18T17:01:20Z","timestamp":1471539680000},"score":1,"resource":{"primary":{"URL":"http:\/\/www.hindawi.com\/journals\/jam\/2015\/516104\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"references-count":12,"alternative-id":["516104","516104"],"URL":"https:\/\/doi.org\/10.1155\/2015\/516104","relation":{},"ISSN":["1110-757X","1687-0042"],"issn-type":[{"value":"1110-757X","type":"print"},{"value":"1687-0042","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]}}}