Reactive Synthesis from Visibly Register Pushdown Automata
Reactive Synthesis from Visibly Register Pushdown Automata
复制标题
DOI：
10.1007/978-3-030-85315-0_19
复制
发表时间：
2021
期刊：
影响因子：
--
通讯作者：
Ryoma Senda;Y. Takata;H. Seki
中科院分区：
文献类型：
--
作者：
Ryoma Senda;Y. Takata;H. Seki
可实现性问题是确定一个给定规范是否存在一个满足的实现.虽然这个问题在递归程序的反应合成领域很重要，但当规范和实现由下推计算模型给出时，这个问题还没有被研究过。本文研究了由下推自动机（PDA）和下推转换器（PDT）以及寄存器下推自动机（RPDA）和寄存器下推转换器（RPDT）给出规范和实现的情况下的可实现性问题。
The realizability problem for a given specificationis to decide whether there exists an implementation satisfying. Although the problem is important in the field of reactive synthesis of recursive programs, the problem has not been studied yet when specification and implementation are given by pushdown computational models. This paper investigates the realizability problem for the cases that a specification and an implementation are given by a pushdown automaton (PDA) and a pushdown transducer (PDT), and a register pushdown automata (RPDA) and a register pushdown transducer (RPDT).