The undecidability of the satisfiability in a process logic for a true concurrent process algebra

摘要

In this paper, we show that the satisfiability of specifications described in a process logic for a true concurrent process algebra is undecidable, even if the specifications have finite states, no disjunction V, and no communication requirement. The notion of true concurrency explicitly distinguishes concurrent behavior from interleaving behavior, and many process algebras extended with true concurrency have been proposed. The result presented in this paper can be extended for most of the true concurrent process algebras, because we use a very simple true concurrent process algebra and a process logic.