HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Conference papers

Verification of Timed Automata Using Rewrite Rules and Strategies

Emmanuel Beffara 1 Olivier Bournez 1 Hassen Kacem 1 Claude Kirchner 1
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : 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.
Keywords : rewriting theory timed automata automates temporisés vérification réécriture
Document type :
Conference papers
Complete list of metadata
https://hal.inria.fr/inria-00100535
Contributor : Publications Loria Connect in order to contact the contributor
Submitted on : Tuesday, September 26, 2006 - 2:46:31 PM
Last modification on : Friday, May 13, 2022 - 10:18:05 PM

Identifiers

  • HAL Id : inria-00100535, version 1

Collections

INRIA | CNRS | LORIA | UNIV-LORRAINE | INRIA2

Citation

Emmanuel Beffara, Olivier Bournez, Hassen Kacem, Claude Kirchner. Verification of Timed Automata Using Rewrite Rules and Strategies. The Seventh Biennal Bar-Ilan Symposium on the Foundations of Artificial Intelligence - BISFAI'01, Jun 2001, Bar-Ilan University, Ramat-Gan, Israel, 15 p. ⟨inria-00100535⟩

Export

BibTeX TEI DC DCterms EndNote Datacite

Share

Metrics

Record views

43

 

Contact                    Legal Notice                    Personal Data