|
Agata Pó³rola, Wojciech Penczek, Maciej Szreter
Reachability Analysis for Timed Automata Based on Partitioning
961
Abstract
Model checking is an approach commonly applied for automated verification
of reachability properties. Given a system $S$ and a property $p$,
reachability model checking consists in an exploration of the state space
of $S$, checking whether there exists a state where $p$ holds.
Since concrete state spaces (models) of timed systems are usually
infinite, they cannot be directly applied to model checking. One of the
solution to this problem is to exploit finite abstract models,
preseving the properties of interest. The paper presents a new method of
buildng abstract models for Timed Automata, based on a partitioning
algorithm. Our pseudo-bisimulating models are often smaller than
forward-reachability graphs , commonly used in reachability
analysis. The method enables verification on-the-fly, i.e., generating of
the model can be stopped as soon as a state satisfying $p$ is found.
Keywords :model checking, Timed Automata,
reachability, abstract models, minimization.
|
|
 |
 |
