New Efficient Petri Net Reductions for Parallel Programs Verification
Haddad, Serge; Pradat-Peyre, Jean-François (2006), New Efficient Petri Net Reductions for Parallel Programs Verification, Parallel Processing Letters, 16, 1, p. 101-116. http://dx.doi.org/10.1142/S0129626406002502
Type
Article accepté pour publication ou publiéDate
2006Journal name
Parallel Processing LettersVolume
16Number
1Publisher
World Scientific
Pages
101-116
Publication identifier
Metadata
Show full item recordAbstract (EN)
Structural model abstraction is a powerful technique for reducing the complexity of a state based enumeration analysis. We present in this paper new efficient Petri nets reductions. First, we define "behavioural" reductions (i.e. based on conditions related to the language of the net) which preserve a fundamental property of a net (i.e. liveness) and any formula of the (action-based) linear time logic that does not observe reduced transitions of the net. We show how to replace these conditions by structural or algebraical ones leading to reductions that can be efficiently checked and applied whereas enlarging the application spectrum of the previous reductions. At last, we illustrate our method on a significant and typical example of a synchronisation pattern of parallel programs.Subjects / Keywords
Petri nets; concurrent software verification; structural abstraction; Reduction theoryRelated items
Showing items related by title and author.
-
Evangelista, Sami; Haddad, Serge; Pradat-Peyre, Jean-François (2005) Communication / Conférence
-
Evangelista, Sami; Haddad, Serge; Pradat-Peyre, Jean-François (2004) Communication / Conférence
-
Couvreur, Jean-Michel; Haddad, Serge; Pradat-Peyre, Jean-François (1993) Communication / Conférence
-
Evangelista, Sami; Haddad, Serge; Pradat-Peyre, Jean-François (2004) Article accepté pour publication ou publié
-
Pradat-Peyre, Jean-François; Haddad, Serge; Couvreur, Jean-Michel (1992) Article accepté pour publication ou publié