Binary Reachability of Timed-register Pushdown Automata and Branching Vector Addition Systems
Binary Reachability of Timed-register Pushdown Automata and Branching Vector Addition Systems
复制标题
定时寄存器下推自动机和分支向量加法系统的二进制可达性
DOI：
10.1145/3326161
复制
发表时间：
2019
影响因子：
0.5
通讯作者：
Clemente L
中科院分区：
文献类型：
--
作者：
Clemente L
定时寄存器下推自动机构成了一个非常有表现力的自动机类，其转换可能涉及状态、输入和具有无限差异的堆栈顶部定时寄存器。它们严格归入了Bouajjani等人的下推时间自动机、Abdulla等人的稠密时间下推自动机以及Clemente和Lasota的轨道有限时间寄存器下推自动机。给出了时间寄存器下推自动机可达性关系的有效逻辑表征。作为推论，我们得到了非空问题的双指数时间过程。我们证明了在时间单调的假设下，复杂度降为单指数。该证明涉及到一个具有状态的一维整数分支向量加法系统的新模型。作为一个有趣的结果，我们证明了后一种模型的可达集是半线性的，在指数时间内可计算。
Timed-register pushdown automata constitute a very expressive class of automata, whose transitions may involve state, input, and top-of-stack timed registers with unbounded differences. They strictly subsume pushdown timed automata of Bouajjani et al., dense-timed pushdown automata of Abdulla et al., and orbit-finite timed-register pushdown automata of Clemente and Lasota. We give an effective logical characterisation of the reachability relation of timed-register pushdown automata. As a corollary, we obtain a doubly exponential time procedure for the non-emptiness problem. We show that the complexity reduces to singly exponential under the assumption of monotonic time. The proofs involve a novel model of one-dimensional integer branching vector addition systems with states. As a result interesting on its own, we show that reachability sets of the latter model are semilinear and computable in exponential time.
登录
查看更多内容
分支向量加法系统的可达性问题需要双指数空间
DOI：
10.1016/j.ipl.2010.06.008
发表时间：
2010
期刊：
Inf. Process. Lett.
影响因子：
--
作者：
R. Lazic
通讯作者：
R. Lazic
使用线性混合观测器验证上下文无关定时系统
DOI：
10.1007/3-540-58179-0_48
发表时间：
1994
期刊：
2012 27th Annual IEEE Symposium on Logic in Computer Science
影响因子：
--
作者：
A. Bouajjani;R. Echahed;R. Robbana
通讯作者：
R. Robbana
DOI：
--
发表时间：
2016
期刊：
--
影响因子：
--
作者：
Goeller S
通讯作者：
Goeller S
一阶可定义下推系统的可达性分析
DOI：
10.4230/lipics.csl.2015.244
发表时间：
2015
期刊：
2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science
影响因子：
--
作者：
Lorenzo Clemente;S. Lasota
通讯作者：
S. Lasota
DOI：
10.1016/j.ic.2014.12.004
发表时间：
2013-02
期刊：
--
影响因子：
--
作者：
John Fearnley;M. Jurdzinski
通讯作者：
John Fearnley;M. Jurdzinski