Differences

This shows you the differences between two versions of the page.

--- epmc:main [2020/11/23 10:43] – ::1
+++ epmc:main [Unknown date] (current) – removed - external edit (Unknown date) 127.0.0.1
@@ Line 1: / Line 1: @@
-====== EPMC - (An Extendible Probabilistic Model Checker, previously known as IscasMC) ======
-====== Introduction ======
-EPMC is a successor of the model checker IscasMC which only focuses on PLTL model checking over MDP.
-===== Support probabilistic models =====
-  * Discrete Time Markov Chains (DTMCs)
-  * Markov Decision Processes (MDPs)
-  * Continuous Time Markov Chains (CTMCs)
-  * Stochastic Multi-player games (SMGs)
-  * Probabilistic Parity Games (PPGs)
-(All input models can be specified in the PRISM format and JANI format.)
-===== Support property  =====
-  * PCTL
-  * PLTL
-  * PCTL*
-  * CSL (in progress)
-  * Transient Properties (in progress)
-  * Expected Rewards (in progress)
-The main characteristics of EPMC are the high modularity of the tool, the possibility to extend EPMC with plugins to add new functionalities, and its availability on multiple platforms. EPMC achieves its flexibility by an infrastructure that consists of a minimal core part and multiple plugins that is very convenient to develop a new model checker based on the core parts of EPMC.
-EPMC is mainly developed in Java, but accesses a few libraries written in C/C++ to increase performance or to access well established legacy code. Its graphical user interface (GUI) is a single static webpage. The GUI communicates with the backend, where core functions (like model checking) and high-privilege operations (like file I/O) are realised.
-----
-====== Download and usage ======
-ePMC is now available publicly. It can be accessed online on GitHub, at [[https://github.com/ISCAS-PMC/ePMC|this repository]]. \\
-Please follow our [[https://github.com/ISCAS-PMC/ePMC/wiki/Documentations|wiki documentations]] to build and use EPMC.
-----
-====== Contact ======
-Comments and feedback about any aspect of ePMC are very welcome. Please contact:
-  * [[https://iscasmc.ios.ac.cn/?page_id=152|Andrea Turrini]]
-----
-====== Other projects =======
-The following are projects that use ePMC:
-  * [[http://faculty.sist.shanghaitech.edu.cn/faculty/songfu/Projects/pamc/epmc-pamc/|EPMC-PAMC]]: A model checker for probabilistic alternating-time Mu-Calculus.
-  * [[https://iscasmc.ios.ac.cn/dpctl/doku.php|dpCTL]]: A tool for checking differential privacy CTL properties on Markov chains and Markov decision processes.
-  * [[https://iscasmc.ios.ac.cn/?page_id=1855|ePMC-petl]]: A plugin of ePMC, which is for “Model Checking Probabilistic Epistemic Logic for Probabilistic Multiagent Systems”.