wiki:News

TracNav?

http://www.mrmc-tool.org/images/news.gif

News

12.01.2011

A new MRMC version is released. The changes are:

  • a new algorithm to compute time-bounded reachability probabilities for non-uniform CTMDPIs. This feature is based on "Continuous-Time Stochastic Games with Time-Bounded Reachability" by Brazdil et al.
  • Bug fixes for time-bounded reachability algorithm for uniform CTMDPIs
  • Improved partition refinement algorithm for lumping. The new algorithm uses a variant of quicksort instead of splay trees for efficient splitting.

Besides this, we worked on improved data structure for sparse matrices for this version; however, while it provided improvements in bisimulation minimisation, it led to serious degradation in simulation. Therefore, we abandoned this plan.

11.11.2009

The next MRMC (version 1.4.1) will be released in the beginning of December (8'th). The new major features will be:

  • The pure simulation-based method for model checking steady-state properties of CTMCs. This completes the CTMC simulation engine.
  • Fixed Fox-Glynn algorithm: In certain cases the computed Poisson probabilities were incorrect. This fix is crucial for computing transient-reachability probabilities of CTMCs (time-interval and time-bounded until).

18.09.2009

Several papers about MRMC were published at QEST'09:

  • "Simulation-Based CTMC Model Checking: An Empirical Evaluation" PDF BibTex
  • "The Ins and Outs of The Probabilistic Model Checker MRMC" PDF BibTex

11.03.2009

We thank Chitra for her work on the next version of MRMC and wish her good luck with her Master's final project! Her successor will be Falko Dulat, who continue working on the next version of MRMC.

18.09.2008

After one and a half year of active participation in the MRMC project, Christina Jansen is going to focus her efforts on her Master's thesis. We wish her good luck!

18.09.2008

MRMC (version 1.4) has been released! Some of the new release features are:

  • Improved performance of bitset datastructure,
  • Added heuristics for discrete event simulation of CTMCs,
  • Small bugfix in the reachability analysis of CTMDPs,
  • Increased test coverage by additional internal and functional tests,
  • Added initial annotations to MRMC for SPLINT static verification,
  • Revised manual.

18.09.2008

An online-survey is now available! As we are working on a major revision of MRMC, we need your input to focus efforts in the right direction. The survey will take about 5 minutes to complete and we would really appreciate your participation.

06.08.2008

A Tutorial Video about MRMC usage was added to the main page of the web site. This video features the main things one has to know in order to be able to use the tool.

01.08.2008

Starting from 01.08.2008 Chitra Hapsari Ayuningtyas begins to work as a scientific programmer in the MRMC project.

27.06.2008

MRMC (version 1.3) has been released! Some of the new release features are:

  • CTMC model checking via discrete event simulation,
  • CTMDPI model checking of time bounded reachability properties,
  • Improved user interface,
  • New and extended manuals (PDF format),
  • Improved source code and tool's reliability,
  • Performance tests for the simulation engine.

12.06.2008

The MRMC web pages are being moved to the new domain: www.mrmc-tool.org.

15.03.2008

Ivan S. Zapreev became a Postdoc in the MAS2.2 group at Centrum voor Wiskunde en Informatica , Amsterdam, The Netherlands.

07.03.2008

Ivan S. Zapreev got his PhD degree at the University of Twente, Enschede, The Netherlands. PDF BibTex

Some of the pictures from the event can be found here: LINK.

01.03.2008

Viet Yen Nguyen has joined the MOVES group in RWTH-Aachen. He will work on advancing MRMC to the next level within the scope of the COMPASS project (sponsored by European Space Agency).

29.11.2007

On 12 Nov 2007, at the last VOSS2 project meeting, Joost-Pieter Katoen gave a talk about the latest development of MRMC. The presentation slides can be found here PDF.

23.11.2007

The paper "How Fast and Fat Is Your Probabilistic Model Checker?" PDF was presented at HVC'07 conference, see BibTex for the reference. The presentation slides can be found here PPT.

03.09.2007

This web-site now features an MRMC downloads counter, see the banner at the top of the page.

27.08.2007

MRMC web-site now conforms to the Transitional XHTML 1.0 standard.

24.08.2007

A news-subscription option was added to the download form of MRMC.

21.08.2007

Our paper, named "How Fast and Fat Is Your Probabilistic Model Checker?" was accepted at HVC'07 conference, see: PDF BibTex

21.08.2007

The New MRMC Version (1.2.2) is now available! This release contains but is not limited by the following features:

  • The support of Mac OS X and Windows + Cygwin platform.
  • Gauss-Seidel algorithm for solving systems of linear equations was added for unbounded-until operator (CSL, PCTL).
  • A non-recursive method for searching Bottom Strongly Connected Components was added.
  • New MRMC is up to two times faster (CSL, PCTL).
  • The test-suite update.

For more details check out the READ.ME file in the root of the distribution's directory tree.

20.08.2007

The new release of MRMC (version 1.2.2) is scheduled to be released within the upcoming two weeks. It will feature the support of Mac OS X and Windows + Cygwin platforms. Among other improvements, new algorithms for graph analysis and solving systems of linear equations were added, the tool performance has been significantly improved, and several important bugs were fixed.

27.07.2007

Varun Aggarwala has left back to India, we wish him a pleasant flight!

24.05.2007

Varun Aggarwala has started working on implementing the simulation relations on Markov Chains into MRMC. He is an internship student from CSE Dept. IIT Guwahati, India.

11.05.2007

Marcel Oldenkamp has brightly defended his Master thesis Probabilistic model checking, A comparison of tools. at the University of Twente, The Netherlands. Marcel has gotten 9, congratulations!

09.05.2007

The upcoming micro-release of MRMC will feature the support of the Mac OS X platform.

09.05.2007

The scheme of the MRMC architecture, on the Index title page of the web-site, has been updated. It can be also reached via this LINK.

20.04.2007

On 10.05.2006 Marcel Oldenkamp defends his Master thesis "Probabilistic model checking, A comparison of tools." at the University of Twente, The Netherlands.

17.04.2007

Starting from 01.05.2006 Christina Jansen begins to work as a scientific programmer (HiWi?) in the MRMC project.

04.04.2007

The preliminary results of Marcel Oldenkamp's master-thesis research, titled: "Probabilistic model checking, A comparison of tools." can be found here LINK.

04.04.2007

The master thesis of Tim Kemna, titled: "Bisimulation Minimization and Probabilistic Model Checking." can be found here PDF.

28.03.2007

The paper "Bisimulation minimization mostly speeds up probabilistic model checking" PDF was presented at TACAS'07 conference, see BibTex for the reference.

The presentation slides can be found here PPT.

09.01.2007

The New MRMC Version (1.2.1) is now available! This release contains but is not limited by the following features:

  • Minor Algorithmic improvements.
  • Interface-usability improvements.
  • Bug-fixes, memory-leaks elimination.
  • Test suite update, with new memory-usage statistics.
  • Source-code refinement.

For more details check out the READ.ME file in the root of the distribution's directory tree.

29.12.2006

In the early January 2007 the New MRMC Version (1.2.1) is going to be available!

15.12.2006

WARNING: The Qureshi-Sanders uniformization algorithm requires ordering of the state space according to the state rewards. That is why temporarily:

  • properly ordered input files should be provided to MRMC
  • lumping (bisimulation) should not be used

in case of CSRL model checking that involves Qureshi-Sanders uniformization algorithm (Time- and reward-bounded until). We already work on fixing these limitations and malfunctions.

08.12.2006

  • Our paper, named "Bisimulation minimization mostly speeds up probabilistic model checking." was accepted at TACAS'07 PDF BibTex
  • There is now a new web-page on the MRMC web-site. It is called Related. There you may find some third-party projects, papers etc. that reference MRMC in this or that way. If you have your reference, that you would like to add/remove, just e-mail us at: mrmc-users mailing list.

14.11.2006

One of you, our dear users, have found that it is possible to build and use MRMC under Windows using Cygwin. The trick is to add:

#include < sys/time.h >

line into the includes section of:

src/mcc.c and src/io/parser/parser_etmcc2.y

files of the distribution. Note that this fix has been added into the currently downloadable version since 14.11.2006.

06.11.2006

Since version 3.0, Prism supports exporting its models into the MRMC model format. For more details see Section 1. of the Documentation of the MRMC interface, version 1.2 or Section 6. of the READ.ME file in the MRMC distribution (starting from version 1.2).

06.11.2006

The New MRMC Version (1.2) is now available! This release contains but is not limited by the following features:

  • Support of formula- dependent and independent lumping for PCTL, CSL, PRCTL, CSRL logics (Until operators).
  • Optimized performance, fixed memory leaks and bugs.
  • Improved command-line parameters support and results output.
  • An extended, separately distributed, test suite with NEW performance tests.

For more details check out the READ.ME file in the root of the distribution's directory tree.

06.11.2006

  • Check out our latest update of the Bibliography page. Now you can find more data like pdf's and presentations there!
  • A paper named "Bisimulation minimization mostly speeds up probabilistic model checking." was submitted to TACAS'07 PDF BibTex

30.10.2006

Now there is a Wikipedia page for MRMC.

25.10.2006

The new MRMC release is coming soon, stay tuned! The next release will contain but won't be limited to the following features:

  • Support of formula dependent and formula independent lumping for PCTL, CSL, PRCTL, CSRL logics (Until operators).
  • Optimized performance, fixed memory leaks and bugs.
  • Improved command-line parameters support and results output.
  • An extended, separately distributed, test suite with NEW performance tests.

15.09.2006

The paper on "Safe On-The-Fly Steady-State Detection for Time-Bounded Reachability" was presented at QEST'06 conference, see BibTex for the reference.

22.08.2006

Tim Kemna brilliantly defended his Master Thesis: "Bisimulation Minimization and Probabilistic Model Checking", currently we work on integrating these techniques into the next release of MRMC.

02.06.2006

The paper on "Safe On-The-Fly Steady-State Detection for Time-Bounded Reachability" has been accepted at QEST'06 conference, see BibTex for the reference.

03.03.2006

A New MRMC Version (1.1 beta)! We have fixed two vital bugs in the implementation of CSL logic:

  • Next operator did not work well.
  • The implementation of Interval Until operator was flawed.

We would like to thank Jose Martinez for detecting these bugs!

24.02.2006

A smart PhD student and a friend of mine, Jose Martinez, has found a potential flaw in MRMC for CSL model checking which is detectable using the Hubble case study (a part of ETMCC distribution). We are investigating this right now. If it is really a problem then the fix will follow immediately.

14.02.2006

The Downloads section now works in a NORMAL mode. You may start downloading sources of MRMC right away! Also some documentation was added to the Spec.? section.

By the way, Happy Valentine's Day!

10.02.2006

The Downloads section now works in a test mode. You may receive the distribution dummy and put yourself on the list for getting the real MRMC version :)!

09.02.2006

An important memory leakage in MRMC was found and eliminated by Tim Kemna, who is our new group member. Great work, Tim!

04.02.2006

This MRMC Home-page has been started!

03.01.2006

The CTIT technical report on Safe On-The-Fly Steady-State Detection for Time-Bounded Reachability has been published, see BibTex for the reference.

15.11.2005

The MRMC is now the first tool that incorporates "Safe On-The-Fly Steady-State Detection for Time-Bounded Reachability"!

30.09.2005

The beta version of MRMC is available for Linux platform. In order to obtain it please e-mail us at mrmc[at]cs.utwente.nl.

23.09.2005

There was a paper publication at QEST'05 Conference on the MRMC tool, see BibTex for details.

Last modified 6 years ago Last modified on Jan 12, 2011, 1:14:33 PM