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 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.

@article{Begdouri2016,
  title     = {An Algorithmic approach for abstracting transient states in timed systems},
  journal   = {International Journal of Advanced Computer Science and Applications},
  volume    = {7},
  number    = {5},
  year      = {2016},
  publisher = {The Science and Information Organization},
  author    = {Mohammed Achkari Begdouri and Houda Bel Mokadem and Mohamed El Haddad},
  doi       = {10.14569/IJACSA.2016.070567},
  url       = {https://doi.org/10.14569/IJACSA.2016.070567}
}