Automated Predicate Abstraction for Real-Time Models

TL;DR

This paper introduces an automated method for creating predicate abstractions of dense real-time models using timed automata, enhancing model analysis with invariant-based pruning.

Contribution

It extends previous work by integrating control location invariants into predicate abstraction for dense real-time models.

Findings

Effective abstraction of dense real-time models

Improved model analysis through invariant-based pruning

Automation reduces manual effort in model abstraction

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.