Please use this identifier to cite or link to this item: https://doi.org/10.1007/978-3-642-32759-9_28
Title: Improved BDD-based discrete analysis of timed systems
Authors: Nguyen, T.K.
Sun, J.
Liu, Y. 
Dong, J.S. 
Liu, Y.
Issue Date: 2012
Source: Nguyen, T.K.,Sun, J.,Liu, Y.,Dong, J.S.,Liu, Y. (2012). Improved BDD-based discrete analysis of timed systems. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 7436 LNCS : 326-340. ScholarBank@NUS Repository. https://doi.org/10.1007/978-3-642-32759-9_28
Abstract: Model checking timed systems through digitization is relatively easy, compared to zone-based approaches. The applicability of digitization, however, is limited mainly for two reasons, i.e., it is only sound for closed timed systems; and clock ticks cause state space explosion. The former is mild as many practical systems are subject to digitization. It has been shown that BDD-based techniques can be used to tackle the latter to some extent. In this work, we significantly improve the existing approaches by keeping the ticks simple in the BDD encoding. Taking advantage of the 'simple' nature of clock ticks, we fine-tune the encoding of ticks and are able to verify systems with many ticks. Furthermore, we develop a BDD library which supports not only encoding/verifying of timed state machines (through digitization) but also composing timed components using a rich set of composition functions. The usefulness and scalability of the library are demonstrated by supporting two languages, i.e., closed timed automata and Stateful Timed CSP. © 2012 Springer-Verlag.
Source Title: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
URI: http://scholarbank.nus.edu.sg/handle/10635/43166
ISBN: 9783642327582
ISSN: 03029743
DOI: 10.1007/978-3-642-32759-9_28
Appears in Collections:Staff Publications

Show full item record
Files in This Item:
There are no files associated with this item.

SCOPUSTM   
Citations

9
checked on Dec 13, 2017

Page view(s)

57
checked on Dec 16, 2017

Google ScholarTM

Check

Altmetric


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.