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.
This research was supported in part by NSF CCF-0429948, NSF-CNS-0610297, ARO W911NF-05-1-0158, and ONR MURI N00014-04-1-0735.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Abrahams, A.: Developing and Executing Electronic Commerce Applications with Occurrences. PhD thesis, Univeristy of Cambridge (2002)
Breaux, T.D., Vail, M.W., Anton, A.I.: Towards regulatory compliance: Extracting rights and obligations to align requirements with regulations. In: Proceedings of the 14th IEEE International Requirements Engineering Conference (2006)
Giblin, C., Liu, A., Muller, S., Pfitzmann, B., Zhou, X.: Regulations Expressed as Logical Models (REALM). In: Moens, M.-F., Spyns, P. (eds.) Legal Knowledge and Information Systems (2005)
U.S. Food and Drug Administration: Code of Federal Regulations, http://www.gpoaccess.gov/cfr/index.html
Barringer, H., Goldberg, A., Havelund, K., Sen, K.: Rule-based runtime verification. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 44–57. Springer, Heidelberg (2004)
McCarty, L.T.: A language for legal discourse - i. basic features. In: Proceedings of ICAIL (1989)
Sergot, M., Sadri, F., Kowalski, R., Kriwaczek, F., Hammond, P., Cory, H.: The british nationality act as a logic program. Communications of the ACM 29(5), 370–386 (1986)
Ross, A.: Directives and Norms. Routlege and Kegan Paul (1968)
Marcus, R.B.: Iterated deontic modalities. Mind 75(300) (1966)
Dinesh, N., Joshi, A., Lee, I., Sokolsky, O.: Reasoning about conditions and exceptions to laws in regulatory conformance checking (in submission, 2008), http://www.cis.upenn.edu/Â nikhild/reasoning.pdf (2008)
Reiter, R.: A logic for default reasoning. In: Readings in nonmonotonic reasoning, pp. 68–93. Morgan Kaufmann Publishers Inc., San Francisco (1987)
Sistla, A.P., Clarke, E.M.: The complexity of propositional linear temporal logic. ACM 32, 733–749 (1985)
Bauer, A., Leucker, M., Schallhart, C.: Monitoring of real-time properties. In: Arun-Kumar, S., Garg, N. (eds.) FSTTCS 2006. LNCS, vol. 4337. Springer, Heidelberg (2006)
Dinesh, N., Joshi, A.K., Lee, I., Webber, B.: Extracting formal specifications from natural language regulatory documents. In: Proceedings of the Fifth International Workshop on Inference in Computational Semantics (2006)
Dinesh, N., Joshi, A., Lee, I., Sokolsky, O.: Logic-based regulatory conformance checking. In: Proceedings of the 14th Monterey Workshop (2007)
von Wright, G.H.: Deontic logic. Mind 60, 1–15 (1951)
Aqvist, L.: Deontic logic. In: Gabbay, D., Guenthner, F. (eds.) Handbook of Philosophical Logic, Extensions of Classical Logic, vol. II, pp. 605–614 (1984)
Bench-Capon, T.J., Robinson, G., Routen, T., Sergot, M.: Logic programming for large scale applications in law: A formalisation of supplementary benefit legislation. In: Proceedings of the 1st International Conference on AI and Law (1987)
Alchourron, C., Makinson, D.: Hierarchies of regulation and their logic. In: Hilpinen, R. (ed.) New Studies in Deontic Logic (1981)
Makinson, D., van der Torre, L.: Input/output logics. Journal of Philosophical Logic 29, 383–408 (2000)
Glasse, E., Engers, T.V., Jacobs, A.: Power: An integrated method for legislation and regulations from their design to their use in e-government services and law enforcement. In: Moens, M.-F. (ed.) Digitale Wetgeving, Digital Legislation, pp. 175–204 (2003)
Barringer, H., Rydeheard, D., Havelund, K.: Rule systems for run-time monitoring: From Eagle to RuleR. In: Sokolsky, O., Taşıran, S. (eds.) RV 2007. LNCS, vol. 4839, pp. 111–125. Springer, Heidelberg (2007)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dinesh, N., Joshi, A., Lee, I., Sokolsky, O. (2008). Checking Traces for Regulatory Conformance. In: Leucker, M. (eds) Runtime Verification. RV 2008. Lecture Notes in Computer Science, vol 5289. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-89247-2_6
Download citation
DOI: https://doi.org/10.1007/978-3-540-89247-2_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-89246-5
Online ISBN: 978-3-540-89247-2
eBook Packages: Computer ScienceComputer Science (R0)