Statistical model checking for composite actor systems

Jonas Eckhardt, Tobias Mühlbauer, José Meseguer, Martin Wirsing

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


In this paper we propose the so-called composite actor model for specifying composed entities such as the Internet. This model extends the actor model of concurrent computation so that it follows the "Reflective Russian Dolls" pattern and supports an arbitrary hierarchical composition of entities. To enable statistical model checking we introduce a new scheduling approach for composite actor models which guarantees the absence of unquantified nondeterminism. The underlying executable specification formalism we use is the rewriting logic-based semantic framework Maude, its probabilistic extension PMaude, and the statistical model checker PVESTA. We formalize a model transformation which - given certain formal requirements - generates a scheduled specification. We prove the correctness of the scheduling approach and the soundness of the transformation by introducing the notions of strong zero-time rule confluence and time-passing bisimulation and by showing that the transformation is a time-passing bisimulation for strongly zero-time rule confluent composite actor specifications.

Original languageEnglish (US)
Title of host publicationRecent Trends in Algebraic Development Techniques - 21st International Workshop, WADT 2012, Revised Selected Papers
Number of pages18
StatePublished - 2013
Event21st International Workshop on Algebraic Development Techniques, WADT 2012 - Salamanca, Spain
Duration: Jun 7 2012Jun 10 2012

Publication series

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


Other21st International Workshop on Algebraic Development Techniques, WADT 2012


  • Actor system
  • Composite actor
  • Maude
  • Rewriting logic
  • Statistical model checking

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)


Dive into the research topics of 'Statistical model checking for composite actor systems'. Together they form a unique fingerprint.

Cite this