Verifying time Petri nets by linear programming

被引：0

作者：

Xuandong Li

机构：

[1] Nanjing University,State Key Laboratory of Novel Software Technology Department of Computer Science and Technology

来源：

Journal of Computer Science and Technology | 2001年 / 16卷

关键词：

real-time system; time Petri net; linear programming; model-checking;

D O I：

暂无

中图分类号：

学科分类号：

摘要：

The paper proposes an approach to solving some verification problems of time Petri nets using linear programming. The approach is based on the observation that forloop-closed time Petri nets, it is only necessary to investigate a finite prefix of an untimed run of the underlying Petri net. Using the technique the paper gives solutions to reachability and bounded delay timing analysis problems. For both problems algorithms are given, that are decision procedures for loop-closed time Petri nets, and semi-decision procedures for general time Petri nets.

引用

页码：39 / 46

页数：7

共 10 条

[1]

Merlin P M(1976)Recoverability of communication protocols — Implications of a theoretical study IEEE Transactions on Communications 24 1036-1043

[2]

Farber D J(1991)Modelling and verification of time dependent systems using time Petri nets IEEE Transactions on Software Engineering 17 259-273

[3]

Berthomieu B(1997)Efficient verifications of parallel real-time systems In Formal Methods in System Design, Kluwer Academic Publishers 11 187-215

[4]

Diaz M(1992)Minimum and maximum delay problems in real-time systems In Formal Methods in System Design 1 385-415

[5]

Yoneda Tomohiro(1997)Bounded day timing analysis of a class of CSP programs In Formal Methods in System Design 11 275-305

[6]

Schlingloff Bernd-Holger(undefined)undefined undefined undefined undefined-undefined

[7]

Courcoubetis C(undefined)undefined undefined undefined undefined-undefined

[8]

Yannakakis M(undefined)undefined undefined undefined undefined-undefined

[9]

Hulgaard H(undefined)undefined undefined undefined undefined-undefined

[10]

Burns S M(undefined)undefined undefined undefined undefined-undefined

← 1 →