skip to main content
10.1145/2687357.2687366acmconferencesArticle/Chapter ViewAbstractPublication PagessplashConference Proceedingsconference-collections
research-article

Efficient TCTL Model Checking Algorithm for Timed Actors

Published: 20 October 2014 Publication History

Abstract

Non-Polynomial time complexity of model checking algorithms for TCTL properties in dense time is one of the obstacles against using model checking for timed systems. Alternatively, polynomial time algorithms are suggested for model checking discrete time models presented as Duration Time Graphs (DTG) versus a subset of TCTL formula (TCTL≤,≥). While TCTL≤,≥ can be model checked in polynomial time, the problem of model checking for exact time condition (TCTL=) is an NP-Hard problem unless certain conditions hold. In this work we tackle model checking of timed actors using DTG. At the first step, we propose a reduction technique by folding all the instantaneous transitions, resulting folded timed transition system (FTS). At the second step, we show how the FTS of timed actors with discrete time can be mapped to a DTG. Then, we show when the necessary conditions hold for the FTS of timed actors and hence there is an O(|S|2 • Φ) algorithm for model checking of complete TCTL properties (including TCTL≤,≥ and TCTL=) which have small constant time quantifiers. We use a set of case studies to illustrate the impact of using this technique in different application domains.

References

[1]
Rebeca Home Page. http://www.rebeca-lang.org.
[2]
L. Aceto and F. Laroussinie. Is your model checker on time? on the complexity of model checking for timed modal logics. Journal of Logic and Algebraic Programming, 52--53:7--51, 2002.
[3]
R. Alur and D. L. Dill. A Theory of Timed Automata. Theoretical Computer Science, 126(2):183--235, 1994.
[4]
C. Baier and J.-P. Katoen. Principles of Model Checking. MIT Press, 2008. ISBN 978-0--262-02649--9.
[5]
J. Bengtsson, K. G. Larsen, F. Larsson, P. Pettersson, and W. Yi. UPPAAL - a Tool Suite for Automatic Verification of Real-Time Systems. In R. Alur, T. A. Henzinger, and E. D. Sontag, editors, Hybrid Systems, volume 1066 of Lecture Notes in Computer Science, pages 232--243. Springer, 1995. ISBN 3--540--61155-X.
[6]
S. V. Campos and E. M. Clarke. Theories and experiences for real-time system development. chapter Real-time Symbolic Model Checking for Discrete Time Models, pages 129--145. World Scientific Publishing Co., Inc., River Edge, NJ, USA, 1994. ISBN 981-02--1923--7. URL http://dl.acm.org/citation.cfm?id=207907.207912.
[7]
S. V. A. Campos, E. M. Clarke,W. R. Marrero, M. Minea, and H. Hiraishi. Computing quantitative characteristics of finite-state real-time systems. In RTSS, pages 266--270. IEEE Computer Society, 1994. ISBN 0--8186--6600--5.
[8]
F. S. de Boer, M. M. Jaghoori, C. Laneve, and G. Zavattaro. Decidability problems for actor systems. In M. Koutny and I. Ulidowski, editors, CONCUR, volume 7454 of Lecture Notes in Computer Science, pages 562--577. Springer, 2012. ISBN 978--3--642--32939--5.
[9]
E. A. Emerson, A. K. Mok, A. P. Sistla, and J. Srinivasan. Quantitative temporal reasoning. volume 4, pages 331--352, 1992.
[10]
M. R. Garey and D. S. Johnson. Computers and Intractability: A Guide to the Theory of NP-Completeness. W. H. Freeman, 1979. ISBN 0--7167--1044--7.
[11]
M. Geilen, S. Tripakis, and M. Wiggers. The earlier the better: a theory of timed actor interfaces. In M. Caccamo, E. Frazzoli, and R. Grosu, editors, HSCC, pages 23--32. ACM, 2011. ISBN 978-1-4503-0629-4.
[12]
E. Khamespanah, Z. Sabahi-Kaviani, R. Khosravi,M. Sirjani, and M.-J. Izadi. Timed-rebeca schedulability and deadlock-freedom analysis using floating-time transition system. In G. A. Agha, R. H. Bordini, A. Marron, and A. Ricci, editors, AGERE!@SPLASH, pages 23--34. ACM, 2012. ISBN 978--1--4503--1630--9.
[13]
F. Laroussinie, P. Schnoebelen, and M. Turuani. On the expressivity and complexity of quantitative branching time temporal logics. Theoretical Computer Science, 297 (1--3):297--315, 2003.
[14]
F. Laroussinie, N. Markey, and P. Schnoebelen. Efficient timed model checking for discrete-time systems. Theoretical Computer Science, 353(1--3):249--271, 2006.
[15]
B. Magnusson. Simulation-Based Analysis of Timed Rebeca Using TeProp and SQL. Master's thesis, Reykjavk University, School of Computer Science, Iceland, 2012. http://rebeca.cs.ru.is/files/MasterThesisBrynjarMagnusson2012.pdf.
[16]
M. Nykänen and E. Ukkonen. The exact path length problem. J. Algorithms, 42(1):41--53, 2002.
[17]
Z. Sabahi-Kaviani, R. Khosravi, M. Sirjani, P.C. Ölveczky, and E. Khamespanah. Formal semantics and analysis of timed rebeca in real-time maude. In C. Artho and P. C. Ölveczky, editors, FTSCS, volume 419 of Communications in Computer and Information Science, pages 178--194. Springer, 2013. ISBN 978--3--319-05415--5.
[18]
Z. Sharifi, M. Mosaffa, S. Mohammadi, and M. Sirjani. Functional and performance analysis of network-onchips using actor-based modeling and formal verification. ECEASST, 66, 2013.
[19]
M. Sirjani and M. M. Jaghoori. Ten Years of Analyzing Actors: Rebeca Experience. In G. Agha, O. Danvy, and J. Meseguer, editors, Formal Modeling: Actors, Open Systems, Biological Systems, volume 7000 of Lecture Notes in Computer Science, pages 20--56. Springer, 2011. ISBN 978--3--642--24932--7.
[20]
M. Sirjani, A. Movaghar, A. Shali, and F. S. de Boer. Modeling and Verification of Reactive Systems using Rebeca. Fundam. Inform., 63(4):385--410, 2004.

