Checking timed Büchi automata emptiness on simulation graphs

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback
Take a look at the new version of this page: [ beta version ]. Tell us what you think.

Checking timed Büchi automata emptiness on simulation graphs

Full text

Pdf (291 KB)

Source

ACM Transactions on Computational Logic (TOCL) archive
Volume 10 , Issue 3 (April 2009) table of contents

Article No.: 15

Year of Publication: 2009

ISSN:1529-3785

Author

Stavros Tripakis

University of California, Berkeley, CA

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 6, Downloads (12 Months): 132, Citation Count: 0

Additional Information:

abstract references index terms collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/1507244.1507245 What is a DOI?

ABSTRACT

Timed automata [Alur and Dill 1994] comprise a popular model for describing real-time and embedded systems and reasoning formally about them. Efficient model-checking algorithms have been developed and implemented in tools such as Kronos [Daws et al. 1996] or Uppaal [Larsen et al. 1997] for checking safety properties on this model, which amounts to reachability. These algorithms use the so-called zone-closed simulation graph, a finite graph that admits efficient representation and has been recently shown to preserve reachability [Bouyer 2004]. Building upon Bouyer [2004] and our previous work [Bouajjani et al. 1997; Tripakis et al. 2005], we show that this graph can also be used for checking liveness properties, in particular, emptiness of timed Büchi automata.

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	Rajeev Alur , Costas Courcoubetis , David Dill, Model-checking in dense real-time, Information and Computation, v.104 n.1, p.2-34, May 1993 [doi>10.1006/inco.1993.1024]
	2	Rajeev Alur , David L. Dill, A theory of timed automata, Theoretical Computer Science, v.126 n.2, p.183-235, April 25, 1994 [doi>10.1016/0304-3975(94)90010-8]
	3	Behrmann, G., Bouyer, P., Larsen, K., and Pelánek, R. 2004. Lower and upper bounds in zone based abstractions of timed automata. In Proceedings of the Workshop on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'04). Lecture Notes in Computer Science, vol. 2988. Springer.
	4	Bengtsson, J. and Yi, W. 2003. On clock difference constraints and termination in reachability analysis of timed automata. In Proceedings of the IEEE International Conference of Formal Engineering Methods (ICFEM'03). Lecture Notes in Computer Science, vol. 2885. Springer.
	5	Berthomieu, B. and Menasche, M. 1983. An enumerative approach for analyzing time Petri nets. IFIP Congress Series 9, 41--46.
	6	A. Bouajjani , S. Tripakis , S. Yovine, On-the-fly symbolic model checking for real-time systems, Proceedings of the 18th IEEE Real-Time Systems Symposium, p.25, December 03-05, 1997
	7	Patricia Bouyer, Forward Analysis of Updatable Timed Automata, Formal Methods in System Design, v.24 n.3, p.281-320, May 2004 [doi>10.1023/B:FORM.0000026093.21513.31]
	8	Clarke, E., Grumberg, O., and Peled, D. 2000. Model Checking. MIT Press.
	9	E. M. Clarke , E. A. Emerson , A. P. Sistla, Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.8 n.2, p.244-263, April 1986 [doi>10.1145/5397.5399]
	10	C. Courcoubetis , M. Vardi , P. Wolper , M. Yannakakis, Memory-efficient algorithms for the verification of temporal properties, Formal Methods in System Design, v.1 n.2-3, p.275-288, Oct. 1992 [doi>10.1007/BF00121128]
	11	C. Daws , A. Olivero , S. Tripakis , S. Yovine, The tool KRONOS, Proceedings of the DIMACS/SYCON workshop on Hybrid systems III : verification and control: verification and control, p.208-219, July 1996, New Brunswick, NeW Jersey, United States
	12	Conrado Daws , Stavros Tripakis, Model Checking of Real-Time Reachability Properties Using Abstractions, Proceedings of the 4th International Conference on Tools and Algorithms for Construction and Analysis of Systems, p.313-329, March 28-April 04, 1998
	13	David L. Dill, Timing Assumptions and Verification of Finite-State Concurrent Systems, Proceedings of the International Workshop on Automatic Verification Methods for Finite State Systems, p.197-212, June 12-14, 1989
	14	Thomas A. Henzinger , Xavier Nicollin , Joseph Sifakis , Sergio Yovine, Symbolic model checking for real-time systems, Information and Computation, v.111 n.2, p.193-244, June 1994 [doi>10.1006/inco.1994.1045]
	15	L. Lamport, Proving the Correctness of Multiprocess Programs, IEEE Transactions on Software Engineering, v.3 n.2, p.125-143, March 1977 [doi>10.1109/TSE.1977.229904]
	16	Larsen, K., Petterson, P., and Yi, W. 1997. Uppaal in a nutshell. Softw. Tools Technol. Transfer 1, 1-2.
	17	Jean-Pierre Queille , Joseph Sifakis, Specification and verification of concurrent systems in CESAR, Proceedings of the 5th Colloquium on International Symposium on Programming, p.337-351, April 06-08, 1982
	18	Tarjan, R. 1972. Depth first search and linear graph algorithms. SIAM J. Comput. 1, 2, 146--170.
	19	Stavros Tripakis , Costas Courcoubetis, Extending Promela and Spin for Real Time, Proceedings of the Second International Workshop on Tools and Algorithms for Construction and Analysis of Systems, p.329-348, March 27-29, 1996
	20	Stavros Tripakis , Sergio Yovine, Analysis of Timed Systems Using Time-Abstracting Bisimulations, Formal Methods in System Design, v.18 n.1, p.25-68, January.2001 [doi>10.1023/A:1008734703554]
	21	Stavros Tripakis , Sergio Yovine , Ahmed Bouajjani, Checking Timed Büchi Automata Emptiness Efficiently, Formal Methods in System Design, v.26 n.3, p.267-292, May 2005 [doi>10.1007/s10703-005-1632-8]