Bisimilar and logically equivalent programs in PDL with parallel operator

摘要

In standard Propositional Dynamic Logic (PDL) literature, the semantics is given by Labeled Transition Systems, where for each program pi we associate a binary relation R-pi. Process Algebras also give semantics to process (terms) by means of Labeled Transition Systems. In both formalisms, PDL and Process Algebra, the key notion to compare processes is bisimulation. In PDL, we also have the notion of logic equivalence, that can be used to prove that two programs pi(1) and pi(2) are logically equivalent proves i(1)>phi <-> i(2)>phi. Unfortunately, logic equivalence and bisimulation do not match in PDL. Bisimilar programs are logic equivalent but the converse does not hold. This paper proposes a semantics and an axiomatization for PDL that makes logically equivalent programs also bisimilar.