The Library
The ideal view on Rackoff's coverability technique
Tools
Lazic, Ranko and Schmitz, Sylvain (2021) The ideal view on Rackoff's coverability technique. Information and Computation, 277 . 104582. doi:10.1016/j.ic.2020.104582 ISSN 0890-5401.
|
PDF
WRAP-ideal-view-Rackoff's-coverability-technique-Lazic-2020.pdf - Accepted Version - Requires a PDF viewer. Available under License Creative Commons Attribution Non-commercial No Derivatives 4.0. Download (1224Kb) | Preview |
Official URL: https://doi.org/10.1016/j.ic.2020.104582
Abstract
Well-structured transition systems form a large class of infinite-state systems, for which safety verification is decidable thanks to a generic backward coverability algorithm. However, for several classes of systems, the generic upper bounds one can extract from the algorithm are far from optimal. In particular, in the case of vector addition systems (VAS) and several of their extensions, the known tight upper bounds were rather derived thanks to ad-hoc arguments based on Rackoff's small witness property.
We show how to derive the same bounds directly on the computations of the VAS instantiation of the generic backward coverability algorithm. This relies on a dual view of the algorithm using ideal decompositions of downwards-closed sets, which exhibits a key structural invariant in the VAS case. This reasoning offers a uniform setting for all well-structured transition systems, including branching ones, and we further apply it to several VAS extensions, deriving optimal upper bounds.
Item Type: | Journal Article | |||||||||
---|---|---|---|---|---|---|---|---|---|---|
Subjects: | Q Science > QA Mathematics | |||||||||
Divisions: | Faculty of Science, Engineering and Medicine > Science > Computer Science | |||||||||
Library of Congress Subject Headings (LCSH): | Mathematics, Algorithms, Vector analysis | |||||||||
Journal or Publication Title: | Information and Computation | |||||||||
Publisher: | Academic Press | |||||||||
ISSN: | 0890-5401 | |||||||||
Official Date: | April 2021 | |||||||||
Dates: |
|
|||||||||
Volume: | 277 | |||||||||
Article Number: | 104582 | |||||||||
DOI: | 10.1016/j.ic.2020.104582 | |||||||||
Status: | Peer Reviewed | |||||||||
Publication Status: | Published | |||||||||
Access rights to Published version: | Restricted or Subscription Access | |||||||||
Date of first compliant deposit: | 2 April 2020 | |||||||||
Date of first compliant Open Access: | 1 April 2021 | |||||||||
RIOXX Funder/Project Grant: |
|
|||||||||
Related URLs: |
Request changes or add full text files to a record
Repository staff actions (login required)
View Item |
Downloads
Downloads per month over past year