The Regular Viewpoint on PA-Processes

PA is the process algebra allowing non-determinism, sequential and parallel compositions, and recursion. We suggest viewing PA-processes as trees, and using treeautomata techniques for verification problems on PA. Our main result is that the set of iterated predecessors of a regular set of PAprocesses is a regular tree language, and similarly for iterated successors. Furthermore, the corresponding tree-automata can be built effectively in polynomial-time. This has many immediate applications to verification problems for PA-processes, among which a simple and general model-checking algorithm. Key words: Process algebra, verification of infinite-state systems, tree-automata.

• Type: Conference
• Year: 1998
• Where: CONCUR
• Authors: Denis Lugiez, Ph. Schnoebelen
• Keywords: CONCUR 1998, Distributed And Parallel Computing, Process Algebra, Regular Tree Language, Verification Problems