Floating time transition system: More efficient analysis of timed actors

Ehsan Khamespanah, Marjan Sirjani, Mahesh Viswanathan, Ramtin Khosravi

Research output: Chapter in Book/Report/Conference proceedingConference contribution


The actor model is a concurrent object-based computational model in which event-driven and asynchronously communicating actors are units of concurrency. Actors are widely used in modeling real-time and distributed systems. Floating-Time Transition System (FTTS) is proposed as an alternative semantics for timed actors, and schedulability and deadlock-freedom analysis techniques have been developed for it. The absence of shared variables and blocking send or receive, and the presence of single-threaded actors along with non-preemptive execution of each message server, ensure that the execution of message servers do not interfere with each other. The Floating-Time Transition System semantics exploits this by executing message servers in isolation, and by relaxing the synchronization of progress of time among actors, and thereby has fewer states in the transition system. Considering an actorbased language, we prove a weak bisimulation relation between FTTS and Timed Transition System, which is generally the standard semantic framework for discrete-time systems. Thus, the FTTS semantics preserves event-based branching-time properties. Our experimental results show a significant reduction in the state space for most of the examples we have studied.

Original languageEnglish (US)
Title of host publicationFormal Aspects of Component Software - 12th International Conference, FACS 2015, Revised Selected Papers
EditorsChristiano Braga, Peter Csaba Ölveczky
Number of pages19
ISBN (Print)9783319289335
StatePublished - 2016
Event12th International Conference on Formal Aspects of Component Software, FACS 2015 - Niteroi, Brazil
Duration: Oct 14 2015Oct 16 2015

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Other12th International Conference on Formal Aspects of Component Software, FACS 2015


  • Actor model
  • Floating time transition system
  • State space reduction
  • Timed Rebeca
  • Timed transition system
  • Verification

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)


Dive into the research topics of 'Floating time transition system: More efficient analysis of timed actors'. Together they form a unique fingerprint.

Cite this