Title: Symbolic Proof of CTL Formulae over Petri Nets
Abstract: We present a method for proving properties of Petri nets expressed in the branching time temporal logic CTL. The framework of CTL formulae, viewed through the notions of predicates and predicate transformers in the context of Petri nets, is also presented. By overcoming the normal limitation of model checking which restricts its applicability to finite state systems this improvement will allow the use of symbolic model checking. The new concept of predicate structure, a symbolic representation of a set of markings of a Petri net, is defined together with a set of associated operations.
Publication Year: 1993
Publication Date: 1993-01-01
Language: en
Type: article
Access and Citation
Cited By Count: 2
AI Researcher Chatbot
Get quick answers to your questions about the article from our AI researcher chatbot