Partial Order Path Technique for Checking Parallel Timed Automata
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.
KeywordsTime Stamp Global Transition Symbolic State Concrete State Local Successor
- 1.R. Alur and D. Dill. Automata for Modelling Real-Time Systems. In Proc. of ICALP’90, LNCS 443, 1990.Google Scholar
- 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.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.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.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.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.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.Hans van der Schoot. Partial-order verification in spin can be more efficient, http://citeseer.nj.nec.com/vanderschoot97partialorder.html.
- 9.T.G. Rokicki. Representing and Modeling Circuits, 1993. PhD thesis, Standford University.Google Scholar
- 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.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.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