文章基本信息

标题：Determinisability of One-Clock Timed Automata
本地全文：下载
作者：Lorenzo Clemente ; S{\l}awomir Lasota ; Rados{\l}aw Pi{\'o}rkowski 等
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2020
卷号：171
页码：42:1-42:17
DOI：10.4230/LIPIcs.CONCUR.2020.42
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：The deterministic membership problem for timed automata asks whether the timed language recognised by a nondeterministic timed automaton can be recognised by a deterministic timed automaton. We show that the problem is decidable when the input automaton is a one-clock nondeterministic timed automaton without epsilon transitions and the number of clocks of the deterministic timed automaton is fixed. We show that the problem in all the other cases is undecidable, i.e., when either 1) the input nondeterministic timed automaton has two clocks or more, or 2) it uses epsilon transitions, or 3) the number of clocks of the output deterministic automaton is not fixed.
关键词：Timed automata; determinisation; deterministic membership problem