Publication Details

Verification of Parametric Concurrent Systems with Prioritized FIFO Resource Management

BOUAJJANI Ahmed, HABERMEHL Peter and VOJNAR Tomáš. Verification of Parametric Concurrent Systems with Prioritized FIFO Resource Management. Lecture Notes in Computer Science, vol. 2003, no. 2761, pp. 174-190. ISSN 0302-9743.
Czech title
Verifikace parametrických systémů paralelních procesů s prioritním FIFO řízením přístupu ke sdíleným zdrojům
Type
journal article
Language
english
Authors
Bouajjani Ahmed (UPAR7)
Habermehl Peter (UPAR7)
Vojnar Tomáš, prof. Ing., Ph.D. (DITS FIT BUT)
URL
Keywords

formal verification, parameterized concurrent systems, cut-offs

Abstract

We consider the problem of parametric verification over a class of systems of processes competing for access to shared resources. We suppose the access to the resources to be controlled according to a FIFO-based policy with a possibility of distinguishing low-priority and high-priority resource requests. We propose a model of the concerned systems based on extended automata with queues. Over this model, we address verification of properties expressed in LTL\X enriched with global process quantification and interpreted on finite as well as fair behaviours of the given systems. In addition, we examine parametric verification of process deadlockability too. By reducing the parametric verification problems to finite-state model checking, we establish several decidability results for different classes of the considered properties and systems (including the special case of systems with the pure FIFO resource management). Moreover, we show that parametric verification against formulae with local process quantification is undecidable in the given context.

Published
2003
Pages
174-190
Journal
Lecture Notes in Computer Science, vol. 2003, no. 2761, ISSN 0302-9743
Book
Concurrency Theory
Publisher
Springer Verlag
Place
Berlin, DE
BibTeX
@ARTICLE{FITPUB7343,
   author = "Ahmed Bouajjani and Peter Habermehl and Tom\'{a}\v{s} Vojnar",
   title = "Verification of Parametric Concurrent Systems with Prioritized FIFO Resource Management",
   pages = "174--190",
   booktitle = "Concurrency Theory",
   journal = "Lecture Notes in Computer Science",
   volume = 2003,
   number = 2761,
   year = 2003,
   location = "Berlin, DE",
   publisher = "Springer Verlag",
   ISSN = "0302-9743",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/7343"
}
Back to top