Automated Predicate Abstraction for Real-Time Models
Electronic Proceedings in Theoretical Computer Science2009Vol. 10, pp. 36–43
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.
Related Papers
- → Using Statically Computed Invariants Inside the Predicate Abstraction and Refinement Loop(2006)38 cited
- Timed Automata with non-Instantaneous Actions(2001)
- → Model checking procedures for infinite state systems(2006)2 cited
- Using statically computed invariants inside the predicate abstraction and refinement loop(2006)
- On computing invariants for predicate abstraction by SAT-solving(2009)