[{"day":"30","author":[{"id":"4A55BD00-F248-11E8-B48F-1D18A9856A87","full_name":"Aminof, Benjamin","last_name":"Aminof","first_name":"Benjamin"},{"last_name":"Jacobs","first_name":"Swen","full_name":"Jacobs, Swen"},{"last_name":"Khalimov","first_name":"Ayrat","full_name":"Khalimov, Ayrat"},{"full_name":"Rubin, Sasha","id":"2EC51194-F248-11E8-B48F-1D18A9856A87","first_name":"Sasha","last_name":"Rubin"}],"title":"Parameterized model checking of token-passing systems","arxiv":1,"department":[{"_id":"KrCh"}],"publisher":"Springer Nature","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","article_processing_charge":"No","ec_funded":1,"scopus_import":"1","publication":"Verification, Model Checking, and Abstract Interpretation","publication_identifier":{"issn":["0302-9743"],"eisbn":["9783642540134"],"isbn":["9783642540127"],"eissn":["1611-3349"]},"quality_controlled":"1","doi":"10.1007/978-3-642-54013-4_15","project":[{"grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425","name":"Game Theory","grant_number":"S11407"},{"name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307"}],"language":[{"iso":"eng"}],"conference":{"end_date":"2014-01-21","start_date":"2014-01-19","name":"VMCAI: Verifcation, Model Checking, and Abstract Interpretation","location":"San Diego, CA, United States"},"type":"conference","month":"01","oa_version":"Preprint","abstract":[{"text":"We revisit the parameterized model checking problem for token-passing systems and specifications in indexed CTL  ∗ \\X. Emerson and Namjoshi (1995, 2003) have shown that parameterized model checking of indexed CTL  ∗ \\X in uni-directional token rings can be reduced to checking rings up to some cutoff size. Clarke et al. (2004) have shown a similar result for general topologies and indexed LTL \\X, provided processes cannot choose the directions for sending or receiving the token.\r\nWe unify and substantially extend these results by systematically exploring fragments of indexed CTL  ∗ \\X with respect to general topologies. For each fragment we establish whether a cutoff exists, and for some concrete topologies, such as rings, cliques and stars, we infer small cutoffs. Finally, we show that the problem becomes undecidable, and thus no cutoffs exist, if processes are allowed to choose the directions in which they send or from which they receive the token.","lang":"eng"}],"date_updated":"2022-05-17T08:36:01Z","page":"262-281","date_created":"2022-03-18T13:01:22Z","volume":8318,"year":"2014","acknowledgement":"This work was supported by the Austrian Science Fund through grant P23499-N23\r\nand through the RiSE network (S11403, S11405, S11406, S11407-N23); ERC Starting Grant (279307: Graph Games); Vienna Science and Technology Fund (WWTF)\r\ngrants PROSEED, ICT12-059, and VRG11-005.","_id":"10884","oa":1,"publication_status":"published","main_file_link":[{"open_access":"1","url":" https://doi.org/10.48550/arXiv.1311.4425"}],"date_published":"2014-01-30T00:00:00Z","external_id":{"arxiv":["1311.4425"]},"status":"public","alternative_title":["LNCS"],"citation":{"ieee":"B. Aminof, S. Jacobs, A. Khalimov, and S. Rubin, “Parameterized model checking of token-passing systems,” in <i>Verification, Model Checking, and Abstract Interpretation</i>, San Diego, CA, United States, 2014, vol. 8318, pp. 262–281.","chicago":"Aminof, Benjamin, Swen Jacobs, Ayrat Khalimov, and Sasha Rubin. “Parameterized Model Checking of Token-Passing Systems.” In <i>Verification, Model Checking, and Abstract Interpretation</i>, 8318:262–81. Springer Nature, 2014. <a href=\"https://doi.org/10.1007/978-3-642-54013-4_15\">https://doi.org/10.1007/978-3-642-54013-4_15</a>.","short":"B. Aminof, S. Jacobs, A. Khalimov, S. Rubin, in:, Verification, Model Checking, and Abstract Interpretation, Springer Nature, 2014, pp. 262–281.","ama":"Aminof B, Jacobs S, Khalimov A, Rubin S. Parameterized model checking of token-passing systems. In: <i>Verification, Model Checking, and Abstract Interpretation</i>. Vol 8318. Springer Nature; 2014:262-281. doi:<a href=\"https://doi.org/10.1007/978-3-642-54013-4_15\">10.1007/978-3-642-54013-4_15</a>","ista":"Aminof B, Jacobs S, Khalimov A, Rubin S. 2014. Parameterized model checking of token-passing systems. Verification, Model Checking, and Abstract Interpretation. VMCAI: Verifcation, Model Checking, and Abstract Interpretation, LNCS, vol. 8318, 262–281.","mla":"Aminof, Benjamin, et al. “Parameterized Model Checking of Token-Passing Systems.” <i>Verification, Model Checking, and Abstract Interpretation</i>, vol. 8318, Springer Nature, 2014, pp. 262–81, doi:<a href=\"https://doi.org/10.1007/978-3-642-54013-4_15\">10.1007/978-3-642-54013-4_15</a>.","apa":"Aminof, B., Jacobs, S., Khalimov, A., &#38; Rubin, S. (2014). Parameterized model checking of token-passing systems. In <i>Verification, Model Checking, and Abstract Interpretation</i> (Vol. 8318, pp. 262–281). San Diego, CA, United States: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-642-54013-4_15\">https://doi.org/10.1007/978-3-642-54013-4_15</a>"},"intvolume":"      8318"},{"status":"public","citation":{"mla":"Grinshpun, Andrey, et al. “Alternating Traps in Muller and Parity Games.” <i>Theoretical Computer Science</i>, vol. 521, Elsevier, 2014, pp. 73–91, doi:<a href=\"https://doi.org/10.1016/j.tcs.2013.11.032\">10.1016/j.tcs.2013.11.032</a>.","ista":"Grinshpun A, Phalitnonkiat P, Rubin S, Tarfulea A. 2014. Alternating traps in Muller and parity games. Theoretical Computer Science. 521, 73–91.","apa":"Grinshpun, A., Phalitnonkiat, P., Rubin, S., &#38; Tarfulea, A. (2014). Alternating traps in Muller and parity games. <i>Theoretical Computer Science</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.tcs.2013.11.032\">https://doi.org/10.1016/j.tcs.2013.11.032</a>","ama":"Grinshpun A, Phalitnonkiat P, Rubin S, Tarfulea A. Alternating traps in Muller and parity games. <i>Theoretical Computer Science</i>. 2014;521:73-91. doi:<a href=\"https://doi.org/10.1016/j.tcs.2013.11.032\">10.1016/j.tcs.2013.11.032</a>","short":"A. Grinshpun, P. Phalitnonkiat, S. Rubin, A. Tarfulea, Theoretical Computer Science 521 (2014) 73–91.","ieee":"A. Grinshpun, P. Phalitnonkiat, S. Rubin, and A. Tarfulea, “Alternating traps in Muller and parity games,” <i>Theoretical Computer Science</i>, vol. 521. Elsevier, pp. 73–91, 2014.","chicago":"Grinshpun, Andrey, Pakawat Phalitnonkiat, Sasha Rubin, and Andrei Tarfulea. “Alternating Traps in Muller and Parity Games.” <i>Theoretical Computer Science</i>. Elsevier, 2014. <a href=\"https://doi.org/10.1016/j.tcs.2013.11.032\">https://doi.org/10.1016/j.tcs.2013.11.032</a>."},"language":[{"iso":"eng"}],"intvolume":"       521","publication_identifier":{"issn":["03043975"]},"oa":1,"publication_status":"published","quality_controlled":"1","main_file_link":[{"url":"http://arxiv.org/abs/1303.3777","open_access":"1"}],"doi":"10.1016/j.tcs.2013.11.032","date_published":"2014-02-13T00:00:00Z","year":"2014","department":[{"_id":"KrCh"}],"user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","publisher":"Elsevier","scopus_import":1,"_id":"2246","publication":"Theoretical Computer Science","month":"02","oa_version":"Submitted Version","type":"journal_article","date_updated":"2021-01-12T06:56:16Z","day":"13","abstract":[{"text":"Muller games are played by two players moving a token along a graph; the winner is determined by the set of vertices that occur infinitely often. The central algorithmic problem is to compute the winning regions for the players. Different classes and representations of Muller games lead to problems of varying computational complexity. One such class are parity games; these are of particular significance in computational complexity, as they remain one of the few combinatorial problems known to be in NP ∩ co-NP but not known to be in P. We show that winning regions for a Muller game can be determined from the alternating structure of its traps. To every Muller game we then associate a natural number that we call its trap depth; this parameter measures how complicated the trap structure is. We present algorithms for parity games that run in polynomial time for graphs of bounded trap depth, and in general run in time exponential in the trap depth. ","lang":"eng"}],"page":"73 - 91","author":[{"first_name":"Andrey","last_name":"Grinshpun","full_name":"Grinshpun, Andrey"},{"full_name":"Phalitnonkiat, Pakawat","first_name":"Pakawat","last_name":"Phalitnonkiat"},{"full_name":"Rubin, Sasha","id":"2EC51194-F248-11E8-B48F-1D18A9856A87","first_name":"Sasha","last_name":"Rubin"},{"full_name":"Tarfulea, Andrei","last_name":"Tarfulea","first_name":"Andrei"}],"publist_id":"4703","date_created":"2018-12-11T11:56:33Z","volume":521,"title":"Alternating traps in Muller and parity games"},{"year":"2014","_id":"475","page":"83 - 90","abstract":[{"lang":"eng","text":"First cycle games (FCG) are played on a finite graph by two players who push a token along the edges until a vertex is repeated, and a simple cycle is formed. The winner is determined by some fixed property Y of the sequence of labels of the edges (or nodes) forming this cycle. These games are traditionally of interest because of their connection with infinite-duration games such as parity and mean-payoff games. We study the memory requirements for winning strategies of FCGs and certain associated infinite duration games. We exhibit a simple FCG that is not memoryless determined (this corrects a mistake in Memoryless determinacy of parity and mean payoff games: a simple proof by Bj⋯orklund, Sandberg, Vorobyov (2004) that claims that FCGs for which Y is closed under cyclic permutations are memoryless determined). We show that θ (n)! memory (where n is the number of nodes in the graph), which is always sufficient, may be necessary to win some FCGs. On the other hand, we identify easy to check conditions on Y (i.e., Y is closed under cyclic permutations, and both Y and its complement are closed under concatenation) that are sufficient to ensure that the corresponding FCGs and their associated infinite duration games are memoryless determined. We demonstrate that many games considered in the literature, such as mean-payoff, parity, energy, etc., satisfy these conditions. On the complexity side, we show (for efficiently computable Y) that while solving FCGs is in PSPACE, solving some families of FCGs is PSPACE-hard. "}],"date_updated":"2021-01-12T08:00:53Z","month":"04","oa_version":"Published Version","type":"conference","volume":146,"file_date_updated":"2020-07-14T12:46:35Z","date_created":"2018-12-11T11:46:41Z","alternative_title":["EPTCS"],"status":"public","intvolume":"       146","citation":{"ieee":"B. Aminof and S. Rubin, “First cycle games,” in <i>Electronic Proceedings in Theoretical Computer Science, EPTCS</i>, Grenoble, France, 2014, vol. 146, pp. 83–90.","chicago":"Aminof, Benjamin, and Sasha Rubin. “First Cycle Games.” In <i>Electronic Proceedings in Theoretical Computer Science, EPTCS</i>, 146:83–90. Open Publishing Association, 2014. <a href=\"https://doi.org/10.4204/EPTCS.146.11\">https://doi.org/10.4204/EPTCS.146.11</a>.","short":"B. Aminof, S. Rubin, in:, Electronic Proceedings in Theoretical Computer Science, EPTCS, Open Publishing Association, 2014, pp. 83–90.","ama":"Aminof B, Rubin S. First cycle games. In: <i>Electronic Proceedings in Theoretical Computer Science, EPTCS</i>. Vol 146. Open Publishing Association; 2014:83-90. doi:<a href=\"https://doi.org/10.4204/EPTCS.146.11\">10.4204/EPTCS.146.11</a>","mla":"Aminof, Benjamin, and Sasha Rubin. “First Cycle Games.” <i>Electronic Proceedings in Theoretical Computer Science, EPTCS</i>, vol. 146, Open Publishing Association, 2014, pp. 83–90, doi:<a href=\"https://doi.org/10.4204/EPTCS.146.11\">10.4204/EPTCS.146.11</a>.","ista":"Aminof B, Rubin S. 2014. First cycle games. Electronic Proceedings in Theoretical Computer Science, EPTCS. SR: Strategic Reasoning, EPTCS, vol. 146, 83–90.","apa":"Aminof, B., &#38; Rubin, S. (2014). First cycle games. In <i>Electronic Proceedings in Theoretical Computer Science, EPTCS</i> (Vol. 146, pp. 83–90). Grenoble, France: Open Publishing Association. <a href=\"https://doi.org/10.4204/EPTCS.146.11\">https://doi.org/10.4204/EPTCS.146.11</a>"},"publication_status":"published","oa":1,"has_accepted_license":"1","ddc":["004"],"date_published":"2014-04-01T00:00:00Z","publisher":"Open Publishing Association","user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","department":[{"_id":"KrCh"}],"publication":"Electronic Proceedings in Theoretical Computer Science, EPTCS","ec_funded":1,"scopus_import":1,"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"author":[{"last_name":"Aminof","first_name":"Benjamin","id":"4A55BD00-F248-11E8-B48F-1D18A9856A87","full_name":"Aminof, Benjamin"},{"last_name":"Rubin","first_name":"Sasha","id":"2EC51194-F248-11E8-B48F-1D18A9856A87","full_name":"Rubin, Sasha"}],"day":"01","file":[{"access_level":"open_access","date_created":"2018-12-12T10:17:08Z","checksum":"4d7b4ab82980cca2b96ac7703992a8c8","date_updated":"2020-07-14T12:46:35Z","file_id":"5260","creator":"system","content_type":"application/pdf","relation":"main_file","file_size":100115,"file_name":"IST-2018-952-v1+1_2014_Rubin_First_cycle.pdf"}],"title":"First cycle games","publist_id":"7345","project":[{"grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"name":"Moderne Concurrency Paradigms","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S11402-N23"},{"grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Game Theory"},{"name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"279307"},{"name":"Efficient Algorithms for Computer Aided Verification","_id":"25892FC0-B435-11E9-9278-68D0E5697425","grant_number":"ICT15-003"}],"conference":{"start_date":"2014-04-05","name":"SR: Strategic Reasoning","location":"Grenoble, France","end_date":"2014-04-06"},"language":[{"iso":"eng"}],"pubrep_id":"952","doi":"10.4204/EPTCS.146.11","quality_controlled":"1"},{"month":"04","type":"conference","oa_version":"None","abstract":[{"lang":"eng","text":"We consider how to edit strings from a source language so that the edited strings belong to a target language, where the languages are given as deterministic finite automata. Non-streaming (or offline) transducers perform edits given the whole source string. We show that the class of deterministic one-pass transducers with registers along with increment and min operation suffices for computing optimal edit distance, whereas the same class of transducers without the min operation is not sufficient. Streaming (or online) transducers perform edits as the letters of the source string are received. We present a polynomial time algorithm for the partial-repair problem that given a bound α asks for the construction of a deterministic streaming transducer (if one exists) that ensures that the ‘maximum fraction’ η of the strings of the source language are edited, within cost α, to the target language."}],"date_updated":"2023-09-05T15:10:38Z","page":"214-225","date_created":"2022-03-21T07:56:21Z","volume":7810,"year":"2013","acknowledgement":"The research was supported by Austrian Science Fund (FWF) Grant No P 23499-N23, FWF NFN Grant No S11407-N23 (RiSE), ERC Start grant (279307: Graph Games), and Microsoft faculty fellows award. Thanks to Gabriele Puppis for suggesting the problem of identifying a deterministic transducer to compute the optimal cost, and to Martin Chmelik for his comments on the introduction.","_id":"10902","publication_status":"published","date_published":"2013-04-15T00:00:00Z","status":"public","alternative_title":["LNCS"],"citation":{"ieee":"K. Chatterjee, S. Chaubal, and S. Rubin, “How to travel between languages,” in <i>7th International Conference on Language and Automata Theory and Applications</i>, Bilbao, Spain, 2013, vol. 7810, pp. 214–225.","chicago":"Chatterjee, Krishnendu, Siddhesh Chaubal, and Sasha Rubin. “How to Travel between Languages.” In <i>7th International Conference on Language and Automata Theory and Applications</i>, 7810:214–25. LNCS. Berlin, Heidelberg: Springer Nature, 2013. <a href=\"https://doi.org/10.1007/978-3-642-37064-9_20\">https://doi.org/10.1007/978-3-642-37064-9_20</a>.","short":"K. Chatterjee, S. Chaubal, S. Rubin, in:, 7th International Conference on Language and Automata Theory and Applications, Springer Nature, Berlin, Heidelberg, 2013, pp. 214–225.","ama":"Chatterjee K, Chaubal S, Rubin S. How to travel between languages. In: <i>7th International Conference on Language and Automata Theory and Applications</i>. Vol 7810. LNCS. Berlin, Heidelberg: Springer Nature; 2013:214-225. doi:<a href=\"https://doi.org/10.1007/978-3-642-37064-9_20\">10.1007/978-3-642-37064-9_20</a>","mla":"Chatterjee, Krishnendu, et al. “How to Travel between Languages.” <i>7th International Conference on Language and Automata Theory and Applications</i>, vol. 7810, Springer Nature, 2013, pp. 214–25, doi:<a href=\"https://doi.org/10.1007/978-3-642-37064-9_20\">10.1007/978-3-642-37064-9_20</a>.","ista":"Chatterjee K, Chaubal S, Rubin S. 2013. How to travel between languages. 7th International Conference on Language and Automata Theory and Applications. LATA: Conference on Language and Automata Theory and ApplicationsLNCS, LNCS, vol. 7810, 214–225.","apa":"Chatterjee, K., Chaubal, S., &#38; Rubin, S. (2013). How to travel between languages. In <i>7th International Conference on Language and Automata Theory and Applications</i> (Vol. 7810, pp. 214–225). Berlin, Heidelberg: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-642-37064-9_20\">https://doi.org/10.1007/978-3-642-37064-9_20</a>"},"intvolume":"      7810","day":"15","author":[{"first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu"},{"last_name":"Chaubal","first_name":"Siddhesh","full_name":"Chaubal, Siddhesh"},{"id":"2EC51194-F248-11E8-B48F-1D18A9856A87","full_name":"Rubin, Sasha","last_name":"Rubin","first_name":"Sasha"}],"title":"How to travel between languages","department":[{"_id":"KrCh"}],"place":"Berlin, Heidelberg","publisher":"Springer Nature","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","article_processing_charge":"No","scopus_import":"1","ec_funded":1,"publication":"7th International Conference on Language and Automata Theory and Applications","publication_identifier":{"issn":["0302-9743"],"eisbn":["9783642370649"],"isbn":["9783642370632"],"eissn":["1611-3349"]},"quality_controlled":"1","doi":"10.1007/978-3-642-37064-9_20","project":[{"grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Game Theory"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"language":[{"iso":"eng"}],"conference":{"location":"Bilbao, Spain","name":"LATA: Conference on Language and Automata Theory and Applications","start_date":"2013-04-02","end_date":"2013-04-05"},"series_title":"LNCS"},{"title":"A Myhill Nerode theorem for automata with advice","publist_id":"7325","author":[{"full_name":"Kruckman, Alex","first_name":"Alex","last_name":"Kruckman"},{"first_name":"Sasha","last_name":"Rubin","full_name":"Rubin, Sasha","id":"2EC51194-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Sheridan","first_name":"John","full_name":"Sheridan, John"},{"last_name":"Zax","first_name":"Ben","full_name":"Zax, Ben"}],"file":[{"access_level":"open_access","date_created":"2018-12-12T10:15:31Z","checksum":"56277f95edc9d531fa3bdc5f9579fda8","file_id":"5152","date_updated":"2020-07-14T12:46:35Z","creator":"system","file_size":97736,"relation":"main_file","content_type":"application/pdf","file_name":"IST-2018-944-v1+1_2012_Rubin_A_Myhill.pdf"}],"day":"07","publication":"Proceedings GandALF 2012","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"scopus_import":1,"ec_funded":1,"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","publisher":"Open Publishing Association","department":[{"_id":"KrCh"}],"doi":"10.4204/EPTCS.96.18","quality_controlled":"1","pubrep_id":"944","conference":{"name":"GandALF: Games, Automata, Logics and Formal Verification","location":"Napoli, Italy","start_date":"2012-09-06","end_date":"2012-09-08"},"language":[{"iso":"eng"}],"project":[{"name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23"},{"call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307"}],"volume":96,"file_date_updated":"2020-07-14T12:46:35Z","date_created":"2018-12-11T11:46:47Z","page":"238 - 246","month":"10","oa_version":"Published Version","type":"conference","date_updated":"2021-01-12T08:01:04Z","abstract":[{"lang":"eng","text":"An automaton with advice is a finite state automaton which has access to an additional fixed infinite string called an advice tape. We refine the Myhill-Nerode theorem to characterize the languages of finite strings that are accepted by automata with advice. We do the same for tree automata with advice."}],"_id":"495","year":"2012","ddc":["004"],"date_published":"2012-10-07T00:00:00Z","oa":1,"publication_status":"published","has_accepted_license":"1","intvolume":"        96","citation":{"apa":"Kruckman, A., Rubin, S., Sheridan, J., &#38; Zax, B. (2012). A Myhill Nerode theorem for automata with advice. In <i>Proceedings GandALF 2012</i> (Vol. 96, pp. 238–246). Napoli, Italy: Open Publishing Association. <a href=\"https://doi.org/10.4204/EPTCS.96.18\">https://doi.org/10.4204/EPTCS.96.18</a>","ista":"Kruckman A, Rubin S, Sheridan J, Zax B. 2012. A Myhill Nerode theorem for automata with advice. Proceedings GandALF 2012. GandALF: Games, Automata, Logics and Formal Verification, EPTCS, vol. 96, 238–246.","mla":"Kruckman, Alex, et al. “A Myhill Nerode Theorem for Automata with Advice.” <i>Proceedings GandALF 2012</i>, vol. 96, Open Publishing Association, 2012, pp. 238–46, doi:<a href=\"https://doi.org/10.4204/EPTCS.96.18\">10.4204/EPTCS.96.18</a>.","ama":"Kruckman A, Rubin S, Sheridan J, Zax B. A Myhill Nerode theorem for automata with advice. In: <i>Proceedings GandALF 2012</i>. Vol 96. Open Publishing Association; 2012:238-246. doi:<a href=\"https://doi.org/10.4204/EPTCS.96.18\">10.4204/EPTCS.96.18</a>","short":"A. Kruckman, S. Rubin, J. Sheridan, B. Zax, in:, Proceedings GandALF 2012, Open Publishing Association, 2012, pp. 238–246.","chicago":"Kruckman, Alex, Sasha Rubin, John Sheridan, and Ben Zax. “A Myhill Nerode Theorem for Automata with Advice.” In <i>Proceedings GandALF 2012</i>, 96:238–46. Open Publishing Association, 2012. <a href=\"https://doi.org/10.4204/EPTCS.96.18\">https://doi.org/10.4204/EPTCS.96.18</a>.","ieee":"A. Kruckman, S. Rubin, J. Sheridan, and B. Zax, “A Myhill Nerode theorem for automata with advice,” in <i>Proceedings GandALF 2012</i>, Napoli, Italy, 2012, vol. 96, pp. 238–246."},"alternative_title":["EPTCS"],"status":"public"},{"quality_controlled":"1","main_file_link":[{"url":"https://arise.or.at/pubpdf/Interpretations_in_Trees_with_Countably_Many_Branches.pdf","open_access":"1"}],"doi":"10.1109/LICS.2012.65","date_published":"2012-01-01T00:00:00Z","oa":1,"publication_status":"published","citation":{"chicago":"Rabinovich, Alexander, and Sasha Rubin. “Interpretations in Trees with Countably Many Branches.” IEEE, 2012. <a href=\"https://doi.org/10.1109/LICS.2012.65\">https://doi.org/10.1109/LICS.2012.65</a>.","ieee":"A. Rabinovich and S. Rubin, “Interpretations in trees with countably many branches,” presented at the LICS: Symposium on Logic in Computer Science, Dubrovnik, Croatia, 2012.","short":"A. Rabinovich, S. Rubin, in:, IEEE, 2012.","ama":"Rabinovich A, Rubin S. Interpretations in trees with countably many branches. In: IEEE; 2012. doi:<a href=\"https://doi.org/10.1109/LICS.2012.65\">10.1109/LICS.2012.65</a>","apa":"Rabinovich, A., &#38; Rubin, S. (2012). Interpretations in trees with countably many branches. Presented at the LICS: Symposium on Logic in Computer Science, Dubrovnik, Croatia: IEEE. <a href=\"https://doi.org/10.1109/LICS.2012.65\">https://doi.org/10.1109/LICS.2012.65</a>","ista":"Rabinovich A, Rubin S. 2012. Interpretations in trees with countably many branches. LICS: Symposium on Logic in Computer Science, LICS, , 6280474.","mla":"Rabinovich, Alexander, and Sasha Rubin. <i>Interpretations in Trees with Countably Many Branches</i>. 6280474, IEEE, 2012, doi:<a href=\"https://doi.org/10.1109/LICS.2012.65\">10.1109/LICS.2012.65</a>."},"language":[{"iso":"eng"}],"conference":{"end_date":"2012-06-28","name":"LICS: Symposium on Logic in Computer Science","location":"Dubrovnik, Croatia","start_date":"2012-06-25"},"status":"public","alternative_title":["LICS"],"project":[{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307"},{"grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering"}],"date_created":"2018-12-11T11:46:47Z","publist_id":"7324","article_number":"6280474","title":"Interpretations in trees with countably many branches","oa_version":"Preprint","month":"01","type":"conference","date_updated":"2021-01-12T08:01:05Z","day":"01","abstract":[{"text":"We study the expressive power of logical interpretations on the class of scattered trees, namely those with countably many infinite branches. Scattered trees can be thought of as the tree analogue of scattered linear orders. Every scattered tree has an ordinal rank that reflects the structure of its infinite branches. We prove, roughly, that trees and orders of large rank cannot be interpreted in scattered trees of small rank. We consider a quite general notion of interpretation: each element of the interpreted structure is represented by a set of tuples of subsets of the interpreting tree. Our trees are countable, not necessarily finitely branching, and may have finitely many unary predicates as labellings. We also show how to replace injective set-interpretations in (not necessarily scattered) trees by 'finitary' set-interpretations.","lang":"eng"}],"author":[{"full_name":"Rabinovich, Alexander","last_name":"Rabinovich","first_name":"Alexander"},{"full_name":"Rubin, Sasha","id":"2EC51194-F248-11E8-B48F-1D18A9856A87","first_name":"Sasha","last_name":"Rubin"}],"scopus_import":1,"ec_funded":1,"_id":"496","year":"2012","department":[{"_id":"KrCh"}],"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","publisher":"IEEE"}]