Efficient timing analysis of a class of Petri nets

  • Henrik Hulgaard
  • Steven M. Burns
Session 12: Invited Talk
Part of the Lecture Notes in Computer Science book series (LNCS, volume 939)


We describe an algebraic technique for performing timing analysis on a restricted class of Petri nets with interval time delays specified on the places of the net. The timing analysis we perform determines the extreme separation in time between specified occurrences of pairs of transitions for all possible timed executions of the system. We present the details of the timing analysis algorithm and demonstrate polynomial running time on a non-trivial parameterized example. Petri nets with 3000 nodes and 1016 reachable states have been analyzed using these techniques.


Timing Assignment Simple Path Concurrent System Simple Cycle Maximum Separation 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 1.
    R. Alur and D. L. Dill. The theory of timed automata. In J. W. de Bakker, C. Huizing, W. P. de Roever, and G. Rosenberg, editors, Real-Time: Theory in Practice, LNCS #600, pages 28–73. Springer-Verlag, 1991.Google Scholar
  2. 2.
    F. Baccelli, G. Cohen, G. J. Olsder, and J.-P. Quadrat. Synchronization and Linearity. John Wiley and Sons, 1992.Google Scholar
  3. 3.
    B. Berthomieu and M. Diaz. Modeling and verification of time dependent systems using time Petri nets. IEEE Transactions on Software Engineering, 17(3):259–273, 1991.Google Scholar
  4. 4.
    E. Best and J. Desel. Partial order behavior and structure of Petri nets. Formal Aspects of Computing, 2:123–138, 1990.CrossRefGoogle Scholar
  5. 5.
    E. Best and Raymond Devillers. Interleaving and partial orders in concurrency: A formal comparison. In M. Wirsing, editor, Formal Description of Programming Concepts-III, pages 299–323, 1986.Google Scholar
  6. 6.
    J. R. Burch. Trace Algebra for Automatic Verification of Real-Time Concurrent Systems. Ph.D. thesis, Carnegie Mellon, August 1992.Google Scholar
  7. 7.
    C. Courcoubetis and M. Yannakakis. Minimum and maximum delay problems in real-time systems. Formal Methods in System Design, 1:385–415, 1992.Google Scholar
  8. 8.
    D. L. Dill, editor. Computer-Aided Verification '94.Google Scholar
  9. 9.
    P. Godefroid. Using partial orders to improve automatic verification methods. In E. M. Clarke and R. P. Kurshan, editors, Computer-Aided Verification '90, pages 321–340.Google Scholar
  10. 10.
    H. Hulgaard and S. M. Burns. Bounded delay timing analysis of a class of CSP programs with choice. In International Symposium on Advanced Research in Asynchronous Circuits and Systems, November 1994.Google Scholar
  11. 11.
    H. Hulgaard, S. M. Burns, T. Amon, and G. Borriello. Practical applications of an efficient time separation of events algorithm. In Proc. International Conf. Computer-Aided Design (ICCAD), pages 146–151, November 1993.Google Scholar
  12. 12.
    H. Hulgaard, S. M. Burns, T. Amon, and G. Borriello. An algorithm for exact bounds on the time separation of events in concurrent systems. To appear in IEEE Transactions on Computers. Available as University of Washington CS&E Technical Report #94-02-02. (anonymous ftp: Scholar
  13. 13.
    K. L. McMillan and D. L. Dill. Algorithms for interface timing verification. In 1992 IEEE International Conference on Computer Design: VLSI in Computers and Processors, October 1992.Google Scholar
  14. 14.
    J. L. Peterson. Petri Net Theory and The Modeling of Systems. Prentice-Hall, 1981.Google Scholar
  15. 15.
    C. V. Ramamoorthy and G. S. Ho. Performance evaluation of asynchronous concurrent systems using Petri nets. IEEE Transactions on Software Engineering, SE-6(5):440–448, September 1980.Google Scholar
  16. 16.
    T. G. Rokicki. Representing and Modeling Digital Circuits. Ph.D. thesis, Stanford University, 1993.Google Scholar
  17. 17.
    T. G. Rokicki and C. J. Myers. Automatic verification of timed circuits. In D. L. Dill, editor, Computer-Aided Verification '94, pages 468–480.Google Scholar
  18. 18.
    W. Vogler. Modular Construction and Partial Order Semantics of Petri Nets. LNCS #625. Springer-Verlag, 1992.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1995

Authors and Affiliations

  • Henrik Hulgaard
    • 1
  • Steven M. Burns
    • 1
  1. 1.Department of Computer Science and EngineeringUniversity of WashingtonSeattle

Personalised recommendations