MPI-INF Logo
Publications

Server    halma.mpi-inf.mpg.de

Proceedings Article, Paper


@InProceedings
Beitrag in Tagungsband, Workshop
Author, Editor
Author(s):
Delzanno, Giorgio
Raskin, Jean-François		dblp
dblp
Editor(s):
Graf, Susann
Schwartzbach, Michael I.		dblp
dblp
BibTeX cite key*:
DelzannoRaskinTACAS2000
Title, Booktitle
Title*:
Symbolic Representation of Upward-Closed Sets
Booktitle*:
Proceedings of the 6th Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS-00); Held as Part of the European Joint Conferences on the Theory and Practice of Software (ETAPS-00)
Event, URLs
Conference URL::
Downloading URL:
Event Address*:
Berlin, Germany
Language:
English
Event Date*
(no longer used):
March 25 - April 2, 2000
Organization:
Event Start Date:
21 May 2024
Event End Date:
21 May 2024
Publisher
Name*:
Springer
URL:
Address*:
Berlin, Germany
Type:
Vol, No, Year, pp.
Series:
Lecture Notes in Computer Science
Volume:
1785
Number:
Month:
Pages:
426-440
Year*:
2000
VG Wort Pages:
ISBN/ISSN:
3-540-67282-6
Sequence Number:
DOI:
Note, Abstract, ©
(LaTeX) Abstract:
      Abstract. The control state reachability problem is decidable for well-structured infinite-state
      systems like unbounded Petri Nets, Vector Addition Systems, Lossy Petri Nets, and Broadcast
      Protocols. An abstract algorithm that solves the problem is given in [ACJT96,FS99]. The algorithm
      computes the closure of the predecessor operator w.r.t. a given upward-closed set of target
      states. When applied to this class of verification problems, traditional (infinite-state) symbolic
      model checkers suffer from the state explosion problem even for very small examples. We
      provide BDD-like data structures to represent in a compact way collections of upwards closed
      sets over numerical domains. This way, we turn the abstract algorithm of [ACJT96,FS99] into a
      practical method. Preliminary experimental results indicate the potential usefulness of our
      method.
URL for the Abstract:
http://link.springer.de/link/service/series/0558/papers/1785/17850426.pdf
Download
Access Level:

Correlation
MPG Unit:
Max-Planck-Institut für Informatik
MPG Subunit:
Programming Logics Group
Audience:
experts only
Appearance:
MPII WWW Server, MPII FTP Server, MPG publications list, university publications list, working group publication list, Fachbeirat



BibTeX Entry:
@INPROCEEDINGS{DelzannoRaskinTACAS2000,
AUTHOR = {Delzanno, Giorgio and Raskin, Jean-François},
 EDITOR = {Graf, Susann and Schwartzbach, Michael I.},
 TITLE = {Symbolic Representation of Upward-Closed Sets},
 BOOKTITLE = {Proceedings of the 6th Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS-00); Held as Part of the European Joint Conferences on the Theory and Practice of Software (ETAPS-00)},
 PUBLISHER = {Springer},
 YEAR = {2000},
 VOLUME = {1785},
 PAGES = {426--440},
 SERIES = {Lecture Notes in Computer Science},
 ADDRESS = {Berlin, Germany},
 ISBN = {3-540-67282-6},
}

Entry last modified by Christine Kiesel, 03/12/2010
Hide details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)

Editor(s)
Christine Kiesel		Created
08/28/2001 10:25:46 AM
Revision
1.
0.


Editor
Christine Kiesel
Christine Kiesel


Edit Date
28.08.2001 10:47:37 AM
28.08.2001 10:45:20 AM