Verification of Timed Automata Using Rewrite Rules and Strategies

Autor:	Beffara, Emmanuel, Bournez, Olivier, Kacem, Hassen, Kirchner, Claude
Rok vydání:	2009
Předmět:	Computer Science - Logic in Computer Science
Druh dokumentu:	Working Paper
Popis:	ELAN is a powerful language and environment for specifying and prototyping deduction systems in a language based on rewrite rules controlled by strategies. Timed automata is a class of continuous real-time models of reactive systems for which efficient model-checking algorithms have been devised. In this paper, we show that these algorithms can very easily be prototyped in the ELAN system. This paper argues through this example that rewriting based systems relying on rules and strategies are a good framework to prototype, study and test rather efficiently symbolic model-checking algorithms, i.e. algorithms which involve combination of graph exploration rules, deduction rules, constraint solving techniques and decision procedures. Comment: In the Proceedings BISFAI 2001, Seventh Biennial Bar-Ilan International Symposium on the Foundations of Artificial Intelligence. Ramat-Gan, 2001
Databáze:	arXiv
Externí odkaz:	http://arxiv.org/abs/0907.3123 Zobrazit plný text záznamu View this record from Arxiv