Labeled real-time automata recover from faults without revealing errors
Resilience in labeled real-time automata
Computational Complexity
Summary
This paper looks at special systems called labeled real-time automata (LRTA) that can experience faults. The authors define when these systems are resilient, meaning they can recover to normal behavior after faults and keep the errors hidden. They provide a way to check if an LRTA is resilient by using specific mathematical tools. This helps model intelligent agents that can handle mistakes and keep functioning smoothly.
What this means in practice
- •For real-time system engineers: Verify if a real-time software system can recover from faults without exposing errors to users during operation.
- •For embedded system developers: Design embedded controllers that maintain normal operation after unexpected faults by applying resilience verification for labeled automata.
A theory result. No direct application yet.
Authors
Kuize Zhang
Abstract
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.