Asynchronously Communicating Visibly Pushdown Systems
[PDF]
[PS] [PS.BZ2] [VIEW]
Bibtex:
@inproceedings{br13async,
author = {Domagoj Babi\'c and Zvonimir Rakamari\'c},
title = {{Asynchronously Communicating Visibly Pushdown Systems}}},
booktitle = {FORTE'13: 2013 IFIP Joint International Conference on
Formal Techniques for Distributed Systems},
year = {2013},
publisher = {Springer},
series = {LNCS},
volume = {7892},
pages = {225 -- 242},
location = {Florence, Italy}
}
Abstract:
We introduce an automata-based formal model suitable for specifying,
modeling, analyzing, and verifying asynchronous task-based and
message-passing programs. Our model consists of visibly pushdown
automata communicating over unbounded reliable point-to-point
first-in-first-out queues. Such a combination unifies two branches of
research, one focused on task-based models, and the other on models of
message-passing programs. Our model generalizes previously proposed
models that have decidable reachability in several ways. Unlike
task-based models of asynchronous programs, our model allows sending and
receiving of messages even when stacks are not empty, without imposing
restrictions on the number of context-switches or communication
topology. Our model also generalizes the well-known communicating
finite-state machines with recognizable channel property allowing (1)
individual components to be visibly pushdown automata, which are more
suitable for modeling (possibly recursive) programs, (2) the set of
words (i.e., languages) of messages on queues to form a visibly pushdown
language, which permits modeling of remote procedure calls and simple
forms of counting, and (3) the relations formed by tuples of such
languages to be synchronized, which permits modeling of complex
interactions among processes. In spite of these generalizations, we
prove that the composite configuration and control-state reachability
are still decidable for our model.