Yet Another Process Logic

We present a process logic that differs from the one introduced by Harel, Kozen and Parikh in several ways. First, we use the extended temporal logic of Wolper for statements about paths. Second, we allow a “repeat” operator in the programs. This allows us to specify programs with infinite computations. However, we limit the interaction between programs and path statements by adopting semantics similar to the ones used by Nishimura. Also, we require atomic programs to be interpreted as binary relations. We argue that this gives us a more appropriate logic. We have obtained an elementary decision procedure for our logic. The time complexity of the decision procedure is four exponentials in the general case and two exponentials if the logic is restricted to finite paths.