# Bounded Context Switching for Valence Systems

@article{Meyer2018BoundedCS, title={Bounded Context Switching for Valence Systems}, author={Roland Meyer and Sebastian Muskalla and Georg Zetzsche}, journal={ArXiv}, year={2018}, volume={abs/1803.09703} }

We study valence systems, finite-control programs over infinite-state memories modeled in terms of graph monoids. Our contribution is a notion of bounded context switching (BCS). Valence systems generalize pushdowns, concurrent pushdowns, and Petri nets. In these settings, our definition conservatively generalizes existing notions. The main finding is that reachability within a bounded number of context switches is in NP, independent of the memory (the graph monoid). Our proof is genuinely… Expand

#### 3 Citations

Scope-Bounded Reachability in Valence Systems

- Computer Science
- CONCUR
- 2021

This work proposes a notion of scope boundedness that coincides with the classical notion when the storage mechanism happens to be a multi-pushdown and shows that with this notion, reachability can be decided in PSPACE for every storage mechanism in the framework. Expand

Reachability of scope-bounded multistack pushdown systems

- Computer Science
- Inf. Comput.
- 2020

The semantics of a multi-stack pushdown system with scope-bounded matching relations are restricted such that a symbol that is pushed onto a stack can be popped only within a given number of contexts involving s, i.e., the scope of matching push and pop transitions is bound. Expand

Context-Bounded Verification of Thread Pools

- Computer Science
- ArXiv
- 2021

The main result, the EXPSPACE upper bound, is derived using a sequence of new succinct encoding techniques of independent language-theoretic interest, which shows a polynomial-time construction of downward closures of languages accepted by succinct pushdown automata as doubly succinct nondeterministic finite automata. Expand

#### References

SHOWING 1-10 OF 60 REFERENCES

The Language Theory of Bounded Context-Switching

- Computer Science
- LATIN
- 2010

This paper considers the language theory of these models: concurrent recursive programs with finite data domains that communicate using shared memory and work within k round-robin rounds of context-switches, and where further the stack operations are made visible (as in visibly pushdown automata), and shows that these automata are determinizable as well. Expand

On the Reachability Analysis of Acyclic Networks of Pushdown Systems

- Mathematics, Computer Science
- CONCUR
- 2008

It is proved mainly that the reachability problem between recognizable sets of configurations is decidable for acyclic networks of pushdown systems, and that for lossy channel pushdown networks, the channel language is effectively recognizable. Expand

On Bounded Reachability Analysis of Shared Memory Systems

- Mathematics, Computer Science
- FSTTCS
- 2014

This paper addresses the reachability problem for pushdown systems communicating via shared memory and proposes a restriction on the behaviours of such systems, called stage bound, towards decidability. Expand

Context-Bounded Analysis of Concurrent Queue Systems

- Computer Science
- TACAS
- 2008

We show that the bounded context-switching reachability problem for concurrent finite systems communicating using unbounded FIFO queues is decidable, where in each context a process reads from only… Expand

On the Complexity of Bounded Context Switching

- Mathematics, Computer Science
- ESA
- 2017

A parameterized analysis of BCS and proves that BCS admits no polynomial kernel, and an algorithm that solves BCS when parameterized by the number of context switches and the size of the memory in O*(m^ (cs)2^(cs)). Expand

Reachability of Multistack Pushdown Systems with Scope-Bounded Matching Relations

- Mathematics, Computer Science
- CONCUR
- 2011

This paper proposes a restriction of the semantics of the general model such that a symbol that is pushed onto a stack can be popped only within a bounded number of context-switches. Expand

The Emptiness Problem for Valence Automata over Graph Monoids

- Computer Science, Mathematics
- Inf. Comput.
- 2021

A model that naturally generalizes both pushdown Petri nets and the priority multicounter machines introduced by Reinhardt is presented, and is shown that this model can be combined with another such extension by Atig and Ganty. Expand

Synchronisation- and Reversal-Bounded Analysis of Multithreaded Programs with Counters

- Computer Science
- CAV
- 2012

It is shown that the synchronisation-bounded reachability problem can be efficiently reduced to the satisfaction of an existential Presburger formula, meaning the problem is NP-complete and can be tackled with efficient SMT solvers such as Z3. Expand

The tree width of auxiliary storage

- Computer Science
- POPL '11
- 2011

This work outlines a uniform mechanism to derive emptiness algorithms for automata, explaining and simplifying several existing results, as well as proving new decidability results. Expand

Controllers for the Verification of Communicating Multi-pushdown Systems

- Computer Science
- CONCUR
- 2014

The aim is to design controllers that observe/restrict the system so that it stays within the verified under-approximation, and to construct a distributed controller with the desired properties and establish the decidability of verification problems for this class. Expand