An efficient TCTL model checking algorithm and a reduction technique for verification of timed actor models

NP-hard time complexity of model checking algorithms for TCTL properties in dense time is one of the obstacles against using model checking for the analysis of real-time systems. Alternatively, a polynomial time algorithm is suggested for model checking of discrete time models against TCTL≤,≥ properties (i.e. TCTL properties without U=c modalities). The algorithm performs model checking against a given formula Φ for a state space with V states and E transitions in O(V(V+E)⋅|Φ|). In this work, we improve the model checking algorithm of TCTL≤,≥ properties, obtaining time complexity of O((Vlg⁡V+E)⋅|Φ|). We tackle the model checking of discrete timed actors as an application of the proposed algorithms. We show how the result of the fine-grained semantics of discrete timed actors can be model checked efficiently against TCTL≤,≥ properties using the proposed algorithm. This is illustrated using the timed actor modeling language Timed Rebeca. In addition to introducing a new efficient model checking algorithm, we propose a reduction technique which safely eliminates instantaneous transitions of transition systems (i.e. transition with zero time duration). We show that the reduction can be applied on-the-fly during the generation of the original timed transition system without a significant cost. We demonstrate the effectiveness of the reduction technique via a set of case studies selected from various application domains. Besides, while TCTL≤,≥ can be model checked in polynomial time, model checking of TCTL properties with U=c modalities is an NP-complete problem. Using the proposed reduction technique, we provide an efficient algorithm for model checking of complete TCTL properties over the reduced transition systems.