Proceedings Article, Paper
@InProceedings
Beitrag in Tagungsband, Workshop


Show entries of:

this year (2019) | last year (2018) | two years ago (2017) | Notes URL

Action:

login to update

Options:








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

URL of the conference:


URL for downloading the paper:


Event Address*:

Berlin, Germany

Language:

English

Event Date*
(no longer used):

March 25 - April 2, 2000

Organization:


Event Start Date:

17 September 2019

Event End Date:

17 September 2019

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
Show details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)
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