Differences

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

--- main [2021/12/13 12:51] – [Manual, structure of the EPMC] andrea
+++ main [2021/12/13 13:04] (current) – [Access to EPMC] andrea
@@ Line 32: / Line 32: @@
   * Bounded responsibility property, ''(G req<sub>1</sub>  => F<sup>%%<=%%bound</sup> reply<sub>1</sub>)& ... & (G req<sub>n</sub> => F<sup>%%<=%%bound</sup> reply<sub>n</sub>)'': for a family of components, each component ''i'' replies to a given request within a given time bound.
   * Bounded responsibility property with fairness, ''(GF req<sub>1</sub> & ... & GF req<sub>n</sub>) & (G req<sub>1</sub> => F<sup>%%<=%%bound</sup> reply<sub>1</sub>) & ... & (G req<sub>n</sub> => F<sup>%%<=%%bound</sup> reply<sub>n</sub>)'': similar to bounded responsibility, suitable for ''P<sub>max=?</sub>'' in MDPs. The fairness ensures that the system is scheduled such that the request occurs infinitely often.
-  * Bounded responsibility property with fairness, ''(GF req<sub>1</sub> & ... & GF req<sub>n</sub>) => ((G req<sub>1</sub> => F<sup>%%<=%%bound</sup> reply<sub>1</sub>) & ... & (G req<sub>n</sub> => F<sup>%%<=%%bound</sup> reply<sub>n</sub>))'': similar to bounded responsibility, suitable for ''P<sub>min=?</sub>'' in MDPs. The fairness ensures that the system is scheduled such that the request occurs infinitely often.
+  * Bounded responsibility property with fairness, ''(GF req<sub>1</sub> & ... & GF req<sub>n</sub>) => %%((%%G req<sub>1</sub> => F<sup>%%<=%%bound</sup> reply<sub>1</sub>) & ... & (G req<sub>n</sub> => F<sup>%%<=%%bound</sup> reply<sub>n</sub>%%))%%'': similar to bounded responsibility, suitable for ''P<sub>min=?</sub>'' in MDPs. The fairness ensures that the system is scheduled such that the request occurs infinitely often.
 ----
@@ Line 65: / Line 65: @@
 ===== Access to EPMC =====
   * Download: EPMC is now available publicly. It can be obtained 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.
-  * Online version of EPMC is available [[https://iscasmc.ios.ac.cn/IscasMC/user/center|here]]. Screenshot of EPMC online:
+  * Online version of EPMC is available [[https://tis.ios.ac.cn/IscasMC/login/login|here]]. Screenshot of EPMC online:
 {{:epmc-web.png}}
@@ Line 79: / Line 79: @@
 === How to install and use ===
-This tool is implemented as a plugin in ePMC. The source code can be found at https://github.com/fuchen1991/epmc-petl. All the implementation details related to PETL model checking are under “epmc-petl/plugins/propertysolver-petl”. And you can find the experiment files used in the paper under “experiment_files”. For building, running and other information about ePMC, please visit https://github.com/liyi-david/ePMC.
+This tool is implemented as a plugin in ePMC. The source code can be found at https://github.com/fuchen1991/epmc-petl. All the implementation details related to PETL model checking are under “epmc-petl/plugins/propertysolver-petl”. And you can find the experiment files used in the paper under “experiment_files”. For building, running and other information about EPMC, please visit https://github.com/ISCAS-PMC/ePMC.
 To perform PETL model checking, please set the following options:
@@ Line 97: / Line 97: @@
 You need to prepare 3 files: one for the model, one for equivalence relations, and one for properties.
-The models should be in the PRISM format([[http://www.prismmodelchecker.org/manual/ThePRISMLanguage|http://www.prismmodelchecker.org/manual/ThePRISMLanguage]]). Note that we redefine the composition of the modules to make the agents all take one local action in each transition, so the transitions from different modules will not synchronize according to the parallel composition operator.
+The models should be in [[http://www.prismmodelchecker.org/manual/ThePRISMLanguage|the PRISM format]]. Note that we redefine the composition of the modules to make the agents all take one local action in each transition, so the transitions from different modules will not synchronize according to the parallel composition operator.
 The equivalence relations are described in this format:
@@ Line 125: / Line 125: @@
 </code>
-Other properties can be described by the PRISM language([[http://www.prismmodelchecker.org/manual/PropertySpecification|http://www.prismmodelchecker.org/manual/PropertySpecification]]).
+Other properties can be described by [[http://www.prismmodelchecker.org/manual/PropertySpecification|the PRISM language]].
 ==== Plugin: dpCTL ====
 === Introduction ===
@@ Line 148: / Line 148: @@
 The following are projects related to 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 model checker for differentially privacy verification.
   * [[https://iscasmc.ios.ac.cn/roll/doku.php|ROLL]]: A learning based tool for models inferring.