Einzeltreffer — DigiBib

In parametric lock-sharing systems processes can spawn new processes to run in parallel, and can create new locks. The behavior of every process is given by a pushdown automaton. We consider infinite behaviors of such systems under strong process fairness condition. A result of a potentially infinite execution of a system is a limit configuration, that is a potentially infinite tree. The verification problem is to determine if a given system has a limit configuration satisfying a given regular property. This formulation of the problem encompasses verification of reachability as well as of many liveness properties. We show that this verification problem, while undecidable in general, is decidable for nested lock usage. We show Exptime-completeness of the verification problem. The main source of complexity is the number of parameters in the spawn operation. If the number of parameters is bounded, our algorithm works in Ptime for properties expressed by parity automata with a fixed number of ranks. ... : LIPIcs, Vol. 279, 34th International Conference on Concurrency Theory (CONCUR 2023), pages 24:1-24:17 ...

Titel:	Model-Checking Parametric Lock-Sharing Systems Against Regular Constraints ...
Autor/in / Beteiligte Person:	Mascle, Corto ; Muscholl, Anca ; Walukiewicz, Igor
Link:	https://github.com/xvisor/xvisor/commit/e5dd8291b5e3f0c552b9aacc73ef2f000ae14c09 https://nbn-resolving.org/urn:nbn:de:hbz:6-21089543742 https://doi.org/10.4230/LIPIcs.CONCUR.2023 https://doi.org/10.1007/978-3-319-10575-8_21 https://doi.org/10.1007/978-3-030-45190-5_21 https://doi.org/10.4230/LIPIcs.ICALP.2020.111 https://doi.org/10.1145/3498678 https://doi.org/10.2200/S00658ED1V01Y201508DCT013 https://doi.org/10.1007/3-540-63141-0_10 https://doi.org/10.1007/11539452_36 https://doi.org/10.1007/978-3-319-68167-2_15 https://doi.org/10.1145/2842603 https://doi.org/10.1007/978-3-319-63390-9_9 https://doi.org/10.1007/978-3-642-18275-4_15 https://doi.org/10.4230/LIPIcs.FSTTCS.2011.457 https://doi.org/10.1109/LICS.2009.45 https://doi.org/10.1007/11513988_49 https://doi.org/10.4230/lipics.concur.2023.2410.4230/LIPIcs.CONCUR.202310.1007/978-3-319-10575-8_2110.1007/978-3-030-45190-5_2110.4230/LIPIcs.ICALP.2020.11110.1145/349867810.2200/S00658ED1V01Y201508DCT01310.1007/3-540-63141-0_1010.1007/11539452_3610.1007/978-3-319-68167-2_1510.1145/284260310.1007/978-3-319-63390-9_910.1007/978-3-642-18275-4_1510.4230/LIPIcs.FSTTCS.2011.45710.1109/LICS.2009.4510.1007/11513988_49
Veröffentlichung:	Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2023
Medientyp:	Konferenz
DOI:	10.4230/lipics.concur.2023.24
Schlagwort:	Parametric systems Locks Model-checking Theory of computation → Distributed computing models
Sonstiges:	Nachgewiesen in: BASE Sprachen: English Collection: DataCite Metadata Store (German National Library of Science and Technology) Document Type: conference object ; article in journal/newspaper File Description: application/pdf Language: English Rights: info:eu-repo/semantics/openAccess ; Creative Commons Attribution 4.0 International license ; https://creativecommons.org/licenses/by/4.0/legalcode ; cc by 4.0

Klicken Sie ein Format an und speichern Sie dann die Daten oder geben Sie eine Empfänger-Adresse ein und lassen Sie sich per Email zusenden.

BibTeX Citavi, JabRef, u.a.
(Literaturverwaltung)

PDF kein Volltext!
(Merkzettel, Notizen)

RIS Endnote, Citavi u.a.
(Literaturverwaltung)

MODS
(XML zur Weiterverarbeitung)

oder

Wählen Sie das für Sie passende Zitationsformat und kopieren Sie es dann in die Zwischenablage, lassen es sich per Mail zusenden oder speichern es als PDF-Datei.

Gewünschter Zitations-Stil:

oder

Bitte prüfen Sie, ob die Zitation formal korrekt ist, bevor Sie sie in einer Arbeit verwenden. Benutzen Sie gegebenenfalls den "Exportieren"-Dialog, wenn Sie ein Literaturverwaltungsprogramm verwenden und die Zitat-Angaben selbst formatieren wollen.

Model-Checking Parametric Lock-Sharing Systems Against Regular Constraints ...