Automated Predicate Abstraction for Real-Time Models
Logic in Computer Science
2009-11-18 v1 Formal Languages and Automata Theory
Abstract
We present a technique designed to automatically compute predicate abstractions for dense real-timed models represented as networks of timed automata. We use the CIPM algorithm in our previous work which computes new invariants for timed automata control locations and prunes the model, to compute a predicate abstraction of the model. We do so by taking information regarding control locations and their newly computed invariants into account.
Keywords
Cite
@article{arxiv.0911.3277,
title = {Automated Predicate Abstraction for Real-Time Models},
author = {Bahareh Badban and Stefan Leue and Jan-Georg Smaus},
journal= {arXiv preprint arXiv:0911.3277},
year = {2009}
}