Rules and Strategies: A Framework for Model-Checking Timed Automata

Title: Rules and Strategies: A Framework for Model-Checking Timed Automata

Research Question: Can the ELAN system, based on rewriting calculus, be used to prototype model-checking algorithms for timed automata, and what are the advantages of using such a formal tool compared to conventional programming languages?

Methodology: The researchers used the ELAN system, which is a powerful language and environment for specifying and prototyping deduction systems in a language based on rewrite rules controlled by strategies. They focused on implementing model-checking algorithms for timed automata, a class of continuous real-time models of reactive systems.

Results: The researchers successfully implemented a tool for verifying reachability properties of product of timed automata using the ELAN system. They found that the system's combination of exploration rules, deduction rules, constraint solving techniques, and decision procedures made it suitable for prototyping model-checking algorithms.

Implications: The use of the ELAN system for prototyping model-checking algorithms offers several advantages. First, it allows for clear flexibility in customizing the algorithms, unlike hard-wired model checkers. Second, the ELAN compiler's efficiency ensures performances are close to dedicated model-checking tools. Overall, this approach demonstrates the power and suitability of rewriting calculus as a framework for understanding and formalizing combinations of proving and constraint-solving techniques.

Link to Article: https://arxiv.org/abs/0109024v1 Authors: arXiv ID: 0109024v1