An Algorithmic approach for abstracting transient states in timed systems

In previous works, the timed logic TCTL was extended with importants modalities, in order to abstract transient states that last for less than k time units. For all modalities of this extension, called TCTL?, the decidability of the model-checking problem has been proved with an appropriate extensio...

Full description

Saved in:
Bibliographic Details
Published in:International journal of advanced computer science & applications 2016-01, Vol.7 (5)
Main Authors: Achkari, Mohammed, Bel, Houda, El, Mohamed
Format: Article
Language:English
Subjects:
Algorithms
Data structures
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:In previous works, the timed logic TCTL was extended with importants modalities, in order to abstract transient states that last for less than k time units. For all modalities of this extension, called TCTL?, the decidability of the model-checking problem has been proved with an appropriate extension of Alur and Dill’s region graph. But this theoretical result does not support a natural implementation due to its state-space explosion problem. This is not surprising since, even for TCTL timed logics, the model checking algorithm that is implemented in tools like UPPAAL or KRONOS is based on a so-called zone algorithm and data structures like DBMs, rather than on explicit sets of regions. In this paper, we propose a symbolic model-checking algorithm which computes the characteristic sets of some TCTL? formulae and checks their truth values. This algorithm generalizes the zone algorithm for TCTL timed logics. We also present a complete correctness proof of this algorithm, and we describe its implementation using the DBM data structure.
ISSN:2158-107X
2156-5570
DOI:10.14569/IJACSA.2016.070567