发表机构
School of Mathematics and Statistic; Xi’an Jiaotong University（数学与统计学院; 西安交通大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文为带标签实时自动机定义韧性（故障后恢复且不泄露），并基于并发组合与观察器给出验证算法，用于建模智能体。
AI 中文摘要
本文刻画了带标签实时自动机（LRTA）的韧性。若每当发生故障事件后，在足够多的事件发生之后，LRTA能恢复正常且故障事件的发生未被泄露，则该LRTA是韧性的。韧性概念反映了LRTA从故障行为中恢复的能力，因此可对智能体进行建模。我们为LRTA提出了一种韧性的定义，并基于两个基本工具——并发组合与观察器——给出了针对该定义的验证算法。
英文摘要
In this paper, we characterize resilience for a labeled real-time automaton (LRTA). An LRTA is resilient if whenever a faulty event occurs, after sufficiently many events occur, the LRTA returns to normalcy and the occurrence of the faulty event is not leaked. The notion of resilience reflects the ability of an LRTA recovering from a faulty behavior, and hence can model an intelligent agent. We formulate one definition of resilience for an LRTA and give verification algorithms for the definition based on two basic tools --- concurrent composition and observer.
Comments21 pages, 12 figures
