判定轨迹等价性的简化语义
摘要：保护协议的许多隐私类型属性可以使用适合的过程代数中的迹等价性属性进行建模。已经证明，通过使用符号执行和约束求解可以决定有趣的有限进程类的这种属性（即，无复制）。然而，这还不足以获得实用的工具。当前的原型在处理过程行为中的许多交錯探索时遇到经典的组合爆炸问题。M"odersheim等人使用部分有序规约技术解决了可达性属性的这个问题。我们重新审视他们的工作，对其进行了泛化和调整，以适应等价性检查。我们通过减少冗余交錯的符号语义来优化，从而获得了一种优化形式。所获得的部分有序规约技术已集成在名为APTE的工具中。我们进行了完整的基准测试，显示出巨大的改进。
作者：David Baelde and St''ephanie Delaune and Lucca Hirschi
论文ID：1704.08540
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22