一种用于基于历史的事务监控的可判定策略语言
计算机科学中的逻辑
2015-05-13 v1 密码学与安全
摘要
在线交易不可避免地涉及陌生人之间的交易，因此一方能够客观地评判另一方的可信度非常重要。在这种场景下，信任用户的决定可以合理地基于该用户过去的行为。我们引入了一种基于线性时序逻辑的规范语言，用于表达根据事务历史对用户行为模式进行分类的策略。我们还提出了一种算法，用于检查事务历史是否遵守规定的策略。为了在实际场景中有用，这种语言应允许表达可能涉及参数量化以及定量或统计模式的现实策略。我们引入了线性时序逻辑的几种扩展以满足这些需求：一种受限形式的全称和存在量化；项语言中的任意可计算函数和关系；以及用于计算公式在过去成立次数的“计数”量词。然后我们证明，针对策略对事务历史进行模型检查（我们称之为基于历史的事务监控问题）在策略公式规模和历史长度上是 PSPACE 完全的。当策略固定时，该问题在多项式时间内变得可判定。我们还考虑了在动作参数并非完全可观测情况下的监控问题。我们形式化了两种此类“部分可观测”监控问题，并证明了它们在某些限制下是可判定的。
引用
@article{arxiv.0903.2904,
title = {A decidable policy language for history-based transaction monitoring},
author = {Andreas Bauer and Rajeev Gore and Alwen Tiu},
journal= {arXiv preprint arXiv:0903.2904},
year = {2015}
}