New Efficient Petri Nets Reductions for Parallel Programs Verification
Abstract
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.
References
- G. Berthelot. Transformation et analyse de réseaux de Petri, applications aux protocoles. Thèse d'état, Universit é Pierre et Marie Curio. Paris. 1983 . Google Scholar
- , Checking properties of nets using transformations ,
LNCS 222 , ed.G. Rozenberg ( Springer-Verlag , 1985 ) . Google Scholar G. Berthelot , Advances in Petri Nets,LNCS 254 (Springer-Verlag, 1986) pp. 359–376. Google Scholar- ACM Transactions on Programming Languages and Systems 16(5), 1512 (1994), DOI: 10.1145/186025.186051. Crossref, ISI, Google Scholar
Ernie Cohen and Leslie Lamport , Reduction in TLA, International Conference on Concurrency Theory (1998) pp. 317–331. Google Scholar- , Advances in Petri Nets 1990 ,
LNCS 483 , eds.J. M. Colom and M. Silva ( 1991 ) . Google Scholar Thomas W. Doeppner Jr. , Parallel program correctness through refinement, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages (ACM Press, 1977) pp. 155–169. Google Scholar-
S. Evangelista , Reliable Software Technologies - Ada-Europe 2003 ,LNCS 2655 ( Springer-Verlag , 2003 ) . Google Scholar - , Correct Hardwure Design and Verification Methods,
LNCS 2144, eds.T. Margaria and T. Melham (Springer-Verlag, 2001) pp. 310–324. Crossref, Google Scholar - , Electronic Notes in Theoretical Computer Science 89 , eds.
Byron Cook , Scott Stoller and Willem Visser ( Elsevier , 2003 ) . Google Scholar Cormac Flanagan and Shaz Qadeer , A type and effect, system for atomicity, Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation (ACM Press, 2003) pp. 338–349. Google Scholar- Stephen N. Freund and Shaz Qadeer. Checking concise specifications for multithreaded software. In Formal Techniques for Java-like Programs, 2003 . Google Scholar
E. Pascal Gribomon , Atomicity refinement and trace reduction theorems, CAV1102, eds.Rajeev Alur and Thomas A. Henzinger (Springer Verlag, New Brunswick, NJ, USA, 1996) pp. 311–322. Google Scholar- ACM 12(7), 373-ff (1969), DOI: 10.1145/363156.363160. Crossref, ISI, Google Scholar
- S. Haddad and J. F. Pradat-Peyre. Efficient reductions for LTL formulae vcrification. Technical Report 634, CEDRIC, CNAM, Paris, http://cedric.cnam.fr, 2004 . Google Scholar
- Commun. ACM 18(12), 717 (1975), DOI: 10.1145/361227.361234. Crossref, ISI, Google Scholar
- Leslie Lamport and Fred B. Schneider. Pretending atomicity. Technical Report TR89-1005, 1989 . Google Scholar
- , High-level Petri Nets, Theory and Application,
LNCS 1825, eds.M. Nielsen and D. Simpson (Springer-Verlag, 2000) pp. 387–408. Google Scholar


