Reachability Problems in Piecewise FIFO Systems
| Autor: | Naghmeh Ghafari, Arie Gurfinkel, Nils Klarlund, Richard J. Trefler |
|---|---|
| Rok vydání: | 2012 |
| Předmět: | |
| Zdroj: | ACM Transactions on Computational Logic. 13:1-33 |
| ISSN: | 1557-945X 1529-3785 |
| DOI: | 10.1145/2071368.2071375 |
| Popis: | Systems consisting of several finite components that communicate via unbounded perfect FIFO channels (i.e., FIFO systems) arise naturally in modeling distributed systems. Despite well-known difficulties in analyzing such systems, they are of significant interest as they can describe a wide range of communication protocols. In this article, we study the problem of computing the set of reachable states of a FIFO system composed of piecewise components. This problem is closely related to calculating the set of all possible channel contents, that is, the limit language , for each control location. We present an algorithm for calculating the limit language of a system with a single communication channel. For multichannel systems, we show that the limit language is piecewise if the initial language is piecewise. Our construction is not effective in general; however, we provide algorithms for calculating the limit language of a restricted class of multichannel systems in which messages are not passed around in cycles through different channels. We show that the worst case complexity of our algorithms for single-channel and important subclasses of multichannel systems is exponential in the size of the initial content of the channels. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|