Title :
A temporal specifications checker for Petri nets
Author_Institution :
Swiss Federal Inst. of Technol., Lausanne, Switzerland
Abstract :
Presents a model-checking method for systems modelled with Petri nets. The authors´ approach is based on a definition of a symbolic representation of sets of markings, with the intended properties of the net expressed by using a specific temporal logic. On one hand, the symbolic representation may structure the state space of the net, thus allowing the consideration of larger systems while, on the other hand, the temporal properties are expressed in a very intuitive temporal language
Keywords :
Petri nets; temporal logic; Petri nets; model-checking method; state space; symbolic representation; temporal language; temporal logic; temporal properties; temporal specifications checker; Iterative algorithms; Logic; Petri nets; State-space methods;
Conference_Titel :
Systems, Man and Cybernetics, 1995. Intelligent Systems for the 21st Century., IEEE International Conference on
Conference_Location :
Vancouver, BC
Print_ISBN :
0-7803-2559-1
DOI :
10.1109/ICSMC.1995.538324
