Wuhan University Journal of Natural Sciences

, Volume 7, Issue 4, pp 415–420 | Cite as

A heuristic method for temporal analysis based on petri net

  • Fu Jian-ming
  • Zhu Fu-xi
  • Xiong Hui


Reachability-based analysis and temporal analysis are used to verify the properties of concurrent systems, and it is important to exploit fast and efficient methods. This paper gives semantics of temporal formulae with edges of the transition system of Petri net, and then presents a fast temporal analyzing method, which takes advantage of both Petri net and temporal logic. The method only expands a path of equivalence trace while the path does not satisfy a property according to trace semantics of Petri net, and can validate directly the property on Petri net. Moreover, we exploit a minimal degree of in-out of a node as heuristics to select a path of an equivalence trace. Finally, we demonstrate the validity of the method that decreases state spaces and improves the verification system with the experimental results.

Key words

Petri net transition system temporal logic trace language 

CLC number

TP 311 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    Tayer R. A General Purpose Algorithm for Analyzing Concurrent Programs.Commun CAM, 1983,26 (5):362–376.Google Scholar
  2. [2]
    Karam G M, Bular R J. Starvation and Critical Race Analyzers for Ada.IEEE Trans Software Engineering, 1990,16(8):829–843.CrossRefGoogle Scholar
  3. [3]
    Reif J H, Smolka S A. The Complexity of Reachability in Distributed Communicating Processes.Acta Information, 1988,25(3):333–354.MATHCrossRefMathSciNetGoogle Scholar
  4. [4]
    Stark P H. Reachability Analysis ofPetri net Using Symmetries.System Analysis Modeling and Simulation, 1991,8:293–303.Google Scholar
  5. [5]
    Antti Valmari. Stubborn Sets for Reduced State Space Generation. In: Grzegorz Rozenberg, editor.Advances in Petri Nets. New York: Springer-Verlag (LNCS 483), 1990, 491–515.Google Scholar
  6. [6]
    Patrice Godefroid, Pierre Wolper. Using Partial Orders for the Efficient Verification of Deadlock Freedom and Safety Properties. In: Kim G, Larse, Arne Skou, editors,Proc CAV’91, Computer-Aided Verification, Springer-Verlag (LNCS 575), 1991, 332–343.Google Scholar
  7. [7]
    McMill K L.Symbolic Model Checking, Boston: MA. Kluwer Academic Publisher, 1994.Google Scholar
  8. [8]
    Burch J R. Symbolic Model Checking with Partitioned Transition Relations.Proceeding of International Conference of VLSI. Scotland, Edinburgh, 1991, 49–52.Google Scholar
  9. [9]
    Fu Jian-ming, Zhu Fu-xi, Peng Rong. A Temporal Analyzed Method Based-Petri Net.Small & Micro Computer System, 2000,21(4): 368–371 (Ch).Google Scholar

Copyright information

© Springer 2002

Authors and Affiliations

  • Fu Jian-ming
    • 1
  • Zhu Fu-xi
    • 1
  • Xiong Hui
    • 1
  1. 1.School of Computer ScienceWuhan UniversityWuhan, HubeiChina

Personalised recommendations