%0 Journal Article %T Preservation of Liveness and Deadlock-Freeness in Synchronous Synthesis of Petri Net Systems
同步合成Petri网系统活性与无死锁性的保持性 %A PU Fei %A LU Wei-Ming %A
蒲飞 %A 陆维明 %J 软件学报 %D 2003 %I %X Synthesis process is an important bottom-up approach on modeling Petri net systems, and the preservation of certain good properties such as liveness, deadlock-freeness, reversibility and so forth is also a significant problem in the study of synthesis processes. In this paper, the preservation of liveness and deadlock-freeness is discussed for a synchronous synthesis process. The difference from other work is that the presented approaches are based on the concurrent composition of paths using a concurrent language. The concurrent language relation formula is presented and proved in the synchronous synthesis of Petri net systems, and it can be applied to judge the liveness and deadlock-freeness of a synthesized system. Meanwhile, criteria which are necessary and sufficient for the liveness and deadlock-freeness of the resultant system are developed. Finally, conditions under which the preservation of liveness and deadlock-freeness holds for the synchronous synthesis of Petri net systems are proposed. %K synchronous synthesis process %K preservation of liveness and deadlock-freeness %K concurrent language %K synchronous path %K concurrent composition of paths
同步合成操作 %K 活性与无死锁性的保持性 %K 并发语言 %K 同步路径 %K 路径并发合成 %U http://www.alljournals.cn/get_abstract_url.aspx?pcid=5B3AB970F71A803DEACDC0559115BFCF0A068CD97DD29835&cid=8240383F08CE46C8B05036380D75B607&jid=7735F413D429542E610B3D6AC0D5EC59&aid=A8912CF7578FABFA&yid=D43C4A19B2EE3C0A&vid=F3583C8E78166B9E&iid=59906B3B2830C2C5&sid=D3A55680A8B4A1DC&eid=0702FE8EC3581E51&journal_id=1000-9825&journal_name=软件学报&referenced_num=10&reference_num=19