PMaude: Rewrite-based Specification Language for Probabilistic Object Systems
Agha, Gul A.; Meseguer, José; Sen, Koushik
- PMaude: Rewrite-based Specification Language for Probabilistic Object Systems
- Agha, Gul A.
- Meseguer, José
- Sen, Koushik
- Issue Date
- programming languages
- distributed systems
- 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
- 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).
Edit Collection Membership