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((V lgV + 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.