摘要
应用时态逻辑提出计时Ｐｅｔｒｉ网的形式化分析方法，基于可达标识列研究受控系统的时态特征及其可控性与控制不变性，给出控制逻辑存在的充要条件，提出了时态公式分解方法，并讨论了禁止状态避免问题。
A formal analysis of timed Petri net is proposed by using temporal logic. Based on markings sequences, temporal properties and controllability of controlled Petri net are studied. The necessary and sufficient condition for the existence of control logic is obtained, and the modular method of temporal feature is induced. Finally a control synthesis procedure is given for timed Petri net based on a temporal formula known as the forbidden state specification.
出处
《控制与决策》
EI
CSCD
北大核心
1999年第2期103-108,114,共7页
Control and Decision
基金
山东省自然科学基金
关键词
计时Petri网
可达标识列
时态特征
离散事件系统
timed Petri net, markings sequences, temporal feature, controllability, control invariance
