%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