等价于Büchi寄存器自动机的带冻结量词的Mu-演算子类

Yoshiaki Takata; Akira Onishi; Ryoma Senda; Hiroyuki Seki

等价于Büchi寄存器自动机的带冻结量词的Mu-演算子类

形式语言与自动机理论 2024-06-18 v1 计算机科学中的逻辑

作者: Yoshiaki Takata , Akira Onishi , Ryoma Senda , Hiroyuki Seki

摘要

寄存器自动机（RA）是有限自动机的一种扩展，用于处理无限域中的数据值。在先前的工作中，我们提出了析取mu $^\downarrow$ -演算，它是带冻结量词的模态mu-演算的一个子类，并证明了它具有与RA相同的表达能力。然而，析取mu $^\downarrow$ -演算被定义为有限字上的逻辑，而模型检测中的时序规范通常以无限字的形式给出。在本文中，我们重新定义了析取mu $^\downarrow$ -演算的语法和语义，使其适用于无限字，并证明所得到的时序逻辑具有与Büchi RA相同的表达能力。

关键词

Mu-演算冻结量词寄存器自动机 Büchi自动机时序逻辑表达能力无限字

引用

@article{arxiv.2406.11351,
  title  = {A Subclass of Mu-Calculus with the Freeze Quantifier Equivalent to Buchi Register Automata},
  author = {Yoshiaki Takata and Akira Onishi and Ryoma Senda and Hiroyuki Seki},
  journal= {arXiv preprint arXiv:2406.11351},
  year   = {2024}
}

备注

6 pages, 1 figure, this is a longer version of a short paper submitted to IEICE Transactions on Information and Systems

等价于Büchi寄存器自动机的带冻结量词的Mu-演算子类

摘要

关键词

引用

备注

相关论文