Show simple item record

dc.contributor.author
Lampka, Kai
dc.date.accessioned
2017-06-09T00:14:39Z
dc.date.available
2017-06-09T00:14:39Z
dc.date.issued
2009
dc.identifier.uri
http://hdl.handle.net/20.500.11850/21567
dc.description.abstract
Modeling formalisms allow one to compactly describe complexsystems. But, once it comes to the actual analysis the high-level descriptions are commonly required to be transformed into flat statetransition systems (ST-systems), e.g. for asserting system properties by means of model checking techniques. Decision Diagrams and their algorithms are well accepted for carrying out the above mentioned transformation. This paper introduces a combined procedure for efficientlyconstructing a Binary Decision Diagram (BDD) which represents the ST-system underlying a high-level model such as a Petri net, UML state chart, set of reactive modules, etc.. The proposed scheme is independent of the model description method, as it combines state enumeration with symbolic, i. e., BDD-based, state space construction techniques. In contrast to existing techniques it exploits state-counter and activity-driven decomposition of high-level models, as this severely reduces the number of state enumerations and softens the hill climbing problem commonly attached to the incremental construction of BDDs. As shown in an empirical evaluation, the proposed technique has the potential not only for outperforming other combined approaches, but is also competitive w. r. t. other fully symbolic state space construction techniques.
dc.language.iso
en
dc.publisher
Computer Engineering and Networks Laboratory, ETH
dc.title
Re-visiting Partitioned Symbolic State Graph Generation for high-level models
dc.type
Report
ethz.journal.title
TIK report
ethz.journal.issue
308
ethz.size
19 p.
ethz.identifier.nebis
000901696
ethz.publication.place
Zürich
ethz.publication.status
published
ethz.date.deposited
2017-06-09T00:15:04Z
ethz.source
ECIT
ethz.identifier.importid
imp59364ccd7e7b796075
ethz.ecitpid
pub:34233
ethz.eth
yes
ethz.availability
Metadata only
ethz.rosetta.installDate
2017-07-14T18:18:41Z
ethz.rosetta.lastUpdated
2017-07-14T18:18:41Z
ethz.rosetta.versionExported
true
ethz.COinS
ctx_ver=Z39.88-2004&rft_val_fmt=info:ofi/fmt:kev:mtx:journal&rft.atitle=Re-visiting%20Partitioned%20Symbolic%20State%20Graph%20Generation%20for%20high-level%20models&rft.jtitle=TIK%20report&rft.date=2009&rft.issue=308&rft.au=Lampka,%20Kai&rft.genre=report&
 Search print copy at ETH Library

Files in this item

FilesSizeFormatOpen in viewer

There are no files associated with this item.

Publication type

Show simple item record