Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
References
Tayer R. A General Purpose Algorithm for Analyzing Concurrent Programs.Commun CAM, 1983,26 (5):362–376.
Karam G M, Bular R J. Starvation and Critical Race Analyzers for Ada.IEEE Trans Software Engineering, 1990,16(8):829–843.
Reif J H, Smolka S A. The Complexity of Reachability in Distributed Communicating Processes.Acta Information, 1988,25(3):333–354.
Stark P H. Reachability Analysis ofPetri net Using Symmetries.System Analysis Modeling and Simulation, 1991,8:293–303.
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.
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.
McMill K L.Symbolic Model Checking, Boston: MA. Kluwer Academic Publisher, 1994.
Burch J R. Symbolic Model Checking with Partitioned Transition Relations.Proceeding of International Conference of VLSI. Scotland, Edinburgh, 1991, 49–52.
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).
Author information
Authors and Affiliations
Additional information
Foundation item: Supported by the National Natural Science, Foundation of China (90104005, 66973034)
Biography: Fu Jian-ming (1969-) male, Ph.D, research interest: high-speed information network and system safety.
Rights and permissions
About this article
Cite this article
Jian-ming, F., Fu-xi, Z. & Hui, X. A heuristic method for temporal analysis based on petri net. Wuhan Univ. J. Nat. Sci. 7, 415–420 (2002). https://doi.org/10.1007/BF02828240
Received:
Issue Date:
DOI: https://doi.org/10.1007/BF02828240