PMaude: Rewrite-based Specification Language for Probabilistic Object Systems

Agha, Gul A.; Meseguer, José; Sen, Koushik

Permalink

https://hdl.handle.net/2142/10959 Copy

Description

Title

PMaude: Rewrite-based Specification Language for Probabilistic Object Systems

Author(s)

• Agha, Gul A.
• Meseguer, José
• Sen, Koushik

Issue Date

2005-03

Keyword(s)

• programming languages
• distributed systems

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 functional programming language. Furthermore, we provide tool support for performing discrete-event simulations of models written in PMaude, and for statistically verifying formal properties 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 model-checking of probabilistic temporal logic properties that we also discuss.

Type of Resource

text

Permalink

http://hdl.handle.net/2142/10959

Copyright and License Information

You are granted permission for the non-commercial reproduction, distribution, display, and performance of this technical report in any format, BUT this permission is only for a period of 45 (forty-five) days from the most recent time that you verified that this technical report is still available from the University of Illinois at Urbana-Champaign Computer Science Department under terms that include this permission. All other rights are reserved by the author(s).

Owning Collections