PMaude: Rewrite-based Specification Language for Probabilistic Object 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 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

References in zbMATH (referenced in 25 articles )

Showing results 1 to 20 of 25.
Sorted by year (citations)

1 2 next

  1. Lemos, Marcilio O. O.; Dantas, Yuri Gil; Fonseca, Iguatemi E.; Nigam, Vivek: On the accuracy of formal verification of selective defenses for TDoS attacks (2018)
  2. Liu, Si; Ölveczky, Peter Csaba; Meseguer, José: Modeling and analyzing mobile ad hoc networks in Real-Time Maude (2016)
  3. Elleuch, Maissa; Hasan, Osman; Tahar, Sofiène; Abid, Mohamed: Formal probabilistic analysis of detection properties in wireless sensor networks (2015)
  4. Liu, Si; Ölveczky, Peter Csaba; Meseguer, José: Formal analysis of leader election in MANETs using Real-Time Maude (2015)
  5. Martí-Oliet, Narciso; Ölveczky, Peter Csaba; Talcott, Carolyn: José Meseguer: scientist and friend extraordinaire (2015)
  6. Belzner, Lenz; De Nicola, Rocco; Vandin, Andrea; Wirsing, Martin: Reasoning (on) service component ensembles in rewriting logic (2014)
  7. Nakajima, Shin: Everlasting challenges with the OBJ language family (2014)
  8. Bentea, Lucian; Ölveczky, Peter Csaba: A probabilistic strategy language for probabilistic rewrite theories and its application to cloud computing (2013)
  9. Eckhardt, Jonas; Mühlbauer, Tobias; Meseguer, José; Wirsing, Martin: Statistical model checking for composite actor systems (2013)
  10. Meseguer, José; Roşu, Grigore: The rewriting logic semantics project: a progress report (2013)
  11. Bulychev, Peter; David, Alexandre; Guldstrand Larsen, Kim; Legay, Axel; Li, Guangyuan; Bøgsted Poulsen, Danny; Stainer, Amelie: Monitor-based statistical model checking for weighted metric temporal logic (2012)
  12. Katelman, Michael; Keller, Sean; Meseguer, José: Rewriting semantics of production rule sets (2012)
  13. Krause, Christian; Giese, Holger: Probabilistic graph transformation systems (2012)
  14. Meseguer, José: Twenty years of rewriting logic (2012)
  15. Wirsing, Martin; Eckhardt, Jonas; Mühlbauer, Tobias; Meseguer, José: Design and analysis of cloud-based architectures with KLAIM and Maude (2012) ioport
  16. AlTurki, Musab; Meseguer, José: PVeSTA: A parallel statistical model checking and quantitative analysis tool (2011) ioport
  17. Basuki, Thomas Anung; Cerone, Antonio; Milazzo, Paolo: Translating stochastic CLS into Maude (2009)
  18. Durán, Francisco; Ölveczky, Peter Csaba: A guide to extending Full Maude illustrated with the implementation of real-time Maude (2009) ioport
  19. Ölveczky, Peter Csaba; Thorvaldsen, Stian: Formal modeling, performance estimation, and model checking of wireless sensor network algorithms in Real-Time Maude (2009)
  20. Şerbănuţă, Traian Florin; Roşu, Grigore; Meseguer, José: A rewriting logic approach to operational semantics (2009)

1 2 next