Skip to Main content Skip to Navigation

The Regular Viewpoint on PA-Processes

Denis Lugiez 1 Philippe Schnoebelen
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : PA is the process algebra allowing non-determinism, sequential and parallel compositions, and recursion. We suggest a view of PA-processes as {\em tree languages}. Our main result is that the set of iterated predecessors of a regular set of PA-processes 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.
Document type :
Complete list of metadata
Contributor : Rapport de Recherche Inria <>
Submitted on : Wednesday, May 24, 2006 - 12:26:23 PM
Last modification on : Friday, February 26, 2021 - 3:28:06 PM
Long-term archiving on: : Sunday, April 4, 2010 - 8:57:51 PM


  • HAL Id : inria-00073287, version 1



Denis Lugiez, Philippe Schnoebelen. The Regular Viewpoint on PA-Processes. [Research Report] RR-3403, INRIA. 1998, pp.27. ⟨inria-00073287⟩



Record views


Files downloads