Formulation of Concurrent Composition in Labeled Real-Time Automata with an Application to Fault Diagnosis

Real-time automata are a widely-used class of real-time systems. In this paper, we formulate a notion of concurrent composition of a labeled real-time automaton (LRTA) in which every pair of an observable faulty path and an observable nonfaulty path that can produce the same timed label sequence are synchronized and unobservable transitions interleave. We prove that a concurrent composition can be computed in time nondeterministically polynomial in the size of the LRTA. We also formulate a notion of diagnosability of an LRTA using infinite runs and derive a necessary and sufficient condition for the negation of the diagnosability using concurrent composition. Finally, we prove that the diagnosability verification problem is coN P-complete. It is well known that the diagnosability verification problem for general labeled timed automata is PSPACE-complete. We find more efficient algorithms for verifying diagnosability for the subclass LRTAs.