Downward Pattern Refinement for Timed Automata

Wehrle, Martin and Kupferschmid, Sebastian. (2016) Downward Pattern Refinement for Timed Automata. International journal on software tools for technology transfer, 18 (1). pp. 41-56.

Full text not available from this repository.

Official URL: http://edoc.unibas.ch/42868/

Downloads: Statistics Overview


Directed model checking is a well-established approach for detecting error states in concurrent systems. A popular variant to find shortest error traces is to apply the A search algorithm with distance heuristics that never overestimate the real error distance. An important class of such distance heuristics is the class of pattern database heuristics. Pattern database heuristics are built on abstractions of the system under consideration. In this paper, we propose downward pattern refinement, a systematic approach for the construction of pattern database heuristics for concurrent systems of timed automata. First, we propose a general framework for pattern databases in the context of timed automata and show that desirable theoretical properties hold for the resulting pattern database. Afterward, we formally define a concept to measure the accuracy of abstractions. Based on this concept, we propose an algorithm for computing succinct abstractions that are still accurate to produce informed pattern databases. We evaluate our approach on large and complex industrial problems. The experiments show the practical potential of the resulting pattern database heuristic.
Faculties and Departments:05 Faculty of Science > Departement Mathematik und Informatik > Informatik > Artificial Intelligence (Helmert)
UniBasel Contributors:Wehrle, Martin
Item Type:Article, refereed
Article Subtype:Research Article
Note:Publication type according to Uni Basel Research Database: Journal article
Identification Number:
Last Modified:05 Apr 2017 13:59
Deposited On:29 Nov 2016 09:07

Repository Staff Only: item control page