Name
Abstract | ||
|---|---|---|
The reachability analysis of recursive programs that communicate asynchronously over reliable Fifo channels calls for restrictions
to ensure decidability. We extend here a model proposed by La Torre, Madhusudan and Parlato [16], based on communicating pushdown
systems that can dequeue with empty stack only. Our extension adds the dual modality, which allows to dequeue with non-empty
stack, and thus models interrupts for working threads. We study (possibly cyclic) network architectures under a semantic assumption
on communication that ensures the decidability of reachability for finite state systems. Subsequently, we determine precisely
how pushdowns can be added to this setting while preserving the decidability; in the positive case we obtain exponential time
as the exact complexity bound of reachability. A second result is a generalization of the doubly exponential time algorithm
of [16] for bounded context analysis to our symmetric queueing policy. We provide here a direct and simpler algorithm.
|
Year | DOI | Venue |
|---|---|---|
2012 | 10.1007/978-3-642-12032-9_19 | Logical Methods in Computer Science |
Keywords | Field | DocType |
reachability analysis,pushdown system,simpler algorithm,exact complexity,exponential time,dual modality,exponential time algorithm,bounded context analysis,finite state system,la torre,models interrupts,network architecture | Discrete mathematics,Computer science,Decidability,Thread (computing),Reachability,Queueing theory,Reachability problem,Double-ended queue,Recursion,Bounded function | Journal |
Volume | Issue | ISSN |
8 | 3 | Logical Methods in Computer Science, Volume 8, Issue 3 (September
27, 2012) lmcs:921 |
ISBN | Citations | PageRank |
3-642-12031-8 | 26 | 0.88 |
References | Authors | |
20 | 4 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Alexander Heußner | 1 | 35 | 3.13 |
| Jérôme Leroux | 2 | 494 | 30.97 |
| Anca Muscholl | 3 | 1179 | 74.92 |
| Grégoire Sutre | 4 | 492 | 35.06 |