Welcome! This site is intended to provide access to a model checking tool developed for the Exogenous Probabilistic Propositional Language (EPPL) and its temporal extensions, Exogenous Probabilistic Computational Tree Logic (EpCTL) and Exogenous Probabilistic Linear Temporal Logic (EpLTL).

Introduction   ·   The Logic   ·   The Tool   ·   References

EPPL is a probabilistic logic developed by Mateus, Sernadas and Sernadas. It has great expressive power that confers it the potential to be used in many fields such as security, reliability, randomized algorithms or quantum computation. As such, the development of tools to deal with this logic is very desirable.

As part of my master's degree thesis, I have coded a simple model checking tool for EPPL temporal extensions, for Windows OS.

If you are wondering why Windows OS only, the reason is that in order to describe states we chose to use MSBNX, a Bayesian networks representation tool developed and supported by Microsoft. Needless to say it is only compatible with Windows, so we decided that the first version of the tool would be Windows compatible. It will eventually be adapted for Unix based OS (once I find a good BN representation tool compatible with them). For now, we are stuck with Windows.

The program is completely open to anyone who wishes to use or modify it.

Enjoy!

In order to understand and use the model checking tool, one must first understand the state logic EPPL and the temporal extensions, EpCTL and EpLTL. For that matter, I recommend reading [MSS05], the original paper on EPPL as well as [BMNP:CTL07], and [BM:LTL09] on the temporal extensions. You may also find [MS04] useful.

An extremely summary description of the logics can be found on the user manual, here.

Essentialy, EPPL is built by enriching classical propositional logic: one takes propositional formulae (and comparisons of terms) as atoms; then, an analog of the propositional construction is built over these "atoms". For implementation purposes, a model for EPPL is a probability space where a probability is assigned to each valuation over the set of propositional symbols in the original propositional logic*.
This allows for relevant probabilistic reasoning over classical formulae.

EPPL temporal extensions, EpLTL and EpCTL should have intuitive syntax and semantics for anyone who knows CTL and LTL [CGD:MC00]. The usual Kripke Structures are extended to probabilistic Kripke structures, and semantics are the obvious extensions of the semantics of EPPL.

*This is not the original definition of an EPPL model. An explanation for this (small) difference can be found here (chapter 3).

The first algorithm proposed (by Baltazar and Mateus) for model checking EPPL can be found in [BM:CTL08]. Although similar, this is not the actual implementation used in the tool.

The main difference between the algorithms lies in the fact that the algorithm proposed in REFERENCE differs from the usual CTL or LTL algorithm in that it uses the model checking algorithm for EPPL to model check EPPL formulas instead of verifying if a propositional symbol belongs to a set, whereas the actual implementation presented here simply reduces the problem to the classical model checking procedure (by using the state logic model checker) and then interprets the result back to EpTemp semantics. The complexity class of the problem remains the same (PSPACE), but the actual implementation is much easier.

We chose to make use of a third party model checker for the classical model checking procedures. The reasoning was that there already exist very good tools that have been refined at length and have dedicated teams working on them; therefore, it would not be reasonable to expect that a tool developed in the scope of this project could compete in efficiency with them. We decided that the time would be better spent developing the reduction algorithm. We chose to use NuSMV, a reimplementation of the CMU SMV. It is a very handy tool on its own, with lots of functionalities and you should check it out.

You can use the tool via a GUI or using a textfile as input. The first approach is is intuitive and aesteticaly pleasant, but may be cumbersome for large systems; the second is less straightforwad but may easily scripted. Details can be found in the user manual.

There are plans to extend the functionalities of the tool as this is a first version. We will upload such improvements as we deem them publishable.

The Tool

The source code is available here. It is NOT extensively commented (and a few comments are still in portuguese) and is poorly structured. This will be corrected in due time. Proceed at your own risk. Please notice that you will have to download and link the CUDD package for handling multi terminal decision diagrams, which can be tricky in Windows.

[MSS05] P.Mateus, A. Sernadas and C.Sernadas. Exogenous semantics approach to enriching logics. In G. Sica, editor, Essays on the Foundations of Mathematics and Logic , volume 1, pages 165-194. Polimetrica, 2005.

[MS04] P.Mateus and A. Sernadas. Exogenous quantum logic. In Proceedings of CombLog'04, Workshop on Combination of Logics: Theory and Applications, pages 141-149, 2004.

[BMNP:CTL07] P. Baltazar, P. Mateus, R. Nagarajan, and N. Papanikolaou. Exogenous probabilistic computation tree logic.Electronic Notes in Theoretical Computer Science, 190(3):95--110, 2007.

[BM:LTL09] P. Baltazar and P. Mateus. Temporalization of probabilistic propositional logic. In S. Artemov and A. Nerode, editors, Logic Foundations of Computer Science 2009, volume 5407 of Lecture Notes in Computer Science, pages 46--60. Springer, 2009.

[CGD:MC00] Edmund M. Clarke, Orna Grumberg and Doron A. Peled. Model Checking. MIT Press, 2000.

Please bear in mind that the tool is not yet fully developed, so a significant number of bugs is to be expected. Kindly report any problems you find to me