Automated Predicate Abstraction for Real-Time Models

Bahareh Badban
(Konstanz university)
Stefan Leue
(Konstanz university)
Jan-Georg Smaus
(Freiburg University)

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.

In Axel Legay: Proceedings International Workshop on Verification of Infinite-State Systems (INFINITY 2009), Bologna, Italy, 31th August 2009, Electronic Proceedings in Theoretical Computer Science 10, pp. 36–43.
Published: 17th November 2009.

ArXived at: http://dx.doi.org/10.4204/EPTCS.10.3 bibtex PDF

Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org