ausblenden:
Schlagwörter:
Computer Science, Logic in Computer Science, cs.LO,Computer Science, Distributed, Parallel, and Cluster Computing, cs.DC,Computer Science, Formal Languages and Automata Theory, cs.FL
Zusammenfassung:
We consider the problem of automatically verifying that a parameterized
family of probabilistic concurrent systems terminates with probability one for
all instances against adversarial schedulers. A parameterized family defines an
infinite-state system: for each number n, the family consists of an instance
with n finite-state processes. In contrast to safety, the parameterized
verification of liveness is currently still considered extremely challenging
especially in the presence of probabilities in the model. One major challenge
is to provide a sufficiently powerful symbolic framework. One well-known
symbolic framework for the parameterized verification of non-probabilistic
concurrent systems is regular model checking. Although the framework was
recently extended to probabilistic systems, incorporating fairness in the
framework - often crucial for verifying termination - has been especially
difficult due to the presence of an infinite number of fairness constraints
(one for each process). Our main contribution is a systematic,
regularity-preserving, encoding of finitary fairness (a realistic notion of
fairness proposed by Alur & Henzinger) in the framework of regular model
checking for probabilistic parameterized systems. Our encoding reduces
termination with finitary fairness to verifying parameterized termination
without fairness over probabilistic systems in regular model checking (for
which a verification framework already exists). We show that our algorithm
could verify termination for many interesting examples from distributed
algorithms (Herman's protocol) and evolutionary biology (Moran process, cell
cycle switch), which do not hold under the standard notion of fairness. To the
best of our knowledge, our algorithm is the first fully-automatic method that
can prove termination for these examples.
