Logics for Weighted Timed Pushdown Automata
Logics for Weighted Timed Pushdown Automata
复制标题
加权定时下推自动机的逻辑
DOI：
10.1007/978-3-319-23534-9_9
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
V. Perevoshchikov
中科院分区：
文献类型：
--
作者：
M. Droste;V. Perevoshchikov
Abdulla，Atig和Stenman提出了一种带时间栈的加权密集时间下推自动机模型来描述实时递归系统的行为。受加权时间下推自动机和Droste和Gastin的加权逻辑的最优可达性问题的可判定性的启发，我们引入了一个在时间词上的加权MSO逻辑，它在表达上等价于加权时间下推自动机.为了证明表达式等价的结果，我们证明了一个分解定理，该定理建立了加权定时下推语言和显式下推语言之间的联系，然后我们应用他们关于显式下推语言的逻辑特征的结果。
Weighted dense-timed pushdown automata with a timed stack were introduced by Abdulla, Atig and Stenman to model the behavior of real-time recursive systems. Motivated by the decidability of the optimal reachability problem for weighted timed pushdown automata and weighted logic of Droste and Gastin, we introduce a weighted MSO logic on timed words which is expressively equivalent to weighted timed pushdown automata. To show the expressive equivalence result, we prove a decomposition theorem which establishes a connection between weighted timed pushdown languages and visibly pushdown languages of Alur and Mudhusudan; then we apply their result about the logical characterization of visibly pushdown languages.
登录
查看更多内容
在强大的可判定逻辑和定时自动机中指定定时状态序列
DOI：
--
发表时间：
1994
期刊：
Formal Techniques in Real-Time and Fault-Tolerant Systems
影响因子：
--
作者：
T. Wilke
通讯作者：
T. Wilke
用于加权时间自动机的 MSO 逻辑
影响因子：
0.8
作者：
Karin Quaas
通讯作者：
Karin Quaas
DOI：
10.2168/lmcs-6(3:23)2010
发表时间：
2010-07
期刊：
Log. Methods Comput. Sci.
影响因子：
--
作者：
Alexandra Silva;M. Bonsangue;J. Rutten
通讯作者：
Alexandra Silva;M. Bonsangue;J. Rutten
嵌套词和代数形式幂级数的加权逻辑
DOI：
10.2168/lmcs-6(1:5)2010
发表时间：
2008
期刊：
Theor. Comput. Sci.
影响因子：
--
作者：
Christian Mathissen
通讯作者：
Christian Mathissen
能量约束下观察者的定时自动机
影响因子：
4.9
作者：
P. Bouyer;U. Fahrenberg;K. Larsen;N. Markey
通讯作者：
N. Markey