The Influence of the Test Operator on the Expressive Power of PDL-like Logics

摘要

Berman and Paterson proved that test-free propositional dynamic logic (PDL) is weaker than PDL. One would raise questions: does a similar result also hold for extensions of PDL? For example, is test-free converse-PDL (CPDL) weaker than CPDL? In what circumstances the test operator can be eliminated without reducing the expressive power of a PDL-based logical formalism? These problems have not yet been studied. As the description logics ALC(trans) and ALC(reg) are, respectively, variants of test-free PDL and PDL, there is a concept of ALC(reg) that is not equivalent to any concept of ALC(trans). Generalizing this, we prove that there is a concept of ALC(reg) that is not equivalent to any concept of the logic that extends ALC(trans) with inverse roles, nominals, qualified number restrictions, the universal role and local reflexivity of roles. We also provide some results for the case with RBoxes and TBoxes. One of them states that tests can be eliminated from TBoxes of the deterministic Horn fragment of ALC(reg).