{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,23]],"date-time":"2026-03-23T10:16:50Z","timestamp":1774261010886,"version":"3.50.1"},"reference-count":41,"publisher":"Cambridge University Press (CUP)","issue":"3","license":[{"start":{"date-parts":[[2015,6,2]],"date-time":"2015-06-02T00:00:00Z","timestamp":1433203200000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2017,3]]},"abstract":"<jats:p>Activities such as clinical investigations (CIs) 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, <jats:italic>i.e.<\/jats:italic> they may have different outcomes whenever applied. We present a formal semantics of our model based on focused proofs of linear logic with definitions. We also determine the computational complexity of various planning problems. Plan compliance problem, for example, is the problem of 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, <jats:italic>i.e.<\/jats:italic> 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. Finally, we show that the restrictions on the form of actions and time constraints taken in the specification of our model are necessary for decidability of the planning problems.<\/jats:p>","DOI":"10.1017\/s096012951500016x","type":"journal-article","created":{"date-parts":[[2015,6,2]],"date-time":"2015-06-02T06:07:44Z","timestamp":1433225264000},"page":"332-375","source":"Crossref","is-referenced-by-count":16,"title":["A rewriting framework and logic for activities subject to regulations"],"prefix":"10.1017","volume":"27","author":[{"given":"MAX","family":"KANOVICH","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"TAJANA","family":"BAN KIRIGIN","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"VIVEK","family":"NIGAM","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"ANDRE","family":"SCEDROV","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"CAROLYN","family":"TALCOTT","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"RANKO","family":"PEROVIC","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2015,6,2]]},"reference":[{"key":"S096012951500016X_ref1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"S096012951500016X_ref32","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-010-0121-8"},{"key":"S096012951500016X_ref31","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03748-1_8"},{"key":"S096012951500016X_ref12","first-page":"187","volume-title":"ICATPN'00","author":"de Frutos Escrig","year":"2000"},{"key":"S096012951500016X_ref5","unstructured":"Baelde D. (2008). A Linear Approach to the Proof-Theory of Least and Greatest Fixed Points. PhD thesis, Ecole Polytechnique."},{"key":"S096012951500016X_ref3","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/2.3.297"},{"key":"S096012951500016X_ref38","doi-asserted-by":"crossref","unstructured":"Nigam V. and Miller D. (2009). Algorithmic specifications in linear logic with subexponentials. 129\u2013140.","DOI":"10.1145\/1599410.1599427"},{"key":"S096012951500016X_ref22","unstructured":"Kanovich M. , Ban Kirigin T. , Nigam V. and Scedrov A. (2010). Bounded memory Dolev-Yao adversaries in collaborative systems. In: FAST. 18\u201333."},{"key":"S096012951500016X_ref27","unstructured":"Kanovich M. I. , Ban Kirigin T. , Nigam V. , Scedrov A. , Talcott C. L. and Perovic R. (2012). A rewriting framework for activities subject to regulations. In: Tiwari A. (ed.) RTA. LIPIcs.Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, volume 15, 305\u2013322."},{"key":"S096012951500016X_ref6","doi-asserted-by":"crossref","unstructured":"Baelde D. and Miller D. (2007). Least and greatest fixed points in linear logic. In: Dershowitz N. and Voronkov A. (eds.) International Conference on Logic for Programming and Automated Reasoning (LPAR), volume 4790, 92\u2013106.","DOI":"10.1007\/978-3-540-75560-9_9"},{"key":"S096012951500016X_ref10","volume-title":"All About Maude: A High-Performance Logical Framework","author":"Clavel","year":"2007"},{"key":"S096012951500016X_ref17","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-2004-12203"},{"key":"S096012951500016X_ref9","doi-asserted-by":"publisher","DOI":"10.1145\/322234.322243"},{"key":"S096012951500016X_ref33","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(99)00171-1"},{"key":"S096012951500016X_ref2","first-page":"1","article-title":"Decision problems for timed automata: A survey","author":"Alur","year":"2004","journal-title":"SFM"},{"key":"S096012951500016X_ref16","doi-asserted-by":"crossref","unstructured":"Dinesh N. , Joshi A. K. , Lee I. and Sokolsky O. (2011). Permission to speak: A logic for access control and conformance. Journal of Logic and Algebraic Programming 50\u201374.","DOI":"10.1016\/j.jlap.2009.12.002"},{"key":"S096012951500016X_ref25","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40203-6_18"},{"key":"S096012951500016X_ref13","doi-asserted-by":"crossref","unstructured":"DeYoung H. , Garg D. , Jia L. , Kaynar D. K. and Datta A. (2010). Experiences in the logical specification of the HIPAA and GLBA privacy laws. In: WPES 73\u201382.","DOI":"10.21236\/ADA571991"},{"key":"S096012951500016X_ref14","doi-asserted-by":"crossref","unstructured":"DeYoung H. , Garg D. and Pfenning F. (2008). An authorization logic with explicit time. In: CSF 133\u2013145.","DOI":"10.21236\/ADA476803"},{"key":"S096012951500016X_ref11","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-2007-15603"},{"key":"S096012951500016X_ref19","unstructured":"Garg D. , Jia L. and Datta A. (2011). Policy auditing over incomplete logs: Theory, implementation and applications. In: CCS'11. 151\u2013162."},{"key":"S096012951500016X_ref30","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129501003413"},{"key":"S096012951500016X_ref29","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-010-9190-1"},{"key":"S096012951500016X_ref15","doi-asserted-by":"crossref","unstructured":"Dinesh N. , Joshi A. K. , Lee I. and Sokolsky O. (2008). Reasoning about conditions and exceptions to laws in regulatory conformance checking. In: DEON 110\u2013124.","DOI":"10.1007\/978-3-540-70525-3_10"},{"key":"S096012951500016X_ref35","doi-asserted-by":"publisher","DOI":"10.2307\/1970290"},{"key":"S096012951500016X_ref41","doi-asserted-by":"crossref","unstructured":"Schroeder-Heister P. (1993). Rules of definitional reflection. In: Vardi M. (ed.) 8th Annual Symposium on Logic in Computer Science, IEEE Computer Society Press, IEEE 222\u2013232.","DOI":"10.1109\/LICS.1993.287585"},{"key":"S096012951500016X_ref24","volume-title":"CSF'09: Proceedings of the 2009 22nd IEEE Computer Security Foundations Symposium","author":"Kanovich","year":"2009"},{"key":"S096012951500016X_ref21","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1036"},{"key":"S096012951500016X_ref8","doi-asserted-by":"crossref","unstructured":"Barth A. , Mitchell J. C. , Datta A. and Sundaram S. (2007). Privacy and utility in business processes. In: CSF 279\u2013294.","DOI":"10.1109\/CSF.2007.26"},{"key":"S096012951500016X_ref40","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2007.06.005"},{"key":"S096012951500016X_ref20","doi-asserted-by":"publisher","DOI":"10.1145\/800213.806517"},{"key":"S096012951500016X_ref7","unstructured":"Barth A. , Datta A. , Mitchell J. C. and Nissenbaum H. (2006). Privacy and contextual integrity: Framework and applications. In: IEEE Symposium on Security and Privacy 184\u2013198."},{"key":"S096012951500016X_ref37","doi-asserted-by":"crossref","unstructured":"Nigam V. , Ban Kirigin T. , Scedrov A. , Talcott C. , Kanovich M. and Perovic R. (2012). Towards an automated assistant for clinical investigations. In: Second ACM SIGHIT International Health Informatics Symposium. 773\u2013778.","DOI":"10.1145\/2110363.2110456"},{"key":"S096012951500016X_ref4","doi-asserted-by":"crossref","unstructured":"Arney D. , Pajic M. , Goldman J. M. , Lee I. , Mangharam R . and Sokolsky O. (2010). Toward patient safety in closed-loop medical device systems. In (ICCPS '10), New York, NY, USA, ACM 139\u2013148.","DOI":"10.1145\/1795194.1795214"},{"key":"S096012951500016X_ref28","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)80591-2"},{"key":"S096012951500016X_ref34","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90182-F"},{"key":"S096012951500016X_ref18","unstructured":"FDA (2014). Code of Federal Regulations, Title 21, Chapter 1, Subchapter D, Part 312: Investigational New Drug Application. Available at http:\/\/www.accessdata.fda.gov\/scripts\/cdrh\/cfdocs\/cfCFR\/CFRSearch.cfm?CFRPart=312&showFR=1."},{"key":"S096012951500016X_ref36","doi-asserted-by":"crossref","unstructured":"Nigam V. (2012). On the complexity of linear authorization logics. In: LICS IEEE 511\u2013520.","DOI":"10.1109\/LICS.2012.61"},{"key":"S096012951500016X_ref23","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2014.07.011"},{"key":"S096012951500016X_ref26","doi-asserted-by":"publisher","DOI":"10.1016\/j.cl.2014.05.003"},{"key":"S096012951500016X_ref39","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-010-9182-1"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S096012951500016X","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,18]],"date-time":"2019-04-18T02:08:17Z","timestamp":1555553297000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S096012951500016X\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,6,2]]},"references-count":41,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2017,3]]}},"alternative-id":["S096012951500016X"],"URL":"https:\/\/doi.org\/10.1017\/s096012951500016x","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,6,2]]}}}