摘要
给出 Petri网弱活性 (无死锁 )与活性的两个语言刻画 ,讨论了同步合成 Petri网的语言性质 .基于 Petri网语言 ,给出了判定 Petri网活性的充分必要条件 .同时研究了 Petri网同步合成过程中活性保持问题 ,给出保持活性的充分必要条件 .
Two language characterizations for weak liveness (free-deadlock) and liveness of Petri nets are given. Some language properties of synchronous composed Petri nets are discussed. Based on Petri net language, a necessary and sufficient condition is given for live Petri net (bounded), and then the liveness preservation in a synchronous composed net is studied and a necessary and sufficient condition is obtained. Those results give a formal language method for net liveness testing and controlling.
出处
《软件学报》
EI
CSCD
北大核心
2001年第4期512-520,共9页
Journal of Software
基金
国家自然科学基金
国家重点基础研究基金
全国优秀博士学位论文作者基金
上海市重点基础研究基金
上海市曙光计划基金
关键词
PETRI网
并发系统
活性
同步合成
形式语言
Characterization
Composition
Control systems
Formal languages
Petri nets
Synchronization
Testing
Theorem proving
