State class constructions for branching analysis of time Petri nets

被引：0

作者：

Berthomieu, B ^{[1
]}

Vernadat, F ^{[1
]}

机构：

[1] CNRS, LAAS, F-31077 Toulouse, France

来源：

TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PROCEEDINGS | 2003年 / 2619卷

关键词：

Time Petri nets; state classes; branching time temporal properties; model-checking; bisimulation; real-time systems modeling and verification;

D O I：

暂无

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

This paper is concerned with construction of some state space abstractions for Time Petri nets. State class spaces were introduced long ago by Berthomieu and Menasche as finite representations for the typically infinite state spaces of Time Petri nets, preserving their linear time temporal properties. This paper proposes a similar construction that preserves their branching time temporal properties. The construction improves a previous proposal by Yoneda and Ryuba. The method has been implemented, computing experiments are reported.

引用

页码：442 / 457

页数：16

共 15 条

[1]

Alur R., 1990, Proceedings. Fifth Annual IEEE Symposium on Logic in Computer Science (90CH2897-7), P414, DOI 10.1109/LICS.1990.113766

[2]

ALUR R, 1996, LECT NOTES COMPUT SC, V630, P340

[3] MODELING AND VERIFICATION OF TIME-DEPENDENT SYSTEMS USING TIME PETRI NETS [J].