Tableau Methods for PA-Processes

Abstract. PA (Process algebra) is the name that has become common use to denote the algebra with a sequential and parallel operator (without communication), plus recursion. PA-processes are a superset of both Basic Parallel Processes (BPP) Chr93] and context-free processes (BPA). We study three problems for PA-processes: The reachability problem, the partial deadlock reachability problem (\Is it possible to reach a state where certain actions are not enabled ?") and the partial livelock reachability problem (\Is it possible to reach a state where certain actions are disabled forever ?"). We present sound and complete tableau systems for these problems and compare them to non-tableau algorithms.

• Type: Conference
• Year: 1997
• Where: TABLEAUX
• Authors: Richard Mayr
• Keywords: Artificial Intelligence, Certain Actions, Deadlock Reachability Problem, Reachability Problem, TABLEAUX 1997