[{"publication_identifier":{"issn":["18605974"]},"month":"09","oa_version":"Published Version","day":"13","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","file":[{"date_created":"2018-12-12T10:14:37Z","date_updated":"2020-07-14T12:46:33Z","file_name":"IST-2015-321-v1+1_main.pdf","checksum":"08041379ba408d40664f449eb5907a8f","file_id":"5090","relation":"main_file","content_type":"application/pdf","file_size":279071,"access_level":"open_access","creator":"system"},{"file_id":"5091","checksum":"08041379ba408d40664f449eb5907a8f","file_name":"IST-2018-955-v1+1_2017_Chatterjee_Edit_distance.pdf","date_updated":"2020-07-14T12:46:33Z","date_created":"2018-12-12T10:14:38Z","creator":"system","relation":"main_file","access_level":"open_access","file_size":279071,"content_type":"application/pdf"}],"author":[{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","first_name":"Thomas A"},{"first_name":"Rasmus","full_name":"Ibsen-Jensen, Rasmus","id":"3B699956-F248-11E8-B48F-1D18A9856A87","last_name":"Ibsen-Jensen","orcid":"0000-0003-4783-0389"},{"last_name":"Otop","first_name":"Jan","full_name":"Otop, Jan"}],"status":"public","type":"journal_article","has_accepted_license":"1","scopus_import":1,"intvolume":"        13","pubrep_id":"955","oa":1,"date_updated":"2023-02-23T12:26:25Z","issue":"3","title":"Edit distance for pushdown automata","publication":"Logical Methods in Computer Science","language":[{"iso":"eng"}],"ddc":["004"],"tmp":{"image":"/image/cc_by_nd.png","legal_code_url":"https://creativecommons.org/licenses/by-nd/4.0/legalcode","name":"Creative Commons Attribution-NoDerivatives 4.0 International (CC BY-ND 4.0)","short":"CC BY-ND (4.0)"},"abstract":[{"text":"The edit distance between two words w 1 , w 2 is the minimal number of word operations (letter insertions, deletions, and substitutions) necessary to transform w 1 to w 2 . The edit distance generalizes to languages L 1 , L 2 , where the edit distance from L 1 to L 2 is the minimal number k such that for every word from L 1 there exists a word in L 2 with edit distance at most k . We study the edit distance computation problem between pushdown automata and their subclasses. The problem of computing edit distance to a pushdown automaton is undecidable, and in practice, the interesting question is to compute the edit distance from a pushdown automaton (the implementation, a standard model for programs with recursion) to a regular language (the specification). In this work, we present a complete picture of decidability and complexity for the following problems: (1) deciding whether, for a given threshold k , the edit distance from a pushdown automaton to a finite automaton is at most k , and (2) deciding whether the edit distance from a pushdown automaton to a finite automaton is finite. ","lang":"eng"}],"publication_status":"published","publisher":"International Federation of Computational Logic","license":"https://creativecommons.org/licenses/by-nd/4.0/","date_published":"2017-09-13T00:00:00Z","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"volume":13,"quality_controlled":"1","project":[{"name":"Moderne Concurrency Paradigms","call_identifier":"FWF","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","grant_number":"S11402-N23"},{"name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23"},{"grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"The Wittgenstein Prize"},{"call_identifier":"FP7","name":"Quantitative Reactive Modeling","grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications"},{"grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Game Theory"}],"ec_funded":1,"related_material":{"record":[{"relation":"earlier_version","id":"1610","status":"public"},{"id":"5438","relation":"earlier_version","status":"public"}]},"year":"2017","citation":{"chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, Rasmus Ibsen-Jensen, and Jan Otop. “Edit Distance for Pushdown Automata.” <i>Logical Methods in Computer Science</i>. International Federation of Computational Logic, 2017. <a href=\"https://doi.org/10.23638/LMCS-13(3:23)2017\">https://doi.org/10.23638/LMCS-13(3:23)2017</a>.","mla":"Chatterjee, Krishnendu, et al. “Edit Distance for Pushdown Automata.” <i>Logical Methods in Computer Science</i>, vol. 13, no. 3, International Federation of Computational Logic, 2017, doi:<a href=\"https://doi.org/10.23638/LMCS-13(3:23)2017\">10.23638/LMCS-13(3:23)2017</a>.","ista":"Chatterjee K, Henzinger TA, Ibsen-Jensen R, Otop J. 2017. Edit distance for pushdown automata. Logical Methods in Computer Science. 13(3).","ama":"Chatterjee K, Henzinger TA, Ibsen-Jensen R, Otop J. Edit distance for pushdown automata. <i>Logical Methods in Computer Science</i>. 2017;13(3). doi:<a href=\"https://doi.org/10.23638/LMCS-13(3:23)2017\">10.23638/LMCS-13(3:23)2017</a>","ieee":"K. Chatterjee, T. A. Henzinger, R. Ibsen-Jensen, and J. Otop, “Edit distance for pushdown automata,” <i>Logical Methods in Computer Science</i>, vol. 13, no. 3. International Federation of Computational Logic, 2017.","short":"K. Chatterjee, T.A. Henzinger, R. Ibsen-Jensen, J. Otop, Logical Methods in Computer Science 13 (2017).","apa":"Chatterjee, K., Henzinger, T. A., Ibsen-Jensen, R., &#38; Otop, J. (2017). Edit distance for pushdown automata. <i>Logical Methods in Computer Science</i>. International Federation of Computational Logic. <a href=\"https://doi.org/10.23638/LMCS-13(3:23)2017\">https://doi.org/10.23638/LMCS-13(3:23)2017</a>"},"date_created":"2018-12-11T11:46:37Z","publist_id":"7356","doi":"10.23638/LMCS-13(3:23)2017","file_date_updated":"2020-07-14T12:46:33Z","_id":"465"},{"ddc":["004"],"tmp":{"image":"/image/cc_by_nd.png","legal_code_url":"https://creativecommons.org/licenses/by-nd/4.0/legalcode","name":"Creative Commons Attribution-NoDerivatives 4.0 International (CC BY-ND 4.0)","short":"CC BY-ND (4.0)"},"abstract":[{"lang":"eng","text":"We consider Markov decision processes (MDPs) with multiple limit-average (or mean-payoff) objectives. There exist two different views: (i) the expectation semantics, where the goal is to optimize the expected mean-payoff objective, and (ii) the satisfaction semantics, where the goal is to maximize the probability of runs such that the mean-payoff value stays above a given vector. We consider optimization with respect to both objectives at once, thus unifying the existing semantics. Precisely, the goal is to optimize the expectation while ensuring the satisfaction constraint. Our problem captures the notion of optimization with respect to strategies that are risk-averse (i.e., ensure certain probabilistic guarantee). Our main results are as follows: First, we present algorithms for the decision problems which are always polynomial in the size of the MDP. We also show that an approximation of the Pareto-curve can be computed in time polynomial in the size of the MDP, and the approximation factor, but exponential in the number of dimensions. Second, we present a complete characterization of the strategy complexity (in terms of memory bounds and randomization) required to solve our problem. "}],"publication_status":"published","publisher":"International Federation of Computational Logic","date_published":"2017-07-03T00:00:00Z","department":[{"_id":"KrCh"}],"quality_controlled":"1","volume":13,"project":[{"name":"International IST Postdoc Fellowship Programme","call_identifier":"FP7","_id":"25681D80-B435-11E9-9278-68D0E5697425","grant_number":"291734"},{"_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23","call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"call_identifier":"H2020","name":"Atomic-Resolution Structures of Mitochondrial Respiratory Chain Supercomplexes (H2020)","grant_number":"701309","_id":"2590DB08-B435-11E9-9278-68D0E5697425"}],"ec_funded":1,"related_material":{"record":[{"relation":"earlier_version","id":"1657","status":"public"},{"status":"public","relation":"earlier_version","id":"5429"},{"status":"public","relation":"earlier_version","id":"5435"}]},"article_number":"15","year":"2017","citation":{"apa":"Chatterjee, K., Křetínská, Z., &#38; Kretinsky, J. (2017). Unifying two views on multiple mean-payoff objectives in Markov decision processes. <i>Logical Methods in Computer Science</i>. International Federation of Computational Logic. <a href=\"https://doi.org/10.23638/LMCS-13(2:15)2017\">https://doi.org/10.23638/LMCS-13(2:15)2017</a>","chicago":"Chatterjee, Krishnendu, Zuzana Křetínská, and Jan Kretinsky. “Unifying Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes.” <i>Logical Methods in Computer Science</i>. International Federation of Computational Logic, 2017. <a href=\"https://doi.org/10.23638/LMCS-13(2:15)2017\">https://doi.org/10.23638/LMCS-13(2:15)2017</a>.","ista":"Chatterjee K, Křetínská Z, Kretinsky J. 2017. Unifying two views on multiple mean-payoff objectives in Markov decision processes. Logical Methods in Computer Science. 13(2), 15.","mla":"Chatterjee, Krishnendu, et al. “Unifying Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes.” <i>Logical Methods in Computer Science</i>, vol. 13, no. 2, 15, International Federation of Computational Logic, 2017, doi:<a href=\"https://doi.org/10.23638/LMCS-13(2:15)2017\">10.23638/LMCS-13(2:15)2017</a>.","ieee":"K. Chatterjee, Z. Křetínská, and J. Kretinsky, “Unifying two views on multiple mean-payoff objectives in Markov decision processes,” <i>Logical Methods in Computer Science</i>, vol. 13, no. 2. International Federation of Computational Logic, 2017.","ama":"Chatterjee K, Křetínská Z, Kretinsky J. Unifying two views on multiple mean-payoff objectives in Markov decision processes. <i>Logical Methods in Computer Science</i>. 2017;13(2). doi:<a href=\"https://doi.org/10.23638/LMCS-13(2:15)2017\">10.23638/LMCS-13(2:15)2017</a>","short":"K. Chatterjee, Z. Křetínská, J. Kretinsky, Logical Methods in Computer Science 13 (2017)."},"publist_id":"7355","date_created":"2018-12-11T11:46:38Z","doi":"10.23638/LMCS-13(2:15)2017","file_date_updated":"2020-07-14T12:46:33Z","_id":"466","publication_identifier":{"issn":["18605974"]},"month":"07","oa_version":"Published Version","day":"03","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","file":[{"relation":"main_file","file_size":511832,"content_type":"application/pdf","access_level":"open_access","creator":"system","date_updated":"2020-07-14T12:46:33Z","date_created":"2018-12-12T10:18:32Z","file_id":"5354","checksum":"bfa405385ec6229ad5ead89ab5751639","file_name":"IST-2018-957-v1+1_2017_Chatterjee_Unifying_two.pdf"}],"author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu"},{"first_name":"Zuzana","full_name":"Křetínská, Zuzana","last_name":"Křetínská"},{"orcid":"0000-0002-8122-2881","last_name":"Kretinsky","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","full_name":"Kretinsky, Jan","first_name":"Jan"}],"type":"journal_article","status":"public","scopus_import":1,"has_accepted_license":"1","intvolume":"        13","oa":1,"pubrep_id":"957","date_updated":"2023-02-23T12:26:16Z","issue":"2","title":"Unifying two views on multiple mean-payoff objectives in Markov decision processes","publication":"Logical Methods in Computer Science","language":[{"iso":"eng"}]},{"publication":"Logical Methods in Computer Science","language":[{"iso":"eng"}],"scopus_import":1,"has_accepted_license":"1","intvolume":"        10","oa":1,"date_updated":"2021-01-12T06:56:11Z","pubrep_id":"389","issue":"1","title":"Exact and approximate determinization of discounted-sum automata","status":"public","type":"journal_article","publication_identifier":{"issn":["18605974"]},"month":"02","oa_version":"Published Version","day":"13","file":[{"checksum":"9f6ea2e2d8d4a32ff0becc29d835bbf8","file_id":"4643","file_name":"IST-2015-389-v1+1_1401.3957.pdf","date_created":"2018-12-12T10:07:45Z","date_updated":"2020-07-14T12:45:34Z","creator":"system","relation":"main_file","access_level":"open_access","file_size":550936,"content_type":"application/pdf"}],"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","author":[{"last_name":"Boker","full_name":"Boker, Udi","first_name":"Udi"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","first_name":"Thomas A"}],"doi":"10.2168/LMCS-10(1:10)2014","file_date_updated":"2020-07-14T12:45:34Z","_id":"2233","ec_funded":1,"year":"2014","citation":{"ama":"Boker U, Henzinger TA. Exact and approximate determinization of discounted-sum automata. <i>Logical Methods in Computer Science</i>. 2014;10(1). doi:<a href=\"https://doi.org/10.2168/LMCS-10(1:10)2014\">10.2168/LMCS-10(1:10)2014</a>","ieee":"U. Boker and T. A. Henzinger, “Exact and approximate determinization of discounted-sum automata,” <i>Logical Methods in Computer Science</i>, vol. 10, no. 1. International Federation of Computational Logic, 2014.","short":"U. Boker, T.A. Henzinger, Logical Methods in Computer Science 10 (2014).","mla":"Boker, Udi, and Thomas A. Henzinger. “Exact and Approximate Determinization of Discounted-Sum Automata.” <i>Logical Methods in Computer Science</i>, vol. 10, no. 1, International Federation of Computational Logic, 2014, doi:<a href=\"https://doi.org/10.2168/LMCS-10(1:10)2014\">10.2168/LMCS-10(1:10)2014</a>.","ista":"Boker U, Henzinger TA. 2014. Exact and approximate determinization of discounted-sum automata. Logical Methods in Computer Science. 10(1).","chicago":"Boker, Udi, and Thomas A Henzinger. “Exact and Approximate Determinization of Discounted-Sum Automata.” <i>Logical Methods in Computer Science</i>. International Federation of Computational Logic, 2014. <a href=\"https://doi.org/10.2168/LMCS-10(1:10)2014\">https://doi.org/10.2168/LMCS-10(1:10)2014</a>.","apa":"Boker, U., &#38; Henzinger, T. A. (2014). Exact and approximate determinization of discounted-sum automata. <i>Logical Methods in Computer Science</i>. International Federation of Computational Logic. <a href=\"https://doi.org/10.2168/LMCS-10(1:10)2014\">https://doi.org/10.2168/LMCS-10(1:10)2014</a>"},"publist_id":"4728","date_created":"2018-12-11T11:56:28Z","publisher":"International Federation of Computational Logic","date_published":"2014-02-13T00:00:00Z","department":[{"_id":"ToHe"}],"volume":10,"quality_controlled":"1","project":[{"call_identifier":"FWF","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23"},{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989","name":"Quantitative Reactive Modeling","call_identifier":"FP7"}],"ddc":["000"],"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)","image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"abstract":[{"lang":"eng","text":" A discounted-sum automaton (NDA) is a nondeterministic finite automaton with edge weights, valuing a run by the discounted sum of visited edge weights. More precisely, the weight in the i-th position of the run is divided by λi, where the discount factor λ is a fixed rational number greater than 1. The value of a word is the minimal value of the automaton runs on it. Discounted summation is a common and useful measuring scheme, especially for infinite sequences, reflecting the assumption that earlier weights are more important than later weights. Unfortunately, determinization of NDAs, which is often essential in formal verification, is, in general, not possible. We provide positive news, showing that every NDA with an integral discount factor is determinizable. We complete the picture by proving that the integers characterize exactly the discount factors that guarantee determinizability: for every nonintegral rational discount factor λ, there is a nondeterminizable λ-NDA. We also prove that the class of NDAs with integral discount factors enjoys closure under the algebraic operations min, max, addition, and subtraction, which is not the case for general NDAs nor for deterministic NDAs. For general NDAs, we look into approximate determinization, which is always possible as the influence of a word's suffix decays. We show that the naive approach, of unfolding the automaton computations up to a sufficient level, is doubly exponential in the discount factor. We provide an alternative construction for approximate determinization, which is singly exponential in the discount factor, in the precision, and in the number of states. We also prove matching lower bounds, showing that the exponential dependency on each of these three parameters cannot be avoided. All our results hold equally for automata over finite words and for automata over infinite words. "}],"publication_status":"published"},{"author":[{"full_name":"Brázdil, Tomáš","first_name":"Tomáš","last_name":"Brázdil"},{"last_name":"Brožek","first_name":"Václav","full_name":"Brožek, Václav"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu"},{"first_name":"Vojtěch","full_name":"Forejt, Vojtěch","last_name":"Forejt"},{"first_name":"Antonín","full_name":"Kučera, Antonín","last_name":"Kučera"}],"day":"14","main_file_link":[{"open_access":"1","url":"http://repository.ist.ac.at/id/eprint/428"}],"oa_version":"Published Version","user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","file":[{"checksum":"803edcc2d8c1acfba44a9ec43a5eb9f0","file_name":"IST-2016-428-v1+1_1104.3489.pdf","file_id":"4656","date_updated":"2020-07-14T12:45:34Z","date_created":"2018-12-12T10:07:57Z","creator":"system","access_level":"open_access","relation":"main_file","content_type":"application/pdf","file_size":375388}],"publication_identifier":{"issn":["18605974"]},"month":"02","status":"public","type":"journal_article","title":"Markov decision processes with multiple long-run average objectives","oa":1,"pubrep_id":"428","date_updated":"2021-01-12T06:56:11Z","issue":"1","intvolume":"        10","scopus_import":1,"has_accepted_license":"1","language":[{"iso":"eng"}],"publication":"Logical Methods in Computer Science","publication_status":"published","abstract":[{"lang":"eng","text":"We study Markov decision processes (MDPs) with multiple limit-average (or mean-payoff) functions. We consider two different objectives, namely, expectation and satisfaction objectives. Given an MDP with κ limit-average functions, in the expectation objective the goal is to maximize the expected limit-average value, and in the satisfaction objective the goal is to maximize the probability of runs such that the limit-average value stays above a given vector. We show that under the expectation objective, in contrast to the case of one limit-average function, both randomization and memory are necessary for strategies even for ε-approximation, and that finite-memory randomized strategies are sufficient for achieving Pareto optimal values. Under the satisfaction objective, in contrast to the case of one limit-average function, infinite memory is necessary for strategies achieving a specific value (i.e. randomized finite-memory strategies are not sufficient), whereas memoryless randomized strategies are sufficient for ε-approximation, for all ε &gt; 0. We further prove that the decision problems for both expectation and satisfaction objectives can be solved in polynomial time and the trade-off curve (Pareto curve) can be ε-approximated in time polynomial in the size of the MDP and 1/ε, and exponential in the number of limit-average functions, for all ε &gt; 0. Our analysis also reveals flaws in previous work for MDPs with multiple mean-payoff functions under the expectation objective, corrects the flaws, and allows us to obtain improved results."}],"ddc":["000"],"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)","image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"project":[{"call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"name":"Game Theory","call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425","grant_number":"S11407"},{"name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"department":[{"_id":"KrCh"}],"volume":10,"quality_controlled":"1","publisher":"International Federation of Computational Logic","date_published":"2014-02-14T00:00:00Z","publist_id":"4727","citation":{"apa":"Brázdil, T., Brožek, V., Chatterjee, K., Forejt, V., &#38; Kučera, A. (2014). Markov decision processes with multiple long-run average objectives. <i>Logical Methods in Computer Science</i>. International Federation of Computational Logic. <a href=\"https://doi.org/10.2168/LMCS-10(1:13)2014\">https://doi.org/10.2168/LMCS-10(1:13)2014</a>","chicago":"Brázdil, Tomáš, Václav Brožek, Krishnendu Chatterjee, Vojtěch Forejt, and Antonín Kučera. “Markov Decision Processes with Multiple Long-Run Average Objectives.” <i>Logical Methods in Computer Science</i>. International Federation of Computational Logic, 2014. <a href=\"https://doi.org/10.2168/LMCS-10(1:13)2014\">https://doi.org/10.2168/LMCS-10(1:13)2014</a>.","ista":"Brázdil T, Brožek V, Chatterjee K, Forejt V, Kučera A. 2014. Markov decision processes with multiple long-run average objectives. Logical Methods in Computer Science. 10(1).","mla":"Brázdil, Tomáš, et al. “Markov Decision Processes with Multiple Long-Run Average Objectives.” <i>Logical Methods in Computer Science</i>, vol. 10, no. 1, International Federation of Computational Logic, 2014, doi:<a href=\"https://doi.org/10.2168/LMCS-10(1:13)2014\">10.2168/LMCS-10(1:13)2014</a>.","short":"T. Brázdil, V. Brožek, K. Chatterjee, V. Forejt, A. Kučera, Logical Methods in Computer Science 10 (2014).","ieee":"T. Brázdil, V. Brožek, K. Chatterjee, V. Forejt, and A. Kučera, “Markov decision processes with multiple long-run average objectives,” <i>Logical Methods in Computer Science</i>, vol. 10, no. 1. International Federation of Computational Logic, 2014.","ama":"Brázdil T, Brožek V, Chatterjee K, Forejt V, Kučera A. Markov decision processes with multiple long-run average objectives. <i>Logical Methods in Computer Science</i>. 2014;10(1). doi:<a href=\"https://doi.org/10.2168/LMCS-10(1:13)2014\">10.2168/LMCS-10(1:13)2014</a>"},"date_created":"2018-12-11T11:56:29Z","year":"2014","ec_funded":1,"file_date_updated":"2020-07-14T12:45:34Z","_id":"2234","doi":"10.2168/LMCS-10(1:13)2014"}]