Source-linked AI summary
Resilience in labeled real-time automata
Kuize Zhang
TL;DR
The paper asks how to define and verify resilience in labeled real-time automata, where a faulty event is followed by recovery to normalcy without leaking its occurrence. It gives a verification method based on concurrent composition and observer, and shows that non-resilience is verifiable in N2EXPTIME.
Problem
The paper addresses how to define and verify LRTA resilience, where after a faulty event the system returns to normalcy without leaking that event.
Source: §1.3 · p. 4Method
The authors use concurrent composition and observer to give a necessary and sufficient condition for the negation of resilience.
Source: §1.3 · p. 4Results
The negation of resilience of an LRTA can be verified in N2EXPTIME.
Source: §3.3 · p. 16Takeaways & Limitations
Applications to practical scenarios, including describing intelligent-agent behavior, are identified as future topics.
Source: §4 · p. 18The procedure cannot compute all relevant pairs because infinitely many exist, so it checks state and state-set combinations instead.
Source: §3.3 · p. 13
Abstract
from arXiv · showhide
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.
1 Introduction
The introduction situates resilience as recovery after faults without leaking their occurrence, then motivates a labeled real-time automaton (LRTA) definition and verification using concurrent composition and observers. It also places this work among prior resilience definitions and extensions of verification tools to LRTAs.
1.1 Background
- Prior work formalized resilience for labeled finite-state automata and timed automata, with differing definitions and decision complexities.The introduction also connects resilience with diagnosability and opacity, and describes resilience as insensitive to faults.Source: §1.1 · p. 2
1.2 Review on the two basic tools needed
- The review traces concurrent composition and observers from LFSA verification to their nontrivial extensions for LRTAs.For LFSAs, concurrent composition supports inference-based verification and, with observers, concealment-based verification.Source: §1.2 · p. 3
1.3 Contribution
- The paper defines LRTA resilience as returning to normalcy after a faulty event without leaking its occurrence, and gives a verification algorithm based on concurrent composition and observers.The negation of resilience can be verified in N2EXPTIME in the size of an LRTA.Source: §1.3 · p. 4
1.4 Structure of the paper
- Section 2 presents notation, LRTA definitions, concurrent composition, and observers; Section 3 gives the main results, followed by a short conclusion in Section 4.Source: §1.4 · p. 4
2 Preliminaries
The preliminaries define LRTAs and their timed observations, then introduce state estimation, self-composition, and observers as tools for reasoning about them. These tools track possible states and synchronize observable behavior, with finite observers providing a computable representation.
2.1 Notation
- The notation section defines Σ* as finite strings over Σ, including the empty string, and Σ+ as those strings excluding it.It also uses |w| for string length and gives standard set notation for number systems and integer ranges.Source: §2.1 · p. 4
2.2 Labeled real-time automata
- An LRTA has finite states and events, transitions with allowed time intervals, initial states, and a labeling function; it uses one clock reset at every transition.Runs generate timed label sequences from observable events, while unobservable events produce no label.Source: §2.2 · pp. 4–6
2.3 State estimation
- The current-state estimate gives the states an LRTA could occupy after a timed label sequence, allowing instantaneous unobservable transitions after its last observable event.The instantaneous-state estimate captures states reachable through unobservable transitions at the instant of entry to a state set.Source: §2.3 · p. 6
2.4 The notion of concurrent composition
- Self-composition CC(A) pairs an LRTA with itself, synchronizing observable events with matching labels while unobservable transitions interleave; computing it is NP-complete.The paired observable transition represents both events occurring after a common delay, followed only by instantaneous transitions.Source: §2.4 · pp. 7–8
2.5 The notion of observer
- An observer tracks state estimates along timed label sequences; its pre-observer has an infinite alphabet, while a finite observer is a computable sub-automaton and may not be unique.For any observed timed label sequence, the observer state represents the corresponding current-state estimate.Source: §2.5 · pp. 8–9
3 Main results
The section defines resilience as eventual observational recovery to non-faulty behavior and presents a necessary-and-sufficient test for non-resilience and an N2EXPTIME verification method using observers and concurrent composition. It illustrates the verification by establishing that A3.8 is resilient with respect to Ef and RI, returning to normalcy without releasing ef.
3.1 Formulation of a definition of resilience
- Recovery points are state pairs whose future languages are equal or included, and resilience requires a faulty run eventually to match a non-faulty run with the same timed labeled sequence.The matched behavior makes the faulty event unobservable and returns the automaton to normalcy.Source: §3.1 · p. 10
3.2 A necessary and sufficient condition for resilience
- Non-resilience holds exactly when a faulty run reaches a repeating automaton–pre-observer state pair without a corresponding recovery point.Theorem 3.2 expresses the repetition through equal automaton and observer states at two positions, alongside the absence of recovery-point matches.Source: §3.2 · pp. 11–12
3.3 A verification algorithm for resilience
- A computable observer and concurrent composition yield an N2EXPTIME verification of non-resilience, replacing the uncomputable pre-observer; the composition and its relevant transitions are also computable in N2EXPTIME.Theorem 3.6 makes the concurrent-composition condition necessary and sufficient for non-resilience.Source: §3.3 · pp. 13, 15, 16
- Lemma 3.3 equates conditions (A) and (B), and Proposition 3.4 states that the satisfiability of (B) and (C) can be verified in N2EXPTIME.Source: §3.3 · pp. 14–15
- The example automaton A3 is not resilient with respect to the specified faulty event set and inclusion recovery points, as shown by both the negation criterion and the concurrent-composition test.Source: §3.3 · p. 16
- The concurrent composition contains a unique faulty transition, (q0, {q0}) → (q4, {q5, q6}), with (q4, q5) ∈ RI.Source: §3.3 · p. 18
- A3.8 is resilient with respect to Ef and RI, returning to normalcy after the faulty event ef occurs.The paper attributes the resilience conclusion to Theorem 3.6.Source: §3.3 · p. 18
- The occurrence of ef cannot be released because both runs produce the timed label sequence (a, 1 + t), and no run corresponds to (25).Source: §3.3 · p. 18
4 Conclusion
The paper defines LRTA resilience and gives an N2EXPTIME verification algorithm based on concurrent composition and observer, while identifying further resilience notions and practical applications as future topics.
4 Conclusion
- The paper defines LRTA resilience and designs an N2EXPTIME verification algorithm based on concurrent composition and observer.Source: §4 · p. 18
- Future work includes exploring other notions of resilience.Source: §4 · p. 18
- Future work also includes practical applications, such as using resilience notions to describe intelligent-agent behavior.Source: §4 · p. 18