Dinesh, N., Joshi, J.K., Lee, I., and Sokolosky O. (2008). Checking traces for
Regulatory Conformance. Presented at RV'08 - Eighth Workshop on Runtime
Verification, a satellite workshop of ETAPS'08. March 2008. 


Abstract: We consider the problem of checking whether the operations of an 
organization conform to a body of regulation. The immediate motivation comes 
from the analysis of the U.S. Food and Drug Administration regulations that 
apply to bloodbanks - organizations that collect, process, store, and use 
donations of blood and blood components. Statements in such regulations convey
constraints on operations or sequences of operations that are performed by an 
organization. It is natural to express these constraints in a temporal logic.

There are two important features of regulatory texts that need to be 
accommodated by a representation in logic. First, the constraints conveyed by 
regulation can be obligatory (required) or permitted (optional). Second, 
statements in regulation refer to others for conditions or exceptions. An 
organization conforms to a body of regulation if and only if it satisfies 
all the obligations. However, permissions provide exceptions to obligations, 
indirectly affecting conformance.

In this paper, we extend linear temporal logic to distinguish between 
obligations and permissions, and to allow statements to refer to others. While
the resulting logic allows for a direct representation of regulation, 
evaluating references between statements has high complexity. We discuss an 
empirically motivated assumption that lets us replace references with tests of
lower complexity, leading to efficient trace-checking algorithms in practice.