mdh.sePublications
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
An efficient TCTL model checking algorithm and a reduction technique for verification of timed actor models
School of Electrical an Computer Engineering, University of Tehran, Tehran, Iran.
School of Computer Science, Reykjavik University, Reykjavik, Iceland.
Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
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((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.

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
Available from: 2018-01-22 Created: 2018-01-22 Last updated: 2018-02-15Bibliographically approved

Open Access in DiVA

No full text in DiVA

Other links

Publisher's full textScopus

Authority records BETA

Sirjani, Marjan

Search in DiVA

By author/editor
Sirjani, Marjan
By organisation
Embedded Systems
In the same journal
Science of Computer Programming
Computer and Information Sciences

Search outside of DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetric score

doi
urn-nbn
Total: 6 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf