TY - GEN
T1 - Floating time transition system
T2 - 12th International Conference on Formal Aspects of Component Software, FACS 2015
AU - Khamespanah, Ehsan
AU - Sirjani, Marjan
AU - Viswanathan, Mahesh
AU - Khosravi, Ramtin
N1 - Funding Information:
This work has been partially supported by the project “Timed Asynchronous Reactive Objects in Distributed Systems: TARO” (nr. 110020021) of the Icelandic Research Fund.
Publisher Copyright:
© Springer International Publishing Switzerland 2016.
PY - 2016
Y1 - 2016
N2 - 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.
AB - 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.
KW - Actor model
KW - Floating time transition system
KW - State space reduction
KW - Timed Rebeca
KW - Timed transition system
KW - Verification
UR - http://www.scopus.com/inward/record.url?scp=84958073311&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84958073311&partnerID=8YFLogxK
U2 - 10.1007/978-3-319-28934-2_13
DO - 10.1007/978-3-319-28934-2_13
M3 - Conference contribution
AN - SCOPUS:84958073311
SN - 9783319289335
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 237
EP - 255
BT - Formal Aspects of Component Software - 12th International Conference, FACS 2015, Revised Selected Papers
A2 - Braga, Christiano
A2 - Ölveczky, Peter Csaba
PB - Springer
Y2 - 14 October 2015 through 16 October 2015
ER -