SEQUENCE-INDEXED LINEAR-TIME TEMPORAL LOGIC: PROOF SYSTEM AND APPLICATION
SEQUENCE-INDEXED LINEAR-TIME TEMPORAL LOGIC: PROOF SYSTEM AND APPLICATION
复制标题
序列索引线性时间时态逻辑：证明系统和应用
DOI：
10.1080/08839514.2010.514231
复制
发表时间：
2010
影响因子：
2.8
通讯作者：
N. Kamide
中科院分区：
文献类型：
--
作者：
K. Kaneiwa;N. Kamide
我们提出了一个证明系统，用于对安全认证系统的某些规范进行推理。为此，一个新的逻辑，序列索引的线性时间时序逻辑（SLTL），是从标准的线性时间时序逻辑（LTL）的语义通过添加一个序列模态算子，表示一个序列的符号。通过这个序列模态算子，我们可以恰当地表达时态推理中客户机和服务器之间的消息流以及服务器的状态。引入了一种求解SLTL的Gentzen型微积分，并证明了它的完备性定理和割消定理。SLTL也被证明是PSPACE完全的，并嵌入到LTL。
We propose a proof system for reasoning on certain specifications of secure authentication systems. For this purpose, a new logic, sequence-indexed linear-time temporal logic (SLTL), is obtained semantically from standard linear-time temporal logic (LTL) by adding a sequence modal operator that represents a sequence of symbols. By this sequence modal operator, we can appropriately express message flows between clients and servers and states of servers in temporal reasoning. A Gentzen-type sequent calculus for SLTL is introduced, and the completeness and cut-elimination theorems for it are proved. SLTL is also shown to be PSPACE-complete and embeddable into LTL.
具有谓词层次结构的顺序排序逻辑编程
DOI：
--
发表时间：
2004
期刊：
Artificial Intelligence 158・2
影响因子：
--
作者：
Ken Kaneiwa
通讯作者：
Ken Kaneiwa