Dynamic Communicating Automata and Branching High-Level MSCs
Dynamic Communicating Automata and Branching High-Level MSCs
复制标题
动态通信自动机和分支高级 MSC
DOI：
--
复制
发表时间：
2013
期刊：
影响因子：
--
通讯作者：
T. Schwentick
中科院分区：
文献类型：
--
作者：
B. Bollig;Aiswarya Cyriac;L. Hélouët;A. Kara;T. Schwentick
我们研究动态通信自动机（DCA），这是经典通信有限状态机的扩展，允许动态创建过程。DCA的行为可以描述为一组消息序列图（MSCs）。当DCA作为实现的模型时，我们建议在规范端分支高级msc （bhmsc）。我们的重点是可实现性问题：给定bHMSC，是否可以构建等效的DCA？由于这个问题是不确定的，我们引入了可执行性的概念，这是可实现性的一个可确定的必要标准。我们证明bHMSCs的可执行性是EXPTIME-complete的。然后，我们确定一类bhmsc，其可执行性实际上意味着可实现性。
We study dynamic communicating automata (DCA), an extension of classical communicating finite-state machines that allows for dynamic creation of processes. The behavior of a DCA can be described as a set of message sequence charts (MSCs). While DCA serve as a model of an implementation, we propose branching high-level MSCs (bHMSCs) on the specification side. Our focus is on the implementability problem: given a bHMSC, can one construct an equivalent DCA? As this problem is undecidable, we introduce the notion of executability, a decidable necessary criterion for implementability. We show that executability of bHMSCs is EXPTIME-complete. We then identify a class of bHMSCs for which executability effectively implies implementability.