Improved BDD-based discrete analysis of timed systems

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

Full description

Saved in:
Bibliographic Details
Main Authors: NGUYEN, Truong Khanh, SUN, Jun, LIU, Yang, DONG, Jin Song, LIU, Yan
Format: text
Language:English
Published: Institutional Knowledge at Singapore Management University 2012
Subjects:
Online Access:https://ink.library.smu.edu.sg/sis_research/5017
https://ink.library.smu.edu.sg/context/sis_research/article/6020/viewcontent/improve_bdd.pdf
Tags: Add Tag
No Tags, Be the first to tag this record!
Institution: Singapore Management University
Language: English
id sg-smu-ink.sis_research-6020
record_format dspace
spelling sg-smu-ink.sis_research-60202020-03-12T09:07:27Z Improved BDD-based discrete analysis of timed systems NGUYEN, Truong Khanh SUN, Jun LIU, Yang DONG, Jin Song LIU, Yan 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-08-01T07:00:00Z text application/pdf https://ink.library.smu.edu.sg/sis_research/5017 info:doi/10.1007/978-3-642-32759-9_28 https://ink.library.smu.edu.sg/context/sis_research/article/6020/viewcontent/improve_bdd.pdf http://creativecommons.org/licenses/by-nc-nd/4.0/ Research Collection School Of Computing and Information Systems eng Institutional Knowledge at Singapore Management University Model Check Linear Temporal Logic Symbolic Model Check Time Automaton State Space Explosion Programming Languages and Compilers Software Engineering
institution Singapore Management University
building SMU Libraries
continent Asia
country Singapore
Singapore
content_provider SMU Libraries
collection InK@SMU
language English
topic Model Check
Linear Temporal Logic
Symbolic Model Check
Time Automaton
State Space Explosion
Programming Languages and Compilers
Software Engineering
spellingShingle Model Check
Linear Temporal Logic
Symbolic Model Check
Time Automaton
State Space Explosion
Programming Languages and Compilers
Software Engineering
NGUYEN, Truong Khanh
SUN, Jun
LIU, Yang
DONG, Jin Song
LIU, Yan
Improved BDD-based discrete analysis of timed systems
description 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.
format text
author NGUYEN, Truong Khanh
SUN, Jun
LIU, Yang
DONG, Jin Song
LIU, Yan
author_facet NGUYEN, Truong Khanh
SUN, Jun
LIU, Yang
DONG, Jin Song
LIU, Yan
author_sort NGUYEN, Truong Khanh
title Improved BDD-based discrete analysis of timed systems
title_short Improved BDD-based discrete analysis of timed systems
title_full Improved BDD-based discrete analysis of timed systems
title_fullStr Improved BDD-based discrete analysis of timed systems
title_full_unstemmed Improved BDD-based discrete analysis of timed systems
title_sort improved bdd-based discrete analysis of timed systems
publisher Institutional Knowledge at Singapore Management University
publishDate 2012
url https://ink.library.smu.edu.sg/sis_research/5017
https://ink.library.smu.edu.sg/context/sis_research/article/6020/viewcontent/improve_bdd.pdf
_version_ 1770575191000219648