Cited By

View all
  • (2018)Modeling and analyzing real-time wireless sensor and actuator networks using actors and model checkingInternational Journal on Software Tools for Technology Transfer (STTT)10.1007/s10009-017-0480-320:5(547-561)Online publication date: 1-Oct-2018
  • (2017)Efficient exact paths for dyck and semi-dyck labeled path reachability (extended abstract)2017 IEEE 8th Annual Ubiquitous Computing, Electronics and Mobile Communication Conference (UEMCON)10.1109/UEMCON.2017.8249039(247-253)Online publication date: Oct-2017
  • (2016)Fast point-to-point Dyck constrained shortest paths on a DAG (Extended abstract)2016 IEEE 7th Annual Ubiquitous Computing, Electronics & Mobile Communication Conference (UEMCON)10.1109/UEMCON.2016.7777894(1-7)Online publication date: Oct-2016
  • Show More Cited By

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences
AGERE! '14: Proceedings of the 4th International Workshop on Programming based on Actors Agents & Decentralized Control
October 2014
146 pages
ISBN:9781450321891
DOI:10.1145/2687357
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

In-Cooperation

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 20 October 2014

Permissions

Request permissions for this article.

Check for updates

Author Tags

  1. actor model
  2. discrete time transition system
  3. duration transition graph
  4. model checking
  5. tctl
  6. timed rebeca

Qualifiers

  • Research-article

Funding Sources

Conference

SPLASH '14
Sponsor:

Acceptance Rates

AGERE! '14 Paper Acceptance Rate 9 of 14 submissions, 64%;
Overall Acceptance Rate 19 of 35 submissions, 54%

Upcoming Conference

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)2
  • Downloads (Last 6 weeks)0
Reflects downloads up to 08 Mar 2025

Other Metrics

Citations

Cited By

View all
  • (2018)Modeling and analyzing real-time wireless sensor and actuator networks using actors and model checkingInternational Journal on Software Tools for Technology Transfer (STTT)10.1007/s10009-017-0480-320:5(547-561)Online publication date: 1-Oct-2018
  • (2017)Efficient exact paths for dyck and semi-dyck labeled path reachability (extended abstract)2017 IEEE 8th Annual Ubiquitous Computing, Electronics and Mobile Communication Conference (UEMCON)10.1109/UEMCON.2017.8249039(247-253)Online publication date: Oct-2017
  • (2016)Fast point-to-point Dyck constrained shortest paths on a DAG (Extended abstract)2016 IEEE 7th Annual Ubiquitous Computing, Electronics & Mobile Communication Conference (UEMCON)10.1109/UEMCON.2016.7777894(1-7)Online publication date: Oct-2016
  • (2016)Statistical model checking of Timed Rebeca modelsComputer Languages, Systems and Structures10.1016/j.cl.2016.01.00445:C(53-79)Online publication date: 1-Apr-2016
  • (2016)On Time ActorsEssays Dedicated to Frank de Boer on Theory and Practice of Formal Methods - Volume 966010.1007/978-3-319-30734-3_25(373-392)Online publication date: 1-Jan-2016
  • (2015)Floating Time Transition SystemRevised Selected Papers of the 12th International Conference on Formal Aspects of Component Software - Volume 953910.1007/978-3-319-28934-2_13(237-255)Online publication date: 14-Oct-2015

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media