Using Formal Verification and Robotic Evolution Techniques to Find Contradictions in Laws Concerning Police Rules of Engagement

There are thousands of laws and regulations in the United States, ranging from the local to the state to the federal level. The sheer number of laws increases the probability that some of these laws may contradict each other. In recent years in the City of Portland, many controversial instances of police officers using force have occurred. In this project we used formal verification and robot programming techniques to validate and find contradictions in laws that govern police use of force. We constructed a model of police officers and bystanders in a robot "game" using the NuSMV software and development language. Temporal logic, which uses a subset of modal logic, along with predicate calculus is used to produce a computational logic tree, which simulates all possibilities in the model. Robot movement is used to model state evolution. We inserted statutes and case law into our model to dictate the behaviors of the actors, in the process developing a formal method of translating laws into operational predicate modal logic clauses. Finally, we run a process to check through the computation tree to find contradictions. Our final results found several contradictions, some of them obvious enough to be used as argument in real court cases, and suggest the legal code should be seriously cleaned up so as to prevent confusion and uncertainty. Our work also suggests that formal verification techniques can be applied to drug laws, tax laws, and other legal venues.