you need to describe the interaction protocol as a state machine, recording the states of policy proposals and describing the possible actions of partners.
Requirements 1 and 2 will be reflected in the protocol: introduce a counter for how many times a proposal has been modified and disallow a "modification" action concerning an adopted proposal.
Requirements 3 and 5 are quantitative. Again, you'll need to introduce appropriate counters. Assuming that nothing is required to happen on any given day, you will not be able to guarantee that any policy has been adopted after 20 days, and assuming that a policy can be adopted immediately after it has been proposed, there is no obvious upper bound on the number of policies (or lower bound on the number of days required) either. By specifying fairness properties and/or minimum delays you may be able to get meaningful results for these questions.