基于超线性时序逻辑的无二义加权自动机的可检测性研究  

A hyper linear temporal logic approach to detectability of unambiguous weighted automata

作　　者：张涛[1] 彭皓天 ZHANG Tao;PENG Haotian(Office of Cybersecurity and Informatization,Tianjin University of Technology,Tianjin 300384,China;School of Control Science and Engineering,Tiangong University,Tianjin 300387,China)

机构地区：[1]天津理工大学网络安全和信息化办公室,天津300384 [2]天津工业大学控制科学与工程学院,天津300387

出　　处：《天津理工大学学报》2025年第1期112-117,共6页Journal of Tianjin University of Technology

基　　金：天津市自然科学基金项目(22JCZDJC00550)。

摘　　要：文中从超线性时序逻辑(hyper linear temporal logic, HyperLTL)的角度深入探讨了加权离散事件系统(discrete event systems, DESs)的可检测性问题。先前关于DESs的研究通常假设事件转换是瞬时的或无需成本的。然而,在实际生产环境中,事件转换往往涉及时间和成本的消耗,这需要在DESs研究中引入加权因素。加权决策策略旨在通过为不同事件或状态分配权重来优化系统性能、指导政策制定,并实现高效、安全和可靠地运行。讨论了从加权DESs建模中得出的无二义加权自动机(unambiguous weighted automata, UWAs)。在此基础上,将其转换为一种特殊的Kripke结构,以捕获此类加权自动机的信息,从而实现HyperLTL的明确表示。In this paper,we delve into the problem of detectability in weighted discrete event systems from the perspective of hyper linear temporal logic(HyperLTL).Prior research on discrete event systems(DESs)typically assumes instantaneous or cost-free event transitions.However,in practical production environments,event transitions often involve time and cost consumption,necessitating the introduction of weighted factors in DESs research.Weighted decision-making strategies aim to optimize system performance,guide policy formulation,and achieve efficient,safe,and reliable operation by assigning weights to different events or states.Here,we discuss unambiguous weighted automata(UWAs)derived from the modeling of weighted DESs.Based on this,we transform them into a special type of Kripke structure to capture information on such weighted automata,enabling explicit representation of HyperLTL.

关 键 词：网络安全 离散事件系统 可检测性 超线性时序逻辑 无二义加权自动机 

分 类 号：TP393[自动化与计算机技术—计算机应用技术]