Reasoning about Dynamic Policies

People often need to reason about policy changes before they are adopted. For example, suppose a website manager knows that users want to enter her site without going through the welcome page. To decide whether or not to permit this, the wise manager will consider the consequences of modifying the policies (e.g., would this allow users to bypass advertisements and legal notices?). Similiarly, people often need to compare policy sets. For example, consider a person who wants to buy health insurance. Before choosing a provider, the customer will want to compare the different policies. In other words, the customer wants to reason about the effect of choosing one policy set over another. We introduce a logic, based on propositional dynamic logic, in which these tasks can be done. We give a sound and complete axiomatization for our logic, and also show that it is decidable. More precisely, the satisfiability problem is decidable in nondeterministic exponential time.