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 extended temporal of Wolper for statements about paths. Second, allow “repeat” operator programs. This allows us to specify programs with infinite computations. However, limit interaction between path adopting semantics similar ones used Nishimura. Also, require atomic be interpreted as binary relations. argue this gives more appropriate logic. have obtained an elementary decision procedure our The time complexity is four exponentials general case two if restricted finite