A heuristic method for temporal analysis based on petri net
- 18 Downloads
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 wordsPetri net transition system temporal logic trace language
CLC numberTP 311
Unable to display preview. Download preview PDF.
- Tayer R. A General Purpose Algorithm for Analyzing Concurrent Programs.Commun CAM, 1983,26 (5):362–376.Google Scholar
- Stark P H. Reachability Analysis ofPetri net Using Symmetries.System Analysis Modeling and Simulation, 1991,8:293–303.Google Scholar
- 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
- 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
- McMill K L.Symbolic Model Checking, Boston: MA. Kluwer Academic Publisher, 1994.Google Scholar
- Burch J R. Symbolic Model Checking with Partitioned Transition Relations.Proceeding of International Conference of VLSI. Scotland, Edinburgh, 1991, 49–52.Google Scholar
- 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