License: Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license (CC BY-NC-ND 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.RTA.2012.305
URN: urn:nbn:de:0030-drops-35000
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2012/3500/
Go to the corresponding LIPIcs Volume Portal

Kanovich, Max ; Ban Kirigin, Tajana ; Nigam, Vivek ; Scedrov, Andre ; Talcott, Carolyn ; Perovic, Ranko

A Rewriting Framework for Activities Subject to Regulations

pdf-format:
23.pdf (0.5 MB)

Abstract

Activities such as clinical investigations or financial processes are
subject to regulations to ensure quality of results and avoid negative consequences. Regulations may be imposed by multiple governmental agencies as well as by institutional policies and protocols. Due to the complexity of both regulations and activities there is great potential for violation due to human error,
misunderstanding, or even intent. Executable formal models of regulations, protocols, and activities can form the foundation for automated assistants to aid planning, monitoring, and compliance checking. We propose a model based on multiset rewriting where time is discrete and is specified by timestamps attached to facts. Actions, as well as initial, goal and critical states may be constrained by means of relative time constraints. Moreover, actions may have non-deterministic effects, that is, they may have different outcomes whenever applied. We demonstrate how specifications in our model can be straightforwardly mapped to the rewriting logic language Maude, and how one can use existing techniques to improve performance.
Finally, we also determine the complexity of the plan compliance problem, that is, finding a plan that leads from an initial state to a desired goal state without reaching any undesired critical state. We consider all actions to be balanced, that is, their pre and post-conditions have the same number of facts. Under this assumption on actions, we show that the plan compliance problem is PSPACE-complete when all actions have only deterministic effects and is
EXPTIME-complete when actions may have non-deterministic effects.

BibTeX - Entry

@InProceedings{kanovich_et_al:LIPIcs:2012:3500,
  author =	{Max Kanovich and Tajana Ban Kirigin and Vivek Nigam and Andre Scedrov and Carolyn Talcott and Ranko Perovic},
  title =	{{A Rewriting Framework for Activities Subject to Regulations}},
  booktitle =	{23rd International Conference on Rewriting Techniques and Applications (RTA'12) },
  pages =	{305--322},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-38-5},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{15},
  editor =	{Ashish Tiwari},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2012/3500},
  URN =		{urn:nbn:de:0030-drops-35000},
  doi =		{10.4230/LIPIcs.RTA.2012.305},
  annote =	{Keywords: Multiset Rewrite Systems, Collaborative Systems, Applications of Rewrite Systems, Clinical Investigations, Maude}
}

Keywords: Multiset Rewrite Systems, Collaborative Systems, Applications of Rewrite Systems, Clinical Investigations, Maude
Collection: 23rd International Conference on Rewriting Techniques and Applications (RTA'12)
Issue Date: 2012
Date of publication: 29.05.2012

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI