{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,3]],"date-time":"2022-04-03T19:56:26Z","timestamp":1649015786162},"reference-count":21,"publisher":"Springer Science and Business Media LLC","issue":"5-6","license":[{"start":{"date-parts":[[2012,1,24]],"date-time":"2012-01-24T00:00:00Z","timestamp":1327363200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2013,10]]},"DOI":"10.1007\/s10009-012-0222-5","type":"journal-article","created":{"date-parts":[[2012,1,23]],"date-time":"2012-01-23T22:22:13Z","timestamp":1327357333000},"page":"541-561","source":"Crossref","is-referenced-by-count":7,"title":["Exploiting structure in LTL synthesis"],"prefix":"10.1007","volume":"15","author":[{"given":"Emmanuel","family":"Filiot","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Naiyong","family":"Jin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jean-Fran\u00e7ois","family":"Raskin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2012,1,24]]},"reference":[{"key":"222_CR1","unstructured":"Acacia. http:\/\/www.antichains.be\/acacia"},{"key":"222_CR2","doi-asserted-by":"crossref","unstructured":"Abadi, M., Lamport, L., Wolper, P.: Realizable and unrealizable specifications of reactive systems. In: International Conference on Automata, Languages and Programming (ICALP) (1989)","DOI":"10.1007\/BFb0035748"},{"issue":"4","key":"222_CR3","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/j.entcs.2007.09.004","volume":"190","author":"R. Bloem","year":"2007","unstructured":"Bloem R., Galler S., Jobstmann B., Piterman N., Pnueli A., Weiglhofer M.: Specify, compile, run: hardware from psl. Electr. Notes Theor. Comput. Sci. 190(4), 3\u201316 (2007)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"222_CR4","doi-asserted-by":"crossref","unstructured":"Ehlers, R.: Symbolic bounded synthesis. In: Proceedings of the International Conference on Computer Aided Verification (CAV). LNCS, vol 6174, pp. 365\u2013379. Springer, Berlin (2010)","DOI":"10.1007\/978-3-642-14295-6_33"},{"key":"222_CR5","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: MiniSat. http:\/\/minisat.se\/ (2010)"},{"key":"222_CR6","doi-asserted-by":"crossref","unstructured":"Filiot, E., Jin, N., Raskin, J.-F.: An antichain algorithm for LTL realizability. In: Proceedings of the International Conference on Computer Aided Verification (CAV). LNCS, vol 5643, pp. 263\u2013277. Springer, Berlin (2009)","DOI":"10.1007\/978-3-642-02658-4_22"},{"key":"222_CR7","doi-asserted-by":"crossref","unstructured":"Filiot, E., Jin, N., Raskin, J.-F.: Compositional algorithms for LTL synthesis. In: International Symposium on Automated Technology for Verification and Analysis (ATVA), pp. 112\u2013127 (2010)","DOI":"10.1007\/978-3-642-15643-4_10"},{"key":"222_CR8","doi-asserted-by":"crossref","unstructured":"Gastin, P., Oddoux, D.: Fast LTL to B\u00fcchi automata translation. In: Proceedings of the International Conference on Computer Aided Verification (CAV). LNCS, pp. 53\u201365. Springer, Berlin (2001)","DOI":"10.1007\/3-540-44585-4_6"},{"key":"222_CR9","doi-asserted-by":"crossref","unstructured":"Jobstmann, B., Bloem, R.: Optimizations for LTL synthesis. In: Formal Methods in Computer-Aided Design (FMCAD), pp. 117\u2013124. IEEE Computer Society (2006)","DOI":"10.1109\/FMCAD.2006.22"},{"key":"222_CR10","doi-asserted-by":"crossref","unstructured":"Kupferman, O., Vardi, M.Y.: Safraless decision procedures. In: IEEE Symposium on Foundations of Computer Science (FOCS) (2005)","DOI":"10.1109\/SFCS.2005.66"},{"key":"222_CR11","unstructured":"Lily. http:\/\/www.iaik.tugraz.at\/content\/research\/design_verification\/lily\/"},{"key":"222_CR12","unstructured":"LTL2BA. http:\/\/www.lsv.ens-cachan.fr\/~gastin\/ltl2ba\/"},{"key":"222_CR13","doi-asserted-by":"crossref","unstructured":"Martin, D.: Borel determinacy. In: Annals of Mathematics, vol. 102, pp. 363\u2013371 (1975)","DOI":"10.2307\/1971035"},{"key":"222_CR14","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: ACM Symposium on Principles of Programming Languages (POPL). ACM, New York 1989","DOI":"10.1145\/75277.75293"},{"key":"222_CR15","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of an asynchronous reactive module. In: Proceedings of 16th ICALP, 1989"},{"key":"222_CR16","doi-asserted-by":"crossref","unstructured":"Safra, S.: On the complexity of \u03c9 automata. In: IEEE Symposium on Foundations of Computer Science (FOCS), pp. 319\u2013327 (1988)","DOI":"10.1109\/SFCS.1988.21948"},{"key":"222_CR17","doi-asserted-by":"crossref","unstructured":"Schewe, S., Finkbeiner, B.: Bounded synthesis. In: International Symposium on Automated Technology for Verification and Analysis (ATVA). LNCS, vol 4762, pp. 474\u2013488. Springer, Berlin (2007)","DOI":"10.1007\/978-3-540-75596-8_33"},{"key":"222_CR18","doi-asserted-by":"crossref","unstructured":"Somenzi, F., Bloem, R.: Efficient B\u00fcchi automata from LTL formulae. In: Proceedings of the International Conference on Computer Aided Verification (CAV) (2000)","DOI":"10.1007\/10722167_21"},{"key":"222_CR19","doi-asserted-by":"crossref","unstructured":"Thomas, W.: Church\u2019s problem and a tour through automata theory. In: Pillars of Computer Science. LNCS, vol 4800, pp 635\u2013655. Springer, Berlin (2008)","DOI":"10.1007\/978-3-540-78127-1_35"},{"key":"222_CR20","unstructured":"Unbeast. http:\/\/react.cs.uni-sb.de\/tools\/unbeast\/"},{"key":"222_CR21","unstructured":"Wring. http:\/\/www.iaik.tugraz.at\/content\/research\/design_verification\/wring\/"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-012-0222-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-012-0222-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-012-0222-5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,22]],"date-time":"2019-06-22T20:48:39Z","timestamp":1561236519000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-012-0222-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,1,24]]},"references-count":21,"journal-issue":{"issue":"5-6","published-print":{"date-parts":[[2013,10]]}},"alternative-id":["222"],"URL":"https:\/\/doi.org\/10.1007\/s10009-012-0222-5","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,1,24]]}}}