PMaude: Rewrite-based Specification Language for Probabilistic Object Systems

Gul Agha, José Meseguer, Koushik Sen

Research output: Contribution to journalArticlepeer-review

Abstract

We introduce a rewrite-based specification language for modelling probabilistic concurrent and distributed systems. The language, based on PMaude, has both a rigorous formal basis and the characteristics of a high-level rule-based programming language. Furthermore, we provide tool support for performing discrete-event simulations of models written in PMaude, and for statistically analyzing various quantitative aspects of such models based on the samples that are generated through discrete-event simulation. Because distributed and concurrent communication protocols can be modelled using actors (concurrent objects with asynchronous message passing), we provide an actor PMaude module. The module aids writing specifications in a probabilistic actor formalism. This allows us to easily write specifications that are purely probabilistic - and not just non-deterministic. The absence of such (un-quantified) non-determinism in a probabilistic system is necessary for a form of statistical analysis that we also discuss. Specifically, we introduce a query language called Quantitative Temporal Expressions (or QuaTEx in short), to query various quantitative aspects of a probabilistic model. We also describe a statistical technique to evaluate QuaTEx expressions for a probabilistic model.

Original languageEnglish (US)
Pages (from-to)213-239
Number of pages27
JournalElectronic Notes in Theoretical Computer Science
Volume153
Issue number2 SPEC. ISS.
DOIs
StatePublished - May 23 2006

Keywords

  • PMaude
  • QuaTEx
  • Specification language
  • actors
  • non-deterministic specification
  • probabilistic specification
  • query language

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'PMaude: Rewrite-based Specification Language for Probabilistic Object Systems'. Together they form a unique fingerprint.

Cite this