Symbolic reachability analysis of FIFO-channel systems with nonregular sets of configurations

We address the verification problem of FIFO-channel systems. We apply the s ymbolic analysis principle to these systems. We represent their sets of con figurations using structures called constrained queue-content decision diag rams (CQDDs) combining finite-state automata with linear arithmetical const raints on number of occurrences of symbols. We show that CQDDs allow forwar d and backward reachability analysis of systems with nonregular sets of con figurations. Moreover, we prove that CQDDs allow to compute the exact effec t of the repeated execution of any fixed cycle in the transition graph of a system. We use this fact to define a generic reachability analysis semi-al gorithm parametrized by a set of cycles Theta. Given a set of configuration s, this semi-algorithm performs a least fixpoint calculation to construct t he set of its successors (or predecessors). At each step, this calculation is accelerated by considering the cycles in Theta as additional "meta-trans itions" in the transition graph, generalizing the approach of Boigelot and Godefroid (CAV'96, Lecture Notes in Computer Science, Vol. 1102, Springer, Berlin, 1996). (C) 1999 Published by Elsevier Science B.V. All rights reser ved.