World Scientific
  • Search
Skip main navigation

Cookies Notification

We use cookies on this site to enhance your user experience. By continuing to browse the site, you consent to the use of our cookies. Learn More
×
Our website is made possible by displaying certain online content using javascript.
In order to view the full content, please disable your ad blocker or whitelist our website www.worldscientific.com.

System Upgrade on Tue, Oct 25th, 2022 at 2am (EDT)

Existing users will be able to log into the site and access content. However, E-commerce and registration of new users may not be available for up to 12 hours.
For online purchase, please visit us again. Contact us at [email protected] for any enquiries.

New Efficient Petri Nets Reductions for Parallel Programs Verification

    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
    • G.   Berthelot , 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
    • Edmund M. Clarke, Orna Grumberg and David E. Long, ACM Transactions on Programming Languages and Systems 16(5), 1512 (1994), DOI: 10.1145/186025.186051. Crossref, ISIGoogle Scholar
    • Ernie Cohen and Leslie Lamport, Reduction in TLA, International Conference on Concurrency Theory (1998) pp. 317–331. Google Scholar
    • G.   Berthelot , 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 et al. , Reliable Software Technologies - Ada-Europe 2003 , LNCS   2655 ( Springer-Verlag , 2003 ) . Google Scholar
    • J. Esparza and C. Schröter, Correct Hardwure Design and Verification Methods, LNCS 2144, eds. T. Margaria and T. Melham (Springer-Verlag, 2001) pp. 310–324. CrossrefGoogle Scholar
    • Cormac   Flanagan and Shaz   Qadeer , 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
    • A. N. Habermann, ACM 12(7), 373-ff (1969), DOI: 10.1145/363156.363160. Crossref, ISIGoogle 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
    • Richard J. Lipton, Commun. ACM 18(12), 717 (1975), DOI: 10.1145/361227.361234. Crossref, ISIGoogle Scholar
    • Leslie Lamport and Fred B. Schneider. Pretending atomicity. Technical Report TR89-1005, 1989 . Google Scholar
    • D. Poitrenaud and J. F. Pradat-Peyre, High-level Petri Nets, Theory and Application, LNCS 1825, eds. M. Nielsen and D. Simpson (Springer-Verlag, 2000) pp. 387–408. Google Scholar