Languages of CTL and RTCTL Calculi in Real-Time Analysis of a System Described by a Fault Tree with Time Dependencies

Minimal cut sets are one of the main results of analysis of fault trees with time dependencies. They contain events leading to a hazard (root of the tree). The events have minimal and maximal time intervals from both their start and end times to the possible appearance of the hazard. These informations may be useful in real-time operation of a system, for which the fault tree was constructed. To achieve it, while observing the working system, the real start and end times of events from the minimal cut sets must be registered to predict the time remaining to the hazard - possibly the time still left to repair a damage, to run a safety procedure, or even to halt the system before it crashes. This article presents a use of languages of CTL and RTCTL calculi in a description of the minimal cut sets and then a use of such a description in deductive real-time analysis of the described system.