单时钟ATA的Büchi-Kamp定理
Büchi-Kamp Theorems for 1-clock ATA
摘要：
本文研究了1-时钟交替时间自动机（1-ATA）及其自然子类的Kamp-like和Büchi-like定理。定义了具有无环复位的1-ATA的概念。这个自动机类被证明是表达等价于时间逻辑$\regmtl$，这是$\mathsf{MTL[F_I]}$扩展与正则表达式守护模态。此外，还引入了具有k-变连通性的未来时控MSO的子类逻辑$\qkmso$ .在类似坎普的结果中，它表明，$\regmtl$是表达等价于$\qkmso$。作为我们的第二个结果，我们定义了合取-析取1-时钟ATA（$\wf$ 1-ATA）的概念。我们表明，$\wf$ 1-ATA与无环复位表示等价的子逻辑$\F\regmtl$的$\regmtl$。此外，$\F\regmtl$在表达上等同于$\qtwomso$，即$\qkmso$的两个可变连接片段。1-ATA的全类被证明是表现等价于$\regmtl$扩展与不动点算子。
英文摘要：
This paper investigates Kamp-like and Büchi-like theorems for 1-clock Alternating Timed Automata (1-ATA) and its natural subclasses. A notion of 1-ATA with loop-free-resets is defined. This automaton class is shown to be expressively equivalent to the temporal logic $\regmtl$ which is $\mathsf{MTL[F_I]}$ extended with a regular expression guarded modality. Moreover, a subclass of future timed MSO with k-variable-connectivity property is introduced as logic $\qkmso$. In a Kamp-like result, it is shown that $\regmtl$ is expressively equivalent to $\qkmso$. As our second result, we define a notion of conjunctive-disjunctive 1-clock ATA ($\wf$ 1-ATA). We show that $\wf$ 1-ATA with loop-free-resets are expressively equivalent to the sublogic $\F\regmtl$ of $\regmtl$. Moreover $\F\regmtl$ is expressively equivalent to $\qtwomso$, the two-variable connected fragment of $\qkmso$. The full class of 1-ATA is shown to be expressively equivalent to $\regmtl$ extended with fixed point operators.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
