Reachability for finite-state process algebras using Horn clauses (Q2842001)

An algorithm for solving the reachability problem in finite systems that are modeled with process algebras (variants of CSP with some syntactical restrictions to ensure a finite number of states) is presented. The method is based on static data flow analysis; actions are equipped with labels which serve only as pointers into the syntax that make it easier to express the properties that are proved for process algebras. With the help of labels generate, kill and exposed operators are defined. The algorithm exploits a set of Horn clauses whose least model corresponds to an overapproximation of the reachable states. The computed model can be refined after each transition, and the algorithm runs until either a state whose reachability should be checked is encountered or it is not in the least model for all constructed states and thus is definitely unreachable. Only a part of the labeled transition system is built what leads to a lower time and memory consumption.