{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,7,2]],"date-time":"2024-07-02T00:12:01Z","timestamp":1719879121936},"reference-count":39,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2024,5,3]],"date-time":"2024-05-03T00:00:00Z","timestamp":1714694400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,5,3]],"date-time":"2024-05-03T00:00:00Z","timestamp":1714694400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Auton Agent Multi-Agent Syst"],"published-print":{"date-parts":[[2024,6]]},"DOI":"10.1007\/s10458-024-09648-7","type":"journal-article","created":{"date-parts":[[2024,5,3]],"date-time":"2024-05-03T06:01:53Z","timestamp":1714716113000},"update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Controller synthesis for linear temporal logic and steady-state specifications"],"prefix":"10.1007","volume":"38","author":[{"given":"Alvaro","family":"Velasquez","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ismail","family":"Alkhouri","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andre","family":"Beckus","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ashutosh","family":"Trivedi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"George","family":"Atia","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,5,3]]},"reference":[{"key":"9648_CR1","unstructured":"Velasquez, A., Alkhouri, I., Beckus, A., Trivedi, A., & Atia, G.(2022). Controller synthesis for omega-regular and steady-state specifications. In Proceedings of the 21st international conference on autonomous agents and multiagent systems (pp. 1310\u20131318)."},{"key":"9648_CR2","doi-asserted-by":"crossref","unstructured":"Thomas, W. (1990). Handbook of theoretical computer science (pp. 133\u2013191). Chap. Automata on Infinite Objects.","DOI":"10.1016\/B978-0-444-88074-1.50009-3"},{"key":"9648_CR3","unstructured":"Perrin, D., & Pin, J. (2004). Infinite words: Automata, semigroups, logic and games. Academic Press."},{"key":"9648_CR4","doi-asserted-by":"crossref","unstructured":"Vardi, M. (2011). The rise and fall of linear time logic. In 2nd International Symposium on Games, Automata, Logics and Formal Verification.","DOI":"10.4204\/EPTCS.54.0.2"},{"key":"9648_CR5","unstructured":"de Alfaro, L. (1998). Formal verification of probabilistic systems. (Ph.D. Thesis, Stanford University)."},{"key":"9648_CR6","unstructured":"Baier, C., & Katoen, J.-P. (2008). Principles of model checking. MIT Press."},{"key":"9648_CR7","doi-asserted-by":"crossref","unstructured":"Akshay, S., Bertrand, N., Haddad, S., & Helouet, L. (2013). The steady-state control problem for markov decision processes. In International conference on quantitative evaluation of systems (pp. 290\u2013304). Springer.","DOI":"10.1007\/978-3-642-40196-1_26"},{"key":"9648_CR8","doi-asserted-by":"crossref","unstructured":"Velasquez, A. (2019). Steady-state policy synthesis for verifiable control. In Proceedings of the 28th international joint conference on artificial intelligence, IJCAI-19 (pp. 5653\u20135661).","DOI":"10.24963\/ijcai.2019\/784"},{"key":"9648_CR9","doi-asserted-by":"crossref","unstructured":"Atia, G., Beckus, A., & Alkhouri, I., Velasquez, A. (2020). Steady-state policy synthesis in multichain markov decision processes. In Proceedings of the 29th international joint conference on artificial intelligence, IJCAI-20 (pp. 4069\u20134075).","DOI":"10.24963\/ijcai.2020\/563"},{"key":"9648_CR10","doi-asserted-by":"publisher","first-page":"1029","DOI":"10.1613\/jair.1.12611","volume":"72","author":"GK Atia","year":"2021","unstructured":"Atia, G. K., Beckus, A., Alkhouri, I., & Velasquez, A. (2021). Steady-state planning in expected reward multichain MDPs. Journal of Artificial Intelligence Research, 72, 1029\u20131082.","journal-title":"Journal of Artificial Intelligence Research"},{"key":"9648_CR11","doi-asserted-by":"crossref","unstructured":"K\u0159et\u00ednsk\u1ef3, J. (2021). LTL-constrained steady-state policy synthesis. arXiv preprint arXiv:2105.14894.","DOI":"10.24963\/ijcai.2021\/565"},{"key":"9648_CR12","doi-asserted-by":"crossref","unstructured":"Kallenberg, L. (2002). Classification problems in MDPs. In Markov Processes and Controlled Markov Chains (pp. 151\u2013165).","DOI":"10.1007\/978-1-4613-0265-0_9"},{"key":"9648_CR13","unstructured":"Sarathy, V., Kasenberg, D., Goel, S., Sinapov, J., & Scheutz, M. (2021). Spotter: Extending symbolic planning operators through targeted reinforcement learning. In Proceedings of the 20th international conference on autonomous agents and multiAgent systems (pp. 1118\u20131126)."},{"issue":"1","key":"9648_CR14","doi-asserted-by":"publisher","first-page":"3515","DOI":"10.3182\/20110828-6-IT-1002.02287","volume":"44","author":"XCD Ding","year":"2011","unstructured":"Ding, X. C. D., Smith, S. L., Belta, C., & Rus, D. (2011). LTL control in uncertain environments with probabilistic satisfaction guarantees. IFAC Proceedings Volumes, 44(1), 3515\u20133520.","journal-title":"IFAC Proceedings Volumes"},{"key":"9648_CR15","doi-asserted-by":"crossref","unstructured":"Lacerda, B., Parker, D., & Hawes, N. (2014). Optimal and dynamic planning for markov decision processes with co-safe LTL specifications. In 2014 IEEE\/RSJ international conference on intelligent robots and systems (pp. 1511\u20131516). IEEE.","DOI":"10.1109\/IROS.2014.6942756"},{"key":"9648_CR16","doi-asserted-by":"crossref","unstructured":"Norris, J. R., & Norris, J. R. (1998). Markov chains, vol. 2. Cambridge University Press.","DOI":"10.1017\/CBO9780511810633"},{"key":"9648_CR17","doi-asserted-by":"crossref","unstructured":"Pnueli, A., & Rosner, R. (1989). On the synthesis of a reactive module. In Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on principles of programming languages (pp. 179\u2013190).","DOI":"10.1145\/75277.75293"},{"key":"9648_CR18","unstructured":"Church, A. (1963). Application of recursive arithmetic to the problem of circuit synthesis. Journal of Symbolic Logic, 28(4)."},{"key":"9648_CR19","doi-asserted-by":"crossref","unstructured":"Etessami, K., Kwiatkowska, M., Vardi, M. Y., & Yannakakis, M. (2007). Multi-objective model checking of Markov decision processes. In International conference on tools and algorithms for the construction and analysis of systems (pp. 50\u201365). Springer.","DOI":"10.1007\/978-3-540-71209-1_6"},{"key":"9648_CR20","unstructured":"Yannakakis, M., Vardi, M. Y., Kwiatkowska, M., & Etessami, K. (2008). Multi-objective model checking of Markov decision processes. Logical Methods in Computer Science."},{"key":"9648_CR21","doi-asserted-by":"crossref","unstructured":"Forejt, V., Kwiatkowska, M., Norman, G., & Parker, D. (2011). Automated verification techniques for probabilistic systems. In International school on formal methods for the design of computer, communication and software systems (pp. 53\u2013113). Springer.","DOI":"10.1007\/978-3-642-21455-4_3"},{"key":"9648_CR22","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., & Henzinger, M. (2011). Faster and dynamic algorithms for maximal end-component decomposition and related graph problems in probabilistic verification. In Symposium on discrete algorithms (SODA) (pp. 1318\u20131336).","DOI":"10.1137\/1.9781611973082.101"},{"key":"9648_CR23","unstructured":"Kallenberg, L. C. M. (1983). Linear programming and finite Markovian control problems. Mathematisch Centrum."},{"key":"9648_CR24","doi-asserted-by":"crossref","unstructured":"Puterman, M. L. (1994). Markov decision processes. Wiley.","DOI":"10.1002\/9780470316887"},{"issue":"3","key":"9648_CR25","doi-asserted-by":"publisher","first-page":"387","DOI":"10.1007\/s001860050035","volume":"48","author":"E Altman","year":"1998","unstructured":"Altman, E. (1998). Constrained Markov decision processes with total cost criteria: Lagrangian approach and dual linear program. Mathematical Methods of Operations Research, 48(3), 387\u2013417.","journal-title":"Mathematical Methods of Operations Research"},{"key":"9648_CR26","doi-asserted-by":"publisher","unstructured":"Feinberg, E. A. (2009). Adaptive computation of optimal nonrandomized policies in constrained average-reward MDPs. In IEEE symposium on adaptive dynamic programming and reinforcement learning (pp. 96\u2013100). https:\/\/doi.org\/10.1109\/ADPRL.2009.4927531","DOI":"10.1109\/ADPRL.2009.4927531"},{"key":"9648_CR27","unstructured":"Sutton, R. S., & Barto, A. G. (2018). Reinforcement learning: An introduction. MIT Press."},{"key":"9648_CR28","doi-asserted-by":"crossref","unstructured":"Bouyer, P., Markey, N., & Matteplackel, R. M. (2014). Averaging in LTL. In: International conference on concurrency theory (pp. 266\u2013280). Springer.","DOI":"10.1007\/978-3-662-44584-6_19"},{"key":"9648_CR29","doi-asserted-by":"crossref","unstructured":"Almagor, S., Boker, U., & Kupferman, O. (2014). Discounting in LTL. In International conference on tools and algorithms for the construction and analysis of systems (pp. 424\u2013439). Springer.","DOI":"10.1007\/978-3-642-54862-8_37"},{"issue":"4","key":"9648_CR30","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2629686","volume":"15","author":"U Boker","year":"2014","unstructured":"Boker, U., Chatterjee, K., Henzinger, T. A., & Kupferman, O. (2014). Temporal specifications with accumulative values. ACM Transactions on Computational Logic (TOCL), 15(4), 1\u201325.","journal-title":"ACM Transactions on Computational Logic (TOCL)"},{"key":"9648_CR31","doi-asserted-by":"crossref","unstructured":"Bollig, B., Decker, N., & Leucker, M. (2012). Frequency linear-time temporal logic. In 2012 6th international symposium on theoretical aspects of software engineering (pp. 85\u201392). IEEE.","DOI":"10.1109\/TASE.2012.43"},{"key":"9648_CR32","doi-asserted-by":"crossref","unstructured":"Svore\u0148ov\u00e1, M., \u010cern\u00e1, I., & Belta, C. (2013). Optimal control of MDPs with temporal logic constraints. In 52nd IEEE conference on decision and control (pp. 3938\u20133943). IEEE.","DOI":"10.1109\/CDC.2013.6760491"},{"key":"9648_CR33","doi-asserted-by":"crossref","unstructured":"Altman, E., Boularouk, S., & Josselin, D. (2019). Constrained Markov decision processes with total expected cost criteria. In Proceedings of the 12th EAI international conference on performance evaluation methodologies and tools (pp. 191\u2013192). ACM.","DOI":"10.1145\/3306309.3306342"},{"issue":"3","key":"9648_CR34","doi-asserted-by":"publisher","first-page":"545","DOI":"10.1287\/moor.27.3.545.316","volume":"27","author":"D Krass","year":"2002","unstructured":"Krass, D., & Vrieze, O. J. (2002). Achieving target state-action frequencies in multichain average-reward Markov decision processes. Mathematics of Operations Research, 27(3), 545\u2013566.","journal-title":"Mathematics of Operations Research"},{"key":"9648_CR35","doi-asserted-by":"crossref","unstructured":"Esparza, J., & K\u0159et\u00ednsk\u1ef3, J. (2014). From ltl to deterministic automata: A safraless compositional approach. In Computer aided verification: 26th international conference, CAV 2014, held as part of the Vienna summer of logic, VSL 2014, Vienna, Austria, July 18\u201322, 2014. Proceedings 26 (pp. 192\u2013208). Springer.","DOI":"10.1007\/978-3-319-08867-9_13"},{"key":"9648_CR36","doi-asserted-by":"crossref","unstructured":"Trevizan, F. W., Thi\u00e9baux, S., & Haslum, P. (2017). Occupation measure heuristics for probabilistic planning. In ICAPS (pp. 306\u2013315).","DOI":"10.1609\/icaps.v27i1.13840"},{"key":"9648_CR37","doi-asserted-by":"crossref","unstructured":"Buchholz, P. (1994). Exact and ordinary lumpability in finite Markov chains. Journal of Applied Probability, 59\u201375.","DOI":"10.2307\/3215235"},{"issue":"1","key":"9648_CR38","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1080\/15326348908807099","volume":"5","author":"U Sumita","year":"1989","unstructured":"Sumita, U., & Rieders, M. (1989). Lumpability and time reversibility in the aggregation-disaggregation method for large Markov chains. Stochastic Models, 5(1), 63\u201381.","journal-title":"Stochastic Models"},{"key":"9648_CR39","unstructured":"ILOG, Inc. (2006). ILOG CPLEX: High-performance software for mathematical programming and optimization. See http:\/\/www.ilog.com\/products\/cplex\/."}],"container-title":["Autonomous Agents and Multi-Agent Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10458-024-09648-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10458-024-09648-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10458-024-09648-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,7,1]],"date-time":"2024-07-01T23:07:07Z","timestamp":1719875227000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10458-024-09648-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,5,3]]},"references-count":39,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2024,6]]}},"alternative-id":["9648"],"URL":"https:\/\/doi.org\/10.1007\/s10458-024-09648-7","relation":{},"ISSN":["1387-2532","1573-7454"],"issn-type":[{"value":"1387-2532","type":"print"},{"value":"1573-7454","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,5,3]]},"assertion":[{"value":"8 April 2024","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"3 May 2024","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors declare no Conflict of interest.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflict of interest"}}],"article-number":"17"}}