Topological Characterisation of Multi-Buffer Simulation

• Autorzy: Hutagalung Milka

Identyfikatory

DOI

10.3233/FI-2021-1999

• Języki publikacji: EN

Abstrakty

EN

Multi-buffer simulation is an extension of simulation preorder that can be used to approximate inclusion of languages recognised by Büchi automata up to their trace closures. DUPLICATOR can use some bounded or unbounded buffers to simulate SPOILER ’s move. It has been shown that multi-buffer simulation can be characterised with the existence of a continuous function. In this paper, we show that such a characterisation can be refined to a more restricted case, that is, to the one where DUPLICATOR only uses bounded buffers, by requiring the function to be Lipschitz continuous instead of only continuous. This characterisation however only holds for some restricted classes of automata. One of the automata should only produce words where each letter cannot commute unboundedly. We show that this property can be syntactically characterised with cyclic-path-connectedness, a refinement of syntactic condition on automata that have regular trace closure. We further show that checking cyclic-path-connectedness is indeed co-NP-complete.

Słowa kluczowe

EN

continuous functions; robots

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2021
• Tom: Vol. 178, nr 1/2
• Strony: 77--99
• Opis fizyczny: Bibliogr. 20 poz., rys.

Twórcy

autor

Hutagalung Milka

• University of Kassel, Germany

Bibliografia

• [1] Abdulla PA, Bouajjani A, Holík L, Kaati L, Vojnar T. Computing Simulations over Tree Automata. In: TACAS’08, LNCS. Springer, 2008 pp. 93-108. doi:10.1007/978-3-540-78800-3_8.
• [2] Fritz C, Wilke T. Simulation relations for alternating Büchi automata. Theoretical Computer Science, 2005. 338(1):275-314. doi:https://doi.org/10.1016/j.tcs.2005.01.016.
• [3] Etessami K, Wilke T, Schuller RA. Fair Simulation Relations, Parity Games, and State Space Reduction for Büchi Automata. In: ICALP’01. 2001 pp. 694-707. doi:10.1137/S0097539703420675.
• [4] Dill D, Hu A, Wong-Toi H. Checking for Language Inclusion Using Simulation Preorders. In: CAV ’91. 1992 pp. 255-265. doi:10.1007/3-540-55179-4_25.
• [5] Etessami K. A Hierarchy of Polynomial-Time Computable Simulations for Automata. In: CONCUR 2002. Springer Berlin Heidelberg, Berlin, Heidelberg, 2002 pp. 131-144. doi:10.1007/3-540-45694-5_10.
• [6] Hutagalung M, Hundeshagen N, Kuske D, Lange M, Lozes É. Multi-Buffer Simulations for Trace Language Inclusion. In: GandALF’16. 2016 pp. 213-227. doi:10.4204/EPTCS.226.15.
• [7] Hutagalung M, Hundeshagen N, Kuske D, Lange M, Lozes É. Two-Buffer Simulation Games. In: Cassting/SynCoP 2016. 2016 pp. 27-38. doi:10.4204/EPTCS.220.3.
• [8] Henzinger TA, Kupferman O, Rajamani SK. Fair Simulation. Inf. Comput., 2002. 173(1):64-81.
• [9] Diekert V. Combinatorics on Traces. Springer-Verlag, Berlin, Heidelberg, 1990. ISBN:0-387-53031-2.
• [10] Rozenberg G, Salomaa A (eds.). Handbook of Formal Languages, Vol. 3: Beyond Words. Springer-Verlag New York, Inc., New York, NY, USA, 1997. ISBN:3-540-60649-1.
• [11] Diekert V, Rozenberg G. The Book of Traces. World Scientific Publishing Co., Inc., River Edge, NJ, USA, 1995. ISBN:9810220588.
• [12] Sakarovitch J. The ”last” decision problem for rational trace languages. In: LATIN’92, LNCS. Springer, 1992 pp. 460-473.
• [13] Finkel O. Three Applications to Rational Relations of the High Undecidability of the Infinite Post Correspondence Problem in a Regular ω-Language. Int. J. Found. Comput. Sci, 2012. 23(7):1481-1498. URL https://doi.org/10.1142/S0129054112400606.
• [14] Clemente L, Mayr R. Advanced automata minimization. In: POPL’13. ACM, 2013 pp. 63-74.
• [15] Hutagalung M, Lange M, Étienne Lozes. Revealing vs. Concealing: More Simulation Games for Büchi Inclusion. In: LATA’13, volume 7810 of LNCS. Springer, 2013 pp. 347-358. doi:10.1007/978-3-642-37064-9_31.
• [16] Holtmann M, Kaiser L, Thomas W. Degrees of Lookahead in Regular Infinite Games. Logical Methods in Computer Science, 2012. 8(3). URL https://doi.org/10.2168/LMCS-8(3:24)2012.
• [17] Clerbout M, Latteux M. Semi-commutations. Information and Computation, 1987. 73(1):59-74. URL https://doi.org/10.1016/0890-5401(87)90040-X.
• [18] Ochmanski E. Regular behaviour of concurrent systems. Bulletin of the EATCS, 1985. 27:56-67. ID:12684522.
• [19] Thomas W. Handbook of Theoretical Computer Science (Vol. B). chapter Automata on Infinite Objects, pp. 133-191. MIT Press, Cambridge, MA, USA. ISBN:0-444-88074-7, 1990.
• [20] Muscholl A, Peled D. Message Sequence Graphs and Decision Problems on Mazurkiewicz Traces, pp. 81-91. Springer Berlin Heidelberg, Berlin, Heidelberg, 1999. doi:10.1007/3-540-48340-3_8.

Uwagi

Opracowanie rekordu ze środków MNiSW, umowa Nr 461252 w ramach programu "Społeczna odpowiedzialność nauki" - moduł: Popularyzacja nauki i promocja sportu (2021).