×

zbMATH — the first resource for mathematics

Remove irrelevant atomic formulas for timed automaton model checking. (English) Zbl 1190.68038
Summary: Most of the timed automata reachability analysis algorithms in the literature explore the state spaces by enumeration of symbolic states, which use time constraints to represent a set of concrete states. A time constraint is a conjunction of atomic formulas which bound the differences of clock values. In this paper, it is shown that some atomic formulas of symbolic states generated by the algorithms can be removed to improve the model checking time- and space-efficiency. Such atomic formulas are called as irrelevant atomic formulas. A method is also presented to detect irrelevant formulas based on the test-reset information about clock variables. An optimized model-checking algorithm is designed based on these techniques. The case studies show that the techniques presented in this paper significantly improve the space- and time-efficiency of reachability analysis.
MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
68Q45 Formal languages and automata
Software:
HyTech; Kronos; Uppaal
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Kim G Larsen, Paul Pettersson, Wang Yi. UPPAAL: Status & Developments. In Proc. the 9th International Conference on Computer-Aided Verification, Orna Grumberg, (ed.), Haifa, Israel, Springer-Verlag, June 1997, LNCS 1254, pp.456–459.
[2] Daws C, Olivero A, Tripakis S, Yovine S. The tool Kronos. In DIMACS Workshop on Verification and Control of Hybrid Systems, LNCS 1066, Springer-Verlag, October 1995.
[3] Henzinger T A, Ho P H. Hytech: The Cornell hybrid technology tool. In Proc. Workshop on Tools and Algorithms for the Construction and Analysis of Systems, 1995, BRICS report series NS-95-2.
[4] Rajeev Alur, David L Dill. A theory of timed automata. Journal of Theoretical Computer Science, 1994, 126(2): 183–235. · Zbl 0803.68071 · doi:10.1016/0304-3975(94)90010-8
[5] Gerd Behrmann, Alexandre David, Kim Guldstrand Larsen. A Tutorial on UPPAAL. In Formal Methods for the Design of Real-Time Systems, International School on Formal Methods for the Design of Computer, Communication and Software Systems, SFM-RT 2004, Bertinoro, Italy, September 13–18, 2004, Revised Lectures, Lecture Notes in Computer Science 3185, Springer 2004, ISBN 3-540-23068-8. · Zbl 1105.68350
[6] Tomas Gerhard Rokicki. Representing and modeling digital circuits [Dissertation]. Stanford University, 1993.
[7] Johan Bengtsson. Clocks, DBMs and states in timed systems, [Dissertation], Uppsala University, 2002.
[8] Zhao Jianhua, Dang Van Hung. Checking timed automata for linear duration properties. Journal of Computer Science and Technology, Sept. 2000, 15(5): 423–429. · Zbl 0961.68079 · doi:10.1007/BF02950405
[9] Li Yong, Dang Van Hung. Checking temporal duration properties of timed automata. Journal of Computer Science and Technology, Nov. 2002, 17(6): 689–698. · Zbl 1056.68096 · doi:10.1007/BF02960759
[10] Zhao Jianhua, Li Xuandong, Zheng Tao, Zheng Guoliang. Removing irrelevant atomic formulas for checking timed automata efficiently. In Proc. FORMATS’03, Marseille, France, September 6–7, 2003, LNCS 2791, pp.34–45. · Zbl 1099.68060
[11] Kalus Havelund, Arne Skou, Kim G Larsen, Kristian Lund. Formal modelling and analysis of an audio/video protocol: An industrial case study using UPPAAL. In Proc. of 18th IEEE Real-Time Systems Symposium, IEEE Computer Society Press, December 1997, pp.2–13.
[12] Daws C, Yovine S. Reducing the number of clock variables of timed automata. In Proc. the 17th IEEE Real Time Systems Symposium, RTSS’96, Washington DC, USA, December 1996, IEEE Computer Society Press, pp.73–81.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.