A rewriting framework and logic for activities subject to regulations
A rewriting framework and logic for activities subject to regulations
复制标题
重写受监管活动的框架和逻辑
DOI：
--
复制
发表时间：
2015
影响因子：
0.5
通讯作者：
Ranko Perovic
中科院分区：
文献类型：
--
作者：
M. Kanovich;Tajana Ban Kirigin;Vivek Nigam;A. Scedrov;C. Talcott;Ranko Perovic
临床研究（CI）或财务流程等活动须遵守法规，以确保结果质量并避免负面后果。多个政府机构以及机构政策和议定书可能会实施条例。由于法规和活动的复杂性，由于人为错误，误解甚至意图而违反的可能性很大。法规、协议和活动的可执行正式模型可以为自动化助理提供基础，以帮助规划、监控和合规性检查。我们提出了一个模型的基础上多集重写的时间是离散的，并指定的时间戳附加到事实。行动，以及初始，目标和关键状态可以通过相对时间约束来约束。此外，行动可能具有不确定性的影响，即无论何时采取行动，都可能产生不同的结果。我们提出了一个正式的语义模型的基础上集中证明线性逻辑的定义。我们还确定各种规划问题的计算复杂性。例如，计划遵从性问题是找到一个从初始状态到期望目标状态而不到达任何不期望的临界状态的计划的问题。我们认为所有行动都是平衡的，即它们的前置条件和后置条件具有相同数量的事实。在这种假设下的行动，我们表明，计划遵守问题是PSPACE完全的所有行动时，只有确定性的影响，是EXPTIME完全的行动时，可能有非确定性的影响。最后，我们表明，在我们的模型的规格采取的行动和时间约束的形式的限制是必要的决策规划问题。
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, i.e. 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, i.e. 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.