文中从超线性时序逻辑(hyper linear temporal logic,HyperLTL)的角度深入探讨了加权离散事件系统(discrete event systems,DESs)的可检测性问题.先前关于DESs的研究通常假设事件转换是瞬时的或无需成本的.然而,在实际生产环境中,事件转换往往涉及时间和成本的消耗,这需要在DESs研究中引入加权因素.加权决策策略旨在通过为不同事件或状态分配权重来优化系统性能、指导政策制定,并实现高效、安全和可靠地运行.讨论了从加权DESs建模中得出的无二义加权自动机(unambiguous weighted automata,UWAs).在此基础上,将其转换为一种特殊的Kripke结构,以捕获此类加权自动机的信息,从而实现HyperLTL的明确表示.
A hyper linear temporal logic approach to detectability of unambiguous weighted automata
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.
cyber securitydiscrete event systemsdetectabilityhyper linear temporal logicunambiguous weighted automata
NETL
NSTL
万方数据
