An efficient TCTL model checking algorithm and a reduction technique for verification of timed actor models
2018 (English)In: Science of Computer Programming, ISSN 0167-6423, E-ISSN 1872-7964, Vol. 153, p. 1-29Article in journal (Refereed) Published
Abstract [en]
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((VlgV+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.
Place, publisher, year, edition, pages
Elsevier B.V. , 2018. Vol. 153, p. 1-29
Keywords [en]
Actor model, Durational transition graph, Model checking, TCTL, Timed Rebeca, Computational complexity, Interactive computer systems, Modeling languages, Polynomial approximation, Real time systems, Semantics, Actor models, Model checking algorithm, Polynomial-time algorithms, Reduction techniques, Timed transition systems, Transition graphs
National Category
Computer and Information Sciences
Identifiers
URN: urn:nbn:se:mdh:diva-38161DOI: 10.1016/j.scico.2017.11.004ISI: 000424068300001Scopus ID: 2-s2.0-85040332415OAI: oai:DiVA.org:mdh-38161DiVA, id: diva2:1176513
2018-01-222018-01-222018-02-15Bibliographically approved