2026-07-23T16:36:37Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:1739 2024-03-06T10:33:04Z ddc:004 open_access

Analyzing Asynchronous Programs with Preemption Atig, Mohamed Faouzi Bouajjani, Ahmed Touili, Tayssir Multiset Pushdown Systems Multithreaded Asynchronous Programs Program verification Verification algorithms Multiset pushdown systems have been introduced by Sen and Viswanathan as an adequate model for asynchronous programs where some procedure calls can be stored as tasks to be processed later. The model is a pushdown system supplied with a multiset of pending tasks. Tasks may be added to the multiset at each transition, whereas a task is taken from the multiset only when the stack is empty. In this paper, we consider an extension of these models where tasks may be of different priority level, and can be preempted at any point of their execution by tasks of higher priority. We investigate the control point reachability problem for these models. Our main result is that this problem is decidable by reduction to the reachability problem for a decidable class of Petri nets with inhibitor arcs. We also identify two subclasses of these models for which the control point reachability problem is reducible respectively to the reachability problem and to the coverability problem for Petri nets (without inhibitor arcs). Schloss Dagstuhl – Leibniz-Zentrum für Informatik Mohamed Faouzi Atig and Ahmed Bouajjani and Tayssir Touili 2008 Is Part Of LIPIcs, Volume 2, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (2008) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSTTCS.2008.1739 urn:nbn:de:0030-drops-17398 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2008.1739 eng https://creativecommons.org/licenses/by-nc-nd/3.0/legalcode