Advertisement

Partial Order Path Technique for Checking Parallel Timed Automata

  • Jianhua Zhao
  • He Xu
  • Xuandong Li
  • 1Tao Zheng
  • Guoliang Zheng
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2469)

Abstract

In a parallel composition of timed automata, some transitions are independent to others. Generally the basic method generates one successors for each of the legal permutations of the transitions. These successors may be combined into one bigger symbolic state. In other words, the basic algorithm slices one big symbolic state into pieces. The number of these pieces can be up to n!, where n is the number of independent transitions.

In this paper, we introduce a concept, ‘partial order path’, to avoid treating the permutations one by one. A partial order path includes a set of transitions and a partial order on this set. Our algorithm generates one symbolic successor w.r.t. each partial order path. This big symbolic successor is just the combination of the successors w.r.t. all the global paths which are consistent to this partial order path. It is shown by some case studies that this method may result in significant space reduction.

Keywords

Time Stamp Global Transition Symbolic State Concrete State Local Successor 
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.

References

  1. 1.
    R. Alur and D. Dill. Automata for Modelling Real-Time Systems. In Proc. of ICALP’90, LNCS 443, 1990.Google Scholar
  2. 2.
    Rajeev Alur, Robert K. Brayton, Thomas A. Henzinger, Shaz Qadeer, and Sriram K. Rajamani. Partial-order reduction in symbolic state-space exploration. In Proceedings of the Ninth International Conference on Computer-aided Verification (CAV 1997), LNCS 1254, pages 340–351. Springer-Verlag, 1997.Google Scholar
  3. 3.
    Johan Bengtsson, Bengt Jonsson, Johan Lilius, and Wang Yi. Partial Order Reductions for Timed Systems. In Proc. of the 9th International Conference on Concurrency Theory, September 1998.Google Scholar
  4. 4.
    C. Daws, A. Olivero, S. Tripakis, and S. Yovine. The tool kronos. In DIMACS Workshop on Verification and Control of Hybrid Systems, LNCS 1066. Springer-Verlag, October 1995.Google Scholar
  5. 5.
    F. Pagani. Partial orders and verification of real-time systems. In B. Jonsson and J. Parrow, editors, Proc. of Formal Techniques in Real-Time and Fault-Tolerant Systems, LNCS 1135, pages 327–346. Springer-Verlag, 1996.Google Scholar
  6. 6.
    Kim G Larsen and Paul Pettersson Wang Yi. UPPAAL: Status & Developments. In Orna Grumberg, editor, Proceedings of the 9th International Conference on Computer-Aided Verification. Haifa, Israel,, LNCS 1254, pages 456–459. Springer-Verlag, June 1997.Google Scholar
  7. 7.
    T.A. Henzinger and P.-H. Ho. Hytech: The cornell hybrid technology tool. In Proc. of Workshop on Tools and Algorithms for the Construction and Analysis of Systems, 1995. BRICS report series NS-95-2.Google Scholar
  8. 8.
    Hans van der Schoot. Partial-order verification in spin can be more efficient, http://citeseer.nj.nec.com/vanderschoot97partialorder.html.
  9. 9.
    T.G. Rokicki. Representing and Modeling Circuits, 1993. PhD thesis, Standford University.Google Scholar
  10. 10.
    C.J. Myers, T.G. Rokicki, and T.H.Y. Meng. POSEET timing and its application to the synthesis and verification of gate-level timed circuits. IEEE Transactions on Computer-Aided Design of Integrated Circuits 18(6):769–786, June 1999.Google Scholar
  11. 11.
    W. Belluomini and C. J. Myers. Timed state space exploration using POSETs. IEEE Transactions on Computer-Aided Design of Integrated Circuits, 19(5), May 2000.Google Scholar
  12. 12.
    Sergio Yovine. Kronos: A verification Tool for Real-Time Systems. Springer International Journal of Software Toolls for Technology Transfer 1(1/2), Oct 1997.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Jianhua Zhao
    • 1
  • He Xu
    • 1
  • Xuandong Li
    • 1
  • 1Tao Zheng
  • Guoliang Zheng
    • 1
  1. 1.State Key Laboratory of Novel Software Technology Dept. of Computer Sci. and Tech.Nanjing UniversityNanjing, JiangsuP.R. China

Personalised recommendations