An Algorithmic approach for abstracting transient states in timed systems
Journal Title: International Journal of Advanced Computer Science & Applications - Year 2016, Vol 7, Issue 5
Abstract
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.
Authors and Affiliations
Mohammed Begdouri, Houda Mokadem, Mohamed Haddad
Keywords
Related Articles
- EP ID EP101673
- DOI 10.14569/IJACSA.2016.070567
- Views 104
- Downloads 0
Impact of Android Phone Rooting on User Data Integrity in Mobile Forensics
Modern cellular phones are potent computing de-vices, and their capabilities are constantly progressing. The Android operating system (OS) is widely used, and the number of accessible apps for Android OS phones is unprec...
DES: Dynamic and Elastic Scalability in Cloud Computing Database Architecture
Nowadays, companies are becoming global organizations. Such organizations do not limit themselves in conducting business in one country. They need dynamic, elastic, scalable cloud computing platform that operates around-...
The result oriented process for students based on distributed datamining
The student result oriented learning process evaluation system is an essential tool and approach for monitoring and controlling the quality of learning process. From the perspective of data analysis, this pap...
Towards Privacy Preserving Commutative Encryption-Based Matchmaking in Mobile Social Network
The last decade or so has witnessed a sharp rise in the growth of mobile devices. These mobile devices and wireless communication technologies enable people around the globe to instantaneously communicate with each other...
A New Steganography Technique using JPEG Images
Steganography is a form of security technique that using ambiguity to hide a secret message within an ordinary message between senders and receivers. In this paper, we propose a new steganography technique for hiding dat...