wiki:news_2006

Version 6 (modified by Dr. Ivan S. Zapreev, 10 years ago) (diff)

Added a nice picture

TracNav?

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

MRMC News

Recent news of 2008

News archive of 2007

News archive of 2006

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: ???

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 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.

News archive of 2005