Your Search Results

Use this resource - and many more! - in your textbook!

AcademicPub holds over eight million pieces of educational content for you to mix-and-match your way.

Experience the freedom of customizing your course pack with AcademicPub!
Not an educator but still interested in using this content? No problem! Visit our provider's page to contact the publisher and get permission directly.

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

By: Perkowski, M.; Sun, L.; Sun, T.;

2012 / IEEE / 978-1-4673-0908-0

Description

This item was taken from the IEEE Conference ' 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.