Topological Characterisation of Multi-Buffer Simulation

Issue title: Special Issue on the 11th International Workshop on Reachability Problems (RP 2017)

Guest editors: Matthew Hague and Igor Potapov

Article type: Research Article

Authors: Hutagalung, Milka^{; *}

Affiliations: University of Kassel, Germany. [email protected]

Correspondence: [*] Address for correspondence: University of Kassel, D-34121 Kassel, Germany

Abstract: 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.

DOI: 10.3233/FI-2021-1999

Journal: Fundamenta Informaticae, vol. 178, no. 1-2, pp. 77-99, 2021