|
Abstract : |
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. Keywords: tableau systems, temporal logic, process algebras, PA-processes 1, |
