Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Fair termination for parameterized probabilistic concurrent systems
FIT, Brno University of Technology, Czech Republic.
Department of Computer Science, University of Oxford, UK.
MPI-SWS Kaiserslautern, Germany.
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems. (Embedded Systems)ORCID iD: 0000-0002-2733-7098
2017 (English)In: Tools and Algorithms for the Construction and Analysis of Systems: Part I, Springer, 2017, p. 499-517Conference paper, Published paper (Refereed)
Abstract [en]

We consider the problem of automatically verifying that a parameterized family of probabilistic concurrent systems terminates with probability one for all instances against adversarial schedulers. A parameterized family defines an infinite-state system: for each number n, the family consists of an instance with n finite-state processes. In contrast to safety, the parameterized verification of liveness is currently still considered extremely challenging especially in the presence of probabilities in the model. One major challenge is to provide a sufficiently powerful symbolic framework. One well-known symbolic framework for the parameterized verification of non-probabilistic concurrent systems is regular model checking. Although the framework was recently extended to probabilistic systems, incorporating fairness in the framework-often crucial for verifying termination-has been especially difficult due to the presence of an infinite number of fairness constraints (one for each process). Our main contribution is a systematic, regularity-preserving, encoding of finitary fairness (a realistic notion of fairness proposed by Alur and Henzinger) in the framework of regular model checking for probabilistic parameterized systems. Our encoding reduces termination with finitary fairness to verifying parameterized termination without fairness over probabilistic systems in regular model checking (for which a verification framework already exists). We show that our algorithm could verify termination for many interesting examples from distributed algorithms (Herman's protocol) and evolutionary biology (Moran process, cell cycle switch), which do not hold under the standard notion of fairness. To the best of our knowledge, our algorithm is the first fully-automatic method that can prove termination for these examples.

Place, publisher, year, edition, pages
Springer, 2017. p. 499-517
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 10205
National Category
Computer Sciences
Identifiers
URN: urn:nbn:se:uu:diva-337240DOI: 10.1007/978-3-662-54577-5_29ISI: 000440734900029ISBN: 978-3-662-54576-8 (print)OAI: oai:DiVA.org:uu-337240DiVA, id: diva2:1168663
Conference
23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) 2017, April 22–29, Uppsala, Sweden
Funder
Swedish Research Council, 2014-5484EU, European Research Council, 610150Available from: 2017-03-31 Created: 2017-12-21 Last updated: 2018-11-19Bibliographically approved

Open Access in DiVA

fulltext(785 kB)14 downloads
File information
File name FULLTEXT01.pdfFile size 785 kBChecksum SHA-512
dd382b3530ccc04d3ddfe7bd72435879d8ba8de238682542a2086ea53043da94037601e1840867218d7911ae80f4a2c09037c06f0e40a55d619e33775926bee3
Type fulltextMimetype application/pdf

Other links

Publisher's full text

Search in DiVA

By author/editor
Rümmer, Philipp
By organisation
Computer Systems
Computer Sciences

Search outside of DiVA

GoogleGoogle Scholar
Total: 14 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

doi
isbn
urn-nbn

Altmetric score

doi
isbn
urn-nbn
Total: 60 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf