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 1 for a state space with V states and E transitions in 0 (V (V + E) . vertical bar Phi vertical bar). In this work, we improve the model checking algorithm of TCTL <=,>= properties, obtaining time complexity of 0 ((V 1g V + E) . vertical bar Phi vertical bar). 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. (C) 2017 Elsevier B.V. All rights reserved